dlinear  0.0.1
Delta-complete SMT solver for linear programming
Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Private Attributes | List of all members
dlinear::LinearFormulaFlattener Class Reference

Used by the PredicateAbstractor to ensure that all the theory literals are in the flattened standard form. More...

#include <LinearFormulaFlattener.h>

Public Member Functions

 LinearFormulaFlattener (const Config &config)
 Construct a new LinearFormulaFlattener object with the given config.
 
Formula Flatten (const Formula &formula)
 Flatten the given formula.
 

Private Member Functions

Formula BuildFlatteredFormula (const Expression &lhs, const Expression &rhs, FormulaKind kind) const
 Use the updated expressions to build a new formula, also removing any mult expression from the left-hand-side.
 

Private Attributes

const Config & config_
 Configuration.
 
std::unordered_map< Formula, Formula > flattened_formulas_
 Cache for the flattered formulas.
 

Detailed Description

Used by the PredicateAbstractor to ensure that all the theory literals are in the flattened standard form.

See also
LinearFormulaFlattener::Flatten

Definition at line 22 of file LinearFormulaFlattener.h.

Constructor & Destructor Documentation

◆ LinearFormulaFlattener()

dlinear::LinearFormulaFlattener::LinearFormulaFlattener ( const Config & config)
inlineexplicit

Construct a new LinearFormulaFlattener object with the given config.

Parameters
configconfiguration

Definition at line 28 of file LinearFormulaFlattener.h.

Member Function Documentation

◆ BuildFlatteredFormula()

Formula dlinear::LinearFormulaFlattener::BuildFlatteredFormula ( const Expression & lhs,
const Expression & rhs,
FormulaKind kind ) const
nodiscardprivate

Use the updated expressions to build a new formula, also removing any mult expression from the left-hand-side.

If a formula is in the form \( a x \lessgtr b \) where \( a, b \in \mathbb{R}, a \ne 0 \) are constants and \( x \in \mathbb{R} \) is an unknown variable, this method will remove the multiplication from the left-hand-side of the formula by dividing both sides by \( a \). If a formula is in the form \( a_1x_1 + a_2x_2 + \dots a_nx_n \lessgtr c \) where \( a_i, c_i \in \mathbb{R} \) are constants and \( x_i \in \mathbb{R} \) is an unknown variable \( \forall i \in \{1, 2, \dots, n\} \), this method will ensure that the first term in the addition of the left-hand-side has a positive coefficient, by multiplying both sides by \( -1 \) if necessary.

Parameters
lhsleft-hand-side expression of the new formula
rhsright-hand-side expression of the new formula
kindkind of the formula (e.g. Eq, Lt, Geq, ...)

Definition at line 37 of file LinearFormulaFlattener.cpp.

◆ Flatten()

Formula dlinear::LinearFormulaFlattener::Flatten ( const Formula & formula)
nodiscard

Flatten the given formula.

A formula is considered flatten if:

  • is in the form \( a_1x_1 + a_2x_2 + \dots a_nx_n \lessgtr c \) where \( a_i, c_i \in \mathbb{R} \) are constants, \( a_1 > 0 \) and \( x_i \in \mathbb{R} \) is a variable \( \forall i \in \{1, 2, \dots, n\} \)
  • calling the method Expand on both of the formula's terms outputs the same expression as the one used as the input
    Warning
    The formula returned has a very limited lifetime, being a reference of either the input formula or flattered_formula_ , whose value may be overwritten at the next invocation of this method.
    Parameters
    formulathe formula to flatten.
    Returns
    a reference to the flattened formula.

Definition at line 16 of file LinearFormulaFlattener.cpp.

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