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 5e6796864d5d9301e739188a224cbc5c49e149e2..5ec842f1a3384cc225a73c4647d3edbbd82badd4 100644 (file)
--- 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 aab63325e3359a291c299bed86a683e4819b1a51..1c28b5569ee40058e702cc73fa148932a83e52be 100644 (file)
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -127,13 +127,12 @@ std::vector<Candidate> 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<Rational>());
       }
-      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<Candidate> 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<Rational>());
       }
-      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 4814fb3000a04d5e9e233cccd7d602283e49f933..db1bee5c7d0fa803d9bccaaf3bd01b2d516fa15d 100644 (file)
--- 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 74c16350390bb7d64c90ab85b8a53200b89dec89..7e1935bc9ebf7bbbb0cb137294764d3af4f642b4 100644 (file)
--- 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 (file)
index 0000000..0d37053
--- /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)