Transforms a symbolic formula f into a CNF formula by preserving its semantics. More...

Inheritance diagram for dlinear::NaiveCnfizer:

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

Formula	Process (const Formula &f) const
	Convert a `f` into an equivalent 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
Nnfizer	nnfizer_ {config_}
	NNFizer. Used to convert the formula into NNF.

Additional Inherited Members
Protected Member Functions inherited from dlinear::FormulaVisitor<>
	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

Transforms a symbolic formula f into a CNF formula by preserving its semantics.

Note: This transform can increase the size exponentially. We are using this transformation in TseitinCnfizer when we process the nested formula in a universally quantified formula.

Definition at line 23 of file NaiveCnfizer.h.

Constructor & Destructor Documentation

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

inlineexplicit

Construct a new NaiveCnfizer object with the given config.

Parameters

config configuration

Definition at line 29 of file NaiveCnfizer.h.

Formula dlinear::NaiveCnfizer::Process ( const Formula & f ) const

nodiscard

Convert a f into an equivalent formula f' in CNF.

Parameters

f	formula to be converted

Definition at line 20 of file NaiveCnfizer.cpp.

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