dlinear
0.0.1
Delta-complete SMT solver for linear programming
|
Tsietin transformation is a method to convert a formula into an equi-satisfiable vector of formulae in CNF. More...
#include <TseitinCnfizer.h>
Public Member Functions | |
TseitinCnfizer (const Config &config) | |
Construct a new TseitinCnfizer object with the given config . | |
std::vector< Formula > | Process (const Formula &f) const |
Convert f into an equi-satisfiable formula in CNF. | |
Public Member Functions inherited from dlinear::GenericFormulaVisitor< Formula, Args... > | |
const IterationStats & | stats () const |
Get read-only access to the statistics of the FormulaVisitor. | |
const Config & | config () const |
Get read-only access to the configuration of the FormulaVisitor. | |
Private Attributes | |
const NaiveCnfizer | naive_cnfizer_ |
Naive CNFizer. Transforms nested formulas inside universal quantification. | |
Additional Inherited Members | |
Protected Member Functions inherited from dlinear::FormulaVisitor< std::map< Variable, Formula > & > | |
FormulaVisitor (const Config &config, const std::string &class_name="FormulaVisitor") | |
Construct a new FormulaVisitor object with the given config . | |
Protected Member Functions inherited from dlinear::GenericFormulaVisitor< Formula, Args... > | |
GenericFormulaVisitor (const Config &config, const std::string &class_name="GenericFormulaVisitor") | |
Construct a new FormulaVisitor object with the given config . | |
Protected Attributes inherited from dlinear::GenericFormulaVisitor< Formula, Args... > | |
const Config & | config_ |
Configuration. | |
IterationStats | stats_ |
Statistics. | |
Tsietin transformation is a method to convert a formula into an equi-satisfiable vector of formulae in CNF.
The method can introduce extra Boolean variables. Check Wikipedia for more information.
Definition at line 27 of file TseitinCnfizer.h.
|
inlineexplicit |
Construct a new TseitinCnfizer object with the given config
.
config | configuration |
Definition at line 33 of file TseitinCnfizer.h.
Convert f
into an equi-satisfiable formula in CNF.
f | formula to convert |
Definition at line 36 of file TseitinCnfizer.cpp.