Inheritance diagram for dlinear::IfThenElseEliminator:

Public Member Functions
Formula	Process (const Formula &f)
	Returns a equisatisfiable formula by eliminating if-then-expressions in `f` by introducing new variables.

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.

Public Member Functions inherited from dlinear::GenericExpressionVisitor< Expression, const Formula & >
const IterationStats &	stats () const
	Get read-only access to the statistics of the GenericExpressionVisitor.

const Config &	config () const
	Get read-only access to the configuration of the GenericExpressionVisitor.

Private Attributes
std::vector< Formula >	added_formulas_
	The added formulas introduced by the elimination process.

std::unordered_set< Variable >	ite_variables_
	The variables introduced by the elimination process.

std::unordered_map< Expression, Variable >	ite_to_var_
	Mapping from ITE to the corresponding variable obtained by ITE elimination.

std::unordered_map< Variable, Formula >	ite_var_to_formulas_
	Mapping from ITE to the corresponding variable obtained by ITE elimination.

std::size_t	counter_
	Counter for the number of introduced variables.

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

Protected Attributes inherited from dlinear::GenericExpressionVisitor< Expression, const Formula & >
const Config &	config_
	Configuration.

IterationStats	stats_
	Statistics.

Detailed Description

Eliminate If-Then-Else expressions by introducing new variables.

Todo: Check "Efficient Term ITE Conversion for Satisfiability Modulo Theories", H. Kim, F. Somenzi, H. Jin. Twelfth International Conference on Theory and Applications of Satisfiability Testing (SAT'09).

Definition at line 28 of file IfThenElseEliminator.h.

Member Function Documentation

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

nodiscard

Returns a equisatisfiable formula by eliminating if-then-expressions in f by introducing new variables.

Parameters

f	Formula to be processed.

Definition at line 21 of file IfThenElseEliminator.cpp.

std::vector<Formula> dlinear::IfThenElseEliminator::added_formulas_

mutableprivate

The added formulas introduced by the elimination process.

Resets after each call to Process.

Definition at line 93 of file IfThenElseEliminator.h.

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