dlinear
0.0.1
Delta-complete SMT solver for linear programming
Loading...
Searching...
No Matches
LinearFormulaFlattener.h
1
11
#pragma once
12
13
#include "dlinear/symbolic/symbolic.h"
14
#include "dlinear/util/Config.h"
15
16
namespace
dlinear
{
17
22
class
LinearFormulaFlattener
{
23
public
:
28
explicit
LinearFormulaFlattener
(
const
Config
& config) :
config_
{config},
flattened_formulas_
{} {}
42
[[nodiscard]]
Formula
Flatten
(
const
Formula
& formula);
43
44
private
:
59
[[nodiscard]]
Formula
BuildFlatteredFormula
(
const
Expression
& lhs,
const
Expression
& rhs, FormulaKind kind)
const
;
60
61
const
Config
&
config_
;
62
std::unordered_map<Formula, Formula>
flattened_formulas_
;
63
};
64
65
}
// namespace dlinear
dlinear::Config
Simple dataclass used to store the configuration of the program.
Definition
Config.h:38
dlinear::LinearFormulaFlattener
Used by the PredicateAbstractor to ensure that all the theory literals are in the flattened standard ...
Definition
LinearFormulaFlattener.h:22
dlinear::LinearFormulaFlattener::BuildFlatteredFormula
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-h...
Definition
LinearFormulaFlattener.cpp:37
dlinear::LinearFormulaFlattener::LinearFormulaFlattener
LinearFormulaFlattener(const Config &config)
Construct a new LinearFormulaFlattener object with the given config.
Definition
LinearFormulaFlattener.h:28
dlinear::LinearFormulaFlattener::config_
const Config & config_
Configuration.
Definition
LinearFormulaFlattener.h:61
dlinear::LinearFormulaFlattener::Flatten
Formula Flatten(const Formula &formula)
Flatten the given formula.
Definition
LinearFormulaFlattener.cpp:16
dlinear::LinearFormulaFlattener::flattened_formulas_
std::unordered_map< Formula, Formula > flattened_formulas_
Cache for the flattered formulas.
Definition
LinearFormulaFlattener.h:62
dlinear::drake::symbolic::Expression
Represents a symbolic form of an expression.
Definition
symbolic_expression.h:162
dlinear::drake::symbolic::Formula
Represents a symbolic form of a first-order logic formula.
Definition
symbolic_formula.h:100
dlinear
Global namespace for the dlinear library.
dlinear
symbolic
LinearFormulaFlattener.h
Generated by
1.11.0