carl::formula_to_cnf Namespace Reference

Typedefs
template<typename Poly >
using	TseitinConstraints = std::vector< Formula< Poly > >
template<typename Poly >
using	ConstraintBounds = FastMap< Poly, std::map< typename Poly::NumberType, std::pair< Relation, Formula< Poly > >> >

Functions
template<typename Poly >
std::vector< Formula< Poly > >	construct_iff (const Formula< Poly > &lhs, const std::vector< Formula< Poly >> &rhs_and)
	Constructs the equivalent of (iff lhs (and *rhs_and))) The result is the list (=> lhs (and *rhs_and)) (=> rhs !lhs) (for each rhs in rhs_and) More...
template<typename Poly >
Formula< Poly >	to_cnf_or (const Formula< Poly > &f, bool keep_constraints, bool simplify_combinations, bool tseitin_equivalence, TseitinConstraints< Poly > &tseitin)
	Converts an OR to cnf. More...

Typedef Documentation

ConstraintBounds

template<typename Poly >

using carl::formula_to_cnf::ConstraintBounds = typedef FastMap<Poly, std::map<typename Poly::NumberType, std::pair<Relation,Formula<Poly> >> >

Definition at line 33 of file CNF.h.

TseitinConstraints

template<typename Poly >

using carl::formula_to_cnf::TseitinConstraints = typedef std::vector<Formula<Poly> >

Definition at line 31 of file CNF.h.

Function Documentation

construct_iff()

template<typename Poly >

std::vector<Formula<Poly> > carl::formula_to_cnf::construct_iff	(	const Formula< Poly > &	lhs,
		const std::vector< Formula< Poly >> &	rhs_and
	)

Constructs the equivalent of (iff lhs (and *rhs_and))) The result is the list (=> lhs (and *rhs_and)) (=> rhs !lhs) (for each rhs in rhs_and)

Definition at line 19 of file CNF.h.

Here is the caller graph for this function:

to_cnf_or()

template<typename Poly >

Formula<Poly> carl::formula_to_cnf::to_cnf_or	(	const Formula< Poly > &	f,
		bool	keep_constraints,
		bool	simplify_combinations,
		bool	tseitin_equivalence,
		TseitinConstraints< Poly > &	tseitin
	)

Converts an OR to cnf.

Definition at line 40 of file CNF.h.

Here is the call graph for this function:

Here is the caller graph for this function: