SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
qe.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include "../QEQuery.h"
4 
5 #include <smtrat-common/smtrat-common.h>
6 
7 namespace smtrat::qe::cad {
8 
9 FormulaT eliminateQuantifiers(const FormulaT& qfree, const QEQuery& quantifiers);
10 
11 }
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