CNF.h File Reference
Include dependency graph for CNF.h:
This graph shows which files directly or indirectly include this file:
Go to the source code of this file.
Namespaces | |
| carl | |
| carl is the main namespace for the library. | |
| carl::formula_to_cnf | |
Typedefs | |
| template<typename Poly > | |
| using | carl::formula_to_cnf::TseitinConstraints = std::vector< Formula< Poly > > |
| template<typename Poly > | |
| using | carl::formula_to_cnf::ConstraintBounds = FastMap< Poly, std::map< typename Poly::NumberType, std::pair< Relation, Formula< Poly > >> > |
Functions | |
| 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) More... | |
| 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. More... | |
| template<typename Poly > | |
| Formula< Poly > | carl::to_cnf (const Formula< Poly > &f, bool keep_constraints=true, bool simplify_combinations=false, bool tseitin_equivalence=true) |
| Converts the given formula to CNF. More... | |
