smtrat::covering_ng::formula Namespace Reference

Namespaces
	complexity
	formula_ds
	pp

Data Structures
class	GraphEvaluation

Typedefs
using	ImplicantOrdering = std::function< bool(cadcells::datastructures::Projections &, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &)>
using	ConstraintOrdering = std::function< bool(cadcells::datastructures::Projections &, const cadcells::datastructures::PolyConstraint &, const cadcells::datastructures::PolyConstraint &)>

Enumerations
enum class	Valuation { TRUE , FALSE , MULTIVARIATE , UNKNOWN }

Functions
std::ostream &	operator<< (std::ostream &o, Valuation v)
carl::Variable	new_var (const cadcells::Assignment &old_ass, const cadcells::Assignment &new_ass)
void	postprocess (cadcells::datastructures::Projections &proj, boost::container::flat_set< cadcells::datastructures::PolyConstraint > &i)

Typedef Documentation

ConstraintOrdering

using smtrat::covering_ng::formula::ConstraintOrdering = typedef std::function<bool(cadcells::datastructures::Projections&, const cadcells::datastructures::PolyConstraint&, const cadcells::datastructures::PolyConstraint&)>

Definition at line 11 of file FormulaEvaluation.h.

ImplicantOrdering

using smtrat::covering_ng::formula::ImplicantOrdering = typedef std::function<bool(cadcells::datastructures::Projections&, const boost::container::flat_set<cadcells::datastructures::PolyConstraint>&, const boost::container::flat_set<cadcells::datastructures::PolyConstraint>&)>

Definition at line 9 of file FormulaEvaluation.h.

Enumeration Type Documentation

Valuation

enum smtrat::covering_ng::formula::Valuation

strong

Enumerator
TRUE
FALSE
MULTIVARIATE
UNKNOWN

Definition at line 13 of file FormulaEvaluation.h.

Function Documentation

new_var()

carl::Variable smtrat::covering_ng::formula::new_var	(	const cadcells::Assignment &	old_ass,
		const cadcells::Assignment &	new_ass
	)

Definition at line 648 of file FormulaEvaluationGraph.cpp.

Here is the caller graph for this function:

operator<<()

std::ostream& smtrat::covering_ng::formula::operator<< ( std::ostream &  o, Valuation  v  )

inline

Definition at line 16 of file FormulaEvaluation.h.

postprocess()

void smtrat::covering_ng::formula::postprocess	(	cadcells::datastructures::Projections &	proj,
		boost::container::flat_set< cadcells::datastructures::PolyConstraint > &	i
	)

Definition at line 883 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

Here is the caller graph for this function: