SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
qe.cpp File Reference
#include "qe.h"
#include "CADElimination.h"
Include dependency graph for qe.cpp:

Go to the source code of this file.

Namespaces

 smtrat
 Class to create the formulas for axioms.
 
 smtrat::qe
 
 smtrat::qe::cad
 

Functions

FormulaT smtrat::qe::cad::eliminateQuantifiers (const FormulaT &qfree, const QEQuery &quantifiers)