diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-20 14:03:04 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-20 14:03:04 -0500 |
commit | 03a11423f2c14c7806d1390094dbd6b47a99cefc (patch) | |
tree | 0a9b4783d72b35128064fae6d08633b4be868204 /src/theory/arith/nonlinear_extension.h | |
parent | 252cd598a389adbb309019883e9a48d091452612 (diff) |
Internally remove redundant assertions and infer equalities in NonLinearExtension (#1633)
Diffstat (limited to 'src/theory/arith/nonlinear_extension.h')
-rw-r--r-- | src/theory/arith/nonlinear_extension.h | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index a37ef97f8..96d37cbc2 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -245,6 +245,17 @@ class NonlinearExtension { void assignOrderIds(std::vector<Node>& vars, NodeMultiset& d_order, unsigned orderType); + /** get assertions + * + * Let M be the set of assertions known by THEORY_ARITH. This function adds a + * set of literals M' to assertions such that M' and M are equivalent. + * + * Examples of how M' differs with M: + * (1) M' may not include t < c (in M) if t < c' is in M' for c' < c, where + * c and c' are constants, + * (2) M' may contain t = c if both t >= c and t <= c are in M. + */ + void getAssertions(std::vector<Node>& assertions); /** check model * * Returns the subset of assertions whose concrete values we cannot show are @@ -700,7 +711,9 @@ private: * that occur in the current context. */ std::vector<Node> checkMonomialInferBounds( - std::vector<Node>& nt_lemmas, const std::vector<Node>& false_asserts); + std::vector<Node>& nt_lemmas, + const std::vector<Node>& asserts, + const std::vector<Node>& false_asserts); /** check factoring * @@ -714,7 +727,8 @@ private: * ...where k is fresh and x*z + y*z > t is a * constraint that occurs in the current context. */ - std::vector<Node> checkFactoring(const std::vector<Node>& false_asserts); + std::vector<Node> checkFactoring(const std::vector<Node>& asserts, + const std::vector<Node>& false_asserts); /** check monomial infer resolution bounds * |