QEQuery.h File Reference

#include <smtrat-common/smtrat-common.h>

Include dependency graph for QEQuery.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

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

Typedefs
using	smtrat::qe::QEQuery = std::vector< std::pair< QuantifierType, std::vector< carl::Variable > >>

Enumerations
enum class	smtrat::qe::QuantifierType { smtrat::qe::EXISTS , smtrat::qe::FORALL }

Functions
std::ostream &	smtrat::qe::operator<< (std::ostream &os, QuantifierType qt)
std::ostream &	smtrat::qe::operator<< (std::ostream &os, const QEQuery &q)
std::vector< std::pair< QuantifierType, carl::Variable > >	smtrat::qe::flattenQEQuery (const QEQuery &query)
QuantifierType	smtrat::qe::type (const std::pair< QuantifierType, std::vector< carl::Variable >> &p)
std::vector< carl::Variable >	smtrat::qe::vars (const std::pair< QuantifierType, std::vector< carl::Variable >> &p)