smtrat::qe Namespace Reference

Namespaces
	cad
	coverings
	fm
	fmplex
	util

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

Enumerations
enum class	QuantifierType { EXISTS , FORALL }

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

Typedef Documentation

QEQuery

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

Definition at line 17 of file QEQuery.h.

Enumeration Type Documentation

QuantifierType

enum smtrat::qe::QuantifierType

strong

Enumerator
EXISTS
FORALL

Definition at line 8 of file QEQuery.h.

Function Documentation

flattenQEQuery()

std::vector<std::pair<QuantifierType,carl::Variable> > smtrat::qe::flattenQEQuery ( const QEQuery &  query )

inline

Definition at line 29 of file QEQuery.h.

Here is the caller graph for this function:

operator<<() [1/2]

std::ostream& smtrat::qe::operator<< ( std::ostream &  os, const QEQuery &  q  )

inline

Definition at line 19 of file QEQuery.h.

operator<<() [2/2]

std::ostream& smtrat::qe::operator<< ( std::ostream &  os, QuantifierType  qt  )

inline

Definition at line 9 of file QEQuery.h.

qe()

std::optional< FormulaT > smtrat::qe::qe

(

const FormulaT &

formula

)

Definition at line 10 of file smtrat-qe.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

type()

QuantifierType smtrat::qe::type ( const std::pair< QuantifierType, std::vector< carl::Variable >> &  p )

inline

Definition at line 39 of file QEQuery.h.

Here is the caller graph for this function:

vars()

std::vector<carl::Variable> smtrat::qe::vars ( const std::pair< QuantifierType, std::vector< carl::Variable >> &  p )

inline

Definition at line 43 of file QEQuery.h.

Here is the caller graph for this function: