Tsietin transformation is a method to convert a formula into an equi-satisfiable vector of formulae in CNF. More...

Inheritance diagram for dlinear::TseitinCnfizer:

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.

Detailed Description

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.

Constructor & Destructor Documentation

dlinear::TseitinCnfizer::TseitinCnfizer ( const Config & config )

inlineexplicit

Construct a new TseitinCnfizer object with the given config.

Parameters

config configuration

Definition at line 33 of file TseitinCnfizer.h.

std::vector< Formula > dlinear::TseitinCnfizer::Process ( const Formula & f ) const

nodiscard

Convert f into an equi-satisfiable formula in CNF.

Parameters

f	formula to convert

Definition at line 36 of file TseitinCnfizer.cpp.

The documentation for this class was generated from the following files: