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

Inheritance diagram for dlinear::PlaistedGreenbaumCnfizer:

Public Member Functions
	PlaistedGreenbaumCnfizer (const Config &config)
	Construct a new PlaistedGreenbaumCnfizer object with the given `config`.

std::pair< std::vector< Formula >, std::vector< Variable > >	Process (const Formula &f) const
	Convert a `f` into an equi-satisfiable formula `f'` 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. Used to transform nested formulas inside universal quantification.

Additional Inherited Members
Protected Member Functions inherited from dlinear::FormulaVisitor< std::vector< Formula > &, std::vector< Variable > & >
	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

Plaisted-Greenbaum 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 28 of file PlaistedGreenbaumCnfizer.h.

Constructor & Destructor Documentation

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

inlineexplicit

Construct a new PlaistedGreenbaumCnfizer object with the given config.

Parameters

config configuration

Definition at line 34 of file PlaistedGreenbaumCnfizer.h.

std::pair< std::vector< Formula >, std::vector< Variable > > dlinear::PlaistedGreenbaumCnfizer::Process ( const Formula & f ) const

nodiscard

Convert a f into an equi-satisfiable formula f' in CNF.

Parameters

f	A formula to be converted.

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