dlinear::PredicateAbstractor Class Reference

Predicate abstraction is a method to convert a first-order logic formula into a Boolean formula. More...

#include <PredicateAbstractor.h>

Inheritance diagram for dlinear::PredicateAbstractor:

Public Member Functions
	PredicateAbstractor (const Config &config)
	Construct a new PredicateAbstractor object with the given config.
Formula	Process (const Formula &f)
	Convert a first-order logic formula f into a Boolean formula by predicate abstraction.
Formula	Process (const std::vector< Formula > &formulas)
	Convert a vector first-order logic formula formulas into a Boolean formula by creating a single conjunction through predicate abstraction.
const std::unordered_map< Variable, Formula > &	var_to_formula_map () const
	Get read-only access to the map of previously converted formulae to variable of the PredicateAbstractor.
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 Member Functions
Formula	VisitFormula (const Formula &f) const override
	Visit an atomic formula.

Private Attributes
std::unordered_map< Variable, Formula >	var_to_formula_map_
	Map from Boolean variable to previously converted formula.
std::unordered_map< Formula, Variable >	formula_to_var_map_
	Map from previously converted formula to Boolean variable.
LinearFormulaFlattener	flattener_
	Linear formula flattener.

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

Predicate abstraction is a method to convert a first-order logic formula into a Boolean formula.

The boolean formula will be a boolean variable or a conjunction of boolean variables. The object keeps a bijective map between newly introduced the boolean variables and the first-order logic formulae.

Definition at line 27 of file PredicateAbstractor.h.

Constructor & Destructor Documentation

PredicateAbstractor()

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

inlineexplicit

Construct a new PredicateAbstractor object with the given config.

Parameters

config

configuration

Definition at line 33 of file PredicateAbstractor.h.

Member Function Documentation

Process() [1/2]

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

nodiscard

Convert a first-order logic formula f into a Boolean formula by predicate abstraction.

For example, a formula \( (x > 0) \land (y < 0) \) will be converted into \( b_1 \land b_2 \) while \( b_1 \) corresponds with \( x > 0 \) and \( b_2 \) corresponds with \( y < 0 \). The class provides operator[b] which looks up the corresponding formula for a Boolean variable \( b \).

Parameters

f	formula to be converted

Returns

boolean formula

Definition at line 18 of file PredicateAbstractor.cpp.

Process() [2/2]

Formula dlinear::PredicateAbstractor::Process ( const std::vector< Formula > & formulas )

nodiscard

Convert a vector first-order logic formula formulas into a Boolean formula by creating a single conjunction through predicate abstraction.

For example, a formula \( (x > 0) \land (y < 0) \) will be converted into \( b_1 \land b_2 \) while \( b_1 \) corresponds with \( x > 0 \) and \( b_2 \) corresponds with \( y < 0 \). The class provides operator[b] which looks up the corresponding formula for a Boolean variable \( b \).

Parameters

f	formula to be converted

Returns

boolean formula

Definition at line 25 of file PredicateAbstractor.cpp.

var_to_formula_map()

const std::unordered_map< Variable, Formula > & dlinear::PredicateAbstractor::var_to_formula_map ( ) const

inlinenodiscard

Get read-only access to the map of previously converted formulae to variable of the PredicateAbstractor.

Returns

map of previously converted formulae to variable of the PredicateAbstractor

Definition at line 61 of file PredicateAbstractor.h.

VisitFormula()

Formula dlinear::PredicateAbstractor::VisitFormula ( const Formula & f ) const

nodiscardoverrideprivate

Visit an atomic formula.

It flattens the formula and creates a new Boolean variable if the formula is not present in the map. Otherwise, it returns the corresponding Boolean variable.

Parameters

f	atomic formula to visit

Returns

newly created Boolean variable in the map var_to_formula_map_ if the formula is not present

existing Boolean variable in the map var_to_formula_map_ if the formula was already present

Definition at line 30 of file PredicateAbstractor.cpp.

---

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

• dlinear/symbolic/PredicateAbstractor.h
• dlinear/symbolic/PredicateAbstractor.cpp