SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
qe.cpp
Go to the documentation of this file.
1 #include "qe.h"
2 
3 #include "CADElimination.h"
4 
5 namespace smtrat::qe::cad {
6 
7 FormulaT eliminateQuantifiers(const FormulaT& qfree, const QEQuery& quantifiers) {
8  cad::CADElimination elim(qfree, quantifiers);
9  return elim.eliminateQuantifiers();
10 }
11 
12 }
smtrat::qe::cad::eliminateQuantifiers
FormulaT eliminateQuantifiers(const FormulaT &qfree, const QEQuery &quantifiers)
Definition: qe.cpp:7
smtrat::qe::QEQuery
std::vector< std::pair< QuantifierType, std::vector< carl::Variable > >> QEQuery
Definition: QEQuery.h:17
smtrat::FormulaT
carl::Formula< Poly > FormulaT
Definition: types.h:37