diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-08-19 23:06:57 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-19 16:06:57 -0500 |
| commit | 6710b082bc6fa8c7f67203a4013657e069479119 (patch) | |
| tree | 3f3ba1065e1100e86526a0b13ab26c759e77f1c2 /src/theory/arith/nl/poly_conversion.cpp | |
| parent | 31717bf7c014bf1971cabcc9b871de5818278126 (diff) | |
(cad solver) Add a partial check method. (#4904)
This PR extends the CAD-based solver to enable partial checks. Essentially, we only collect the first interval that is excluded for the first variable and return that one as a lemma. This does not leave a lot of choice on "how partial" the check should be, but it is fairly easy to implement and does not add additional overhead.
It also fixes some confusion in excluding_interval_to_lemma...
Diffstat (limited to 'src/theory/arith/nl/poly_conversion.cpp')
| -rw-r--r-- | src/theory/arith/nl/poly_conversion.cpp | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 8345fc5a1..e3bf4712d 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -360,17 +360,18 @@ Node excluding_interval_to_lemma(const Node& variable, if (is_algebraic_number(lv)) { return nm->mkNode( - Kind::AND, + Kind::OR, nm->mkNode( - Kind::GT, variable, nm->mkConst(poly_utils::toRationalBelow(lv))), - nm->mkNode(Kind::LT, + Kind::LT, variable, nm->mkConst(poly_utils::toRationalBelow(lv))), + nm->mkNode(Kind::GT, variable, nm->mkConst(poly_utils::toRationalAbove(lv)))); } else { - return nm->mkNode( - Kind::EQUAL, variable, nm->mkConst(poly_utils::toRationalBelow(lv))); + return nm->mkNode(Kind::DISTINCT, + variable, + nm->mkConst(poly_utils::toRationalBelow(lv))); } } if (li) @@ -384,7 +385,7 @@ Node excluding_interval_to_lemma(const Node& variable, Kind::LT, variable, nm->mkConst(poly_utils::toRationalBelow(lv))); } return nm->mkNode( - Kind::AND, + Kind::OR, nm->mkNode( Kind::GT, variable, nm->mkConst(poly_utils::toRationalAbove(uv))), nm->mkNode( |