From: Gereon Kremer Date: Wed, 23 Feb 2022 17:29:18 +0000 (+0100) Subject: Fix icp candidate parsing (#8137) X-Git-Tag: cvc5-1.0.0~399 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=659068a3b3ba4bc9fed9a53ee5e1cf06e66d8df5;p=cvc5.git Fix icp candidate parsing (#8137) For constraints of the form c * x ~ poly(x) where c != 1 we would sometimes forget to take the inverse of c when parsing the assertion to the internal representation of the ICP solver. This PR fixes this issue, and does a few more changes: --nl-icp is really not well-tested and disabled by default. We make it an expert option. we no longer issue the propagation lemmas if we already found a conflict the nl-icp trace was heavily polluted by output from the interval utils, which are now moved to a new nl-icp-debug trace Fixes #8135. --- diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 5e6796864..5ec842f1a 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -568,7 +568,7 @@ name = "Arithmetic Theory" [[option]] name = "nlICP" - category = "regular" + category = "expert" long = "nl-icp" type = "bool" default = "false" diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index aab63325e..1c28b5569 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -127,13 +127,12 @@ std::vector ICPSolver::constructCandidates(const Node& n) } poly::Rational rhsmult; poly::Polynomial rhs = as_poly_polynomial(val, d_mapper, rhsmult); - rhsmult = poly::Rational(1) / rhsmult; // only correct up to a constant (denominator is thrown away!) if (!veq_c.isNull()) { rhsmult = poly_utils::toRational(veq_c.getConst()); } - Candidate res{lhs, rel, rhs, rhsmult, n, collectVariables(val)}; + Candidate res{lhs, rel, rhs, poly::inverse(rhsmult), n, collectVariables(val)}; Trace("nl-icp") << "\tAdded " << res << " from " << n << std::endl; result.emplace_back(res); } @@ -153,12 +152,11 @@ std::vector ICPSolver::constructCandidates(const Node& n) } poly::Rational rhsmult; poly::Polynomial rhs = as_poly_polynomial(val, d_mapper, rhsmult); - rhsmult = poly::Rational(1) / rhsmult; if (!veq_c.isNull()) { rhsmult = poly_utils::toRational(veq_c.getConst()); } - Candidate res{lhs, rel, rhs, rhsmult, n, collectVariables(val)}; + Candidate res{lhs, rel, rhs, poly::inverse(rhsmult), n, collectVariables(val)}; Trace("nl-icp") << "\tAdded " << res << " from " << n << std::endl; result.emplace_back(res); } @@ -357,9 +355,7 @@ void ICPSolver::check() } d_im.addPendingLemma(NodeManager::currentNM()->mkOr(mis), InferenceId::ARITH_NL_ICP_CONFLICT); - did_progress = true; - progress = false; - break; + return; } } while (progress); if (did_progress) diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp index 4814fb300..db1bee5c7 100644 --- a/src/theory/arith/nl/icp/intersection.cpp +++ b/src/theory/arith/nl/icp/intersection.cpp @@ -35,13 +35,13 @@ PropagationResult intersect_interval_with(poly::Interval& cur, const poly::Interval& res, std::size_t size_threshold) { - Trace("nl-icp") << cur << " := " << cur << " intersected with " << res + Trace("nl-icp-debug") << cur << " := " << cur << " intersected with " << res << std::endl; if (bitsize(get_lower(res)) > size_threshold || bitsize(get_upper(res)) > size_threshold) { - Trace("nl-icp") << "Reached bitsize threshold" << std::endl; + Trace("nl-icp-debug") << "Reached bitsize threshold" << std::endl; return PropagationResult::NOT_CHANGED; } @@ -52,7 +52,7 @@ PropagationResult intersect_interval_with(poly::Interval& cur, if (get_upper(res) < get_lower(cur)) { // upper(res) at 1 - Trace("nl-icp") << "res < cur -> conflict" << std::endl; + Trace("nl-icp-debug") << "res < cur -> conflict" << std::endl; return PropagationResult::CONFLICT; } if (get_upper(res) == get_lower(cur)) @@ -60,13 +60,13 @@ PropagationResult intersect_interval_with(poly::Interval& cur, // upper(res) at 2 if (get_upper_open(res) || get_lower_open(cur)) { - Trace("nl-icp") << "meet at lower, but one is open -> conflict" + Trace("nl-icp-debug") << "meet at lower, but one is open -> conflict" << std::endl; return PropagationResult::CONFLICT; } if (!is_point(cur)) { - Trace("nl-icp") << "contracts to point interval at lower" << std::endl; + Trace("nl-icp-debug") << "contracts to point interval at lower" << std::endl; cur = poly::Interval(get_upper(res)); return PropagationResult::CONTRACTED; } @@ -80,14 +80,14 @@ PropagationResult intersect_interval_with(poly::Interval& cur, if (get_lower(res) < get_lower(cur)) { // lower(res) at 1 - Trace("nl-icp") << "lower(cur) .. upper(res)" << std::endl; + Trace("nl-icp-debug") << "lower(cur) .. upper(res)" << std::endl; cur.set_upper(get_upper(res), get_upper_open(res)); return PropagationResult::CONTRACTED; } if (get_lower(res) == get_lower(cur)) { // lower(res) at 2 - Trace("nl-icp") << "meet at lower, lower(cur) .. upper(res)" << std::endl; + Trace("nl-icp-debug") << "meet at lower, lower(cur) .. upper(res)" << std::endl; cur = poly::Interval(get_lower(cur), get_lower_open(cur) || get_lower_open(res), get_upper(res), @@ -101,7 +101,7 @@ PropagationResult intersect_interval_with(poly::Interval& cur, Assert(get_lower(res) > get_lower(cur)) << "Comparison operator does weird stuff."; // lower(res) at 3 - Trace("nl-icp") << "cur covers res" << std::endl; + Trace("nl-icp-debug") << "cur covers res" << std::endl; cur = res; return PropagationResult::CONTRACTED_WITHOUT_CURRENT; } @@ -111,7 +111,7 @@ PropagationResult intersect_interval_with(poly::Interval& cur, if (get_lower(res) < get_lower(cur)) { // lower(res) at 1 - Trace("nl-icp") << "res covers cur but meet at upper" << std::endl; + Trace("nl-icp-debug") << "res covers cur but meet at upper" << std::endl; if (get_upper_open(res) && !get_upper_open(cur)) { cur.set_upper(get_upper(cur), true); @@ -122,7 +122,7 @@ PropagationResult intersect_interval_with(poly::Interval& cur, if (get_lower(res) == get_lower(cur)) { // lower(res) at 2 - Trace("nl-icp") << "same bounds but check openness" << std::endl; + Trace("nl-icp-debug") << "same bounds but check openness" << std::endl; bool changed = false; if (get_lower_open(res) && !get_lower_open(cur)) { @@ -148,7 +148,7 @@ PropagationResult intersect_interval_with(poly::Interval& cur, Assert(get_lower(res) > get_lower(cur)) << "Comparison operator does weird stuff."; // lower(res) at 3 - Trace("nl-icp") << "cur covers res but meet at upper" << std::endl; + Trace("nl-icp-debug") << "cur covers res but meet at upper" << std::endl; cur = poly::Interval(get_lower(res), get_lower_open(res), get_upper(res), @@ -167,13 +167,13 @@ PropagationResult intersect_interval_with(poly::Interval& cur, if (get_lower(res) < get_lower(cur)) { // lower(res) at 1 - Trace("nl-icp") << "res covers cur" << std::endl; + Trace("nl-icp-debug") << "res covers cur" << std::endl; return PropagationResult::NOT_CHANGED; } if (get_lower(res) == get_lower(cur)) { // lower(res) at 2 - Trace("nl-icp") << "res covers cur but meet at lower" << std::endl; + Trace("nl-icp-debug") << "res covers cur but meet at lower" << std::endl; if (get_lower_open(res) && is_point(cur)) { return PropagationResult::CONFLICT; @@ -190,7 +190,7 @@ PropagationResult intersect_interval_with(poly::Interval& cur, if (get_lower(res) < get_upper(cur)) { // lower(res) at 3 - Trace("nl-icp") << "lower(res) .. upper(cur)" << std::endl; + Trace("nl-icp-debug") << "lower(res) .. upper(cur)" << std::endl; cur.set_lower(get_lower(res), get_lower_open(res)); return PropagationResult::CONTRACTED; } @@ -199,13 +199,13 @@ PropagationResult intersect_interval_with(poly::Interval& cur, // lower(res) at 4 if (get_lower_open(res) || get_upper_open(cur)) { - Trace("nl-icp") << "meet at upper, but one is open -> conflict" + Trace("nl-icp-debug") << "meet at upper, but one is open -> conflict" << std::endl; return PropagationResult::CONFLICT; } if (!is_point(cur)) { - Trace("nl-icp") << "contracts to point interval at upper" << std::endl; + Trace("nl-icp-debug") << "contracts to point interval at upper" << std::endl; cur = poly::Interval(get_lower(res)); return PropagationResult::CONTRACTED; } @@ -214,7 +214,7 @@ PropagationResult intersect_interval_with(poly::Interval& cur, Assert(get_lower(res) > get_upper(cur)); // lower(res) at 5 - Trace("nl-icp") << "res > cur -> conflict" << std::endl; + Trace("nl-icp-debug") << "res > cur -> conflict" << std::endl; return PropagationResult::CONFLICT; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 74c163503..7e1935bc9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -765,6 +765,7 @@ set(regress_0_tests regress0/nl/issue5737-div00.smt2 regress0/nl/issue5740-mod00.smt2 regress0/nl/issue5740-2-mod00.smt2 + regress0/nl/issue8135-icp-candidates.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 regress0/nl/nia-wrong-tl.smt2 diff --git a/test/regress/regress0/nl/issue8135-icp-candidates.smt2 b/test/regress/regress0/nl/issue8135-icp-candidates.smt2 new file mode 100644 index 000000000..0d370539e --- /dev/null +++ b/test/regress/regress0/nl/issue8135-icp-candidates.smt2 @@ -0,0 +1,7 @@ +; REQUIRES: poly +; COMMAND-LINE: --nl-icp +; EXPECT: sat +(set-logic QF_NIA) +(declare-const a Int) +(assert (> (- a) (* (+ a a) (+ a 1)))) +(check-sat)