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
16namespace dlinear {
17
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
Simple dataclass used to store the configuration of the program.
Definition Config.h:38
Used by the PredicateAbstractor to ensure that all the theory literals are in the flattened standard ...
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...
LinearFormulaFlattener(const Config &config)
Construct a new LinearFormulaFlattener object with the given config.
const Config & config_
Configuration.
Formula Flatten(const Formula &formula)
Flatten the given formula.
std::unordered_map< Formula, Formula > flattened_formulas_
Cache for the flattered formulas.
Represents a symbolic form of an expression.
Represents a symbolic form of a first-order logic formula.
Global namespace for the dlinear library.