Make sure conflicts are not rewritten (in arithmetic) (#5219)

The arithmetic inference manager did rewrite conflicts, which lead to nodes from the conflict not being assumptions (but rewritten assumptions) triggering an assertion. This rewrite is now removed.
Furthermore rewrites triggering the same assertion within the icp subsolver have been refactored to avoid this issue.

diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp
index 5a1c3096600581043df49bf145d26311330580e7..7cae40bbb9dd1b594b806f42a0a3d4d211d26ff6 100644 (file)
--- a/src/theory/arith/bound_inference.cpp
+++ b/src/theory/arith/bound_inference.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/bound_inference.h"
 
 #include "theory/arith/normal_form.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
@@ -95,7 +96,7 @@ const std::map<Node, Bounds>& BoundInference::get() const { return d_bounds; }
 bool BoundInference::add(const Node& n)
 {
   // Parse the node as a comparison
-  auto comp = Comparison::parseNormalForm(n);
+  auto comp = Comparison::parseNormalForm(Rewriter::rewrite(n));
   auto dec = comp.decompose(true);
   if (std::get<0>(dec).isVariable())
   {

diff --git a/src/theory/arith/inference_id.cpp b/src/theory/arith/inference_id.cpp
index d984e09f28e8bcd5440836a19ebe99a6676bd2f9..a0dc19d81f6216b6d8ff30ae57d898712fe5039d 100644 (file)
--- a/src/theory/arith/inference_id.cpp
+++ b/src/theory/arith/inference_id.cpp
@@ -42,6 +42,8 @@ const char* toString(InferenceId i)
     case InferenceId::NL_IAND_VALUE_REFINE: return "IAND_VALUE_REFINE";
     case InferenceId::NL_CAD_CONFLICT: return "CAD_CONFLICT";
     case InferenceId::NL_CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL";
+    case InferenceId::NL_ICP_CONFLICT: return "ICP_CONFLICT";
+    case InferenceId::NL_ICP_PROPAGATION: return "ICP_PROPAGATION";
     default: return "?";
   }
 }

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 77f042d4df732a53fcf51cd6ad15528e43a241b5..656b5ed0dde8c9d46011015808a43536075c3b9e 100644 (file)
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -95,7 +95,7 @@ void InferenceManager::addConflict(const Node& conf, InferenceId inftype)
 {
   Trace("arith::infman") << "Adding conflict: " << inftype << " " << conf
                          << std::endl;
-  conflict(Rewriter::rewrite(conf));
+  conflict(conf);
 }
 
 bool InferenceManager::hasUsed() const

diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index 43905d802c98cfa1f5432b7e2bf0e9e8e0526ee2..7f97d51b6e5d3d7f29e6729b0321fe94ae08f437 100644 (file)
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -77,7 +77,8 @@ std::vector<Node> ICPSolver::collectVariables(const Node& n) const
 
 std::vector<Candidate> ICPSolver::constructCandidates(const Node& n)
 {
-  auto comp = Comparison::parseNormalForm(n).decompose(false);
+  auto comp =
+      Comparison::parseNormalForm(Rewriter::rewrite(n)).decompose(false);
   Kind k = std::get<1>(comp);
   if (k == Kind::DISTINCT)
   {
@@ -305,13 +306,12 @@ void ICPSolver::reset(const std::vector<Node>& assertions)
   d_state.reset();
   for (const auto& n : assertions)
   {
-    Node tmp = Rewriter::rewrite(n);
-    Trace("nl-icp") << "Adding " << tmp << std::endl;
-    if (tmp.getKind() != Kind::CONST_BOOLEAN)
+    Trace("nl-icp") << "Adding " << n << std::endl;
+    if (n.getKind() != Kind::CONST_BOOLEAN)
     {
-      if (!d_state.d_bounds.add(tmp))
+      if (!d_state.d_bounds.add(n))
       {
-        addCandidate(tmp);
+        addCandidate(n);
       }
     }
   }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5d4501309d42cbe7455b514d7049dde8c420b7b1..cc5c911ff40fb7ca9c126de5274ed64355e01461 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -49,6 +49,7 @@ set(regress_0_tests
   regress0/arith/issue3683.smt2
   regress0/arith/issue4367.smt2
   regress0/arith/issue4525.smt2
+  regress0/arith/issue5219-conflict-rewrite.smt2
   regress0/arith/ite-lift.smt2
   regress0/arith/leq.01.smtv1.smt2
   regress0/arith/miplib.cvc

diff --git a/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2
new file mode 100644 (file)
index 0000000..3c8a949
--- /dev/null
+++ b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2
@@ -0,0 +1,8 @@
+; REQUIRES: poly
+; COMMAND-LINE: --theoryof-mode=term --nl-ext --nl-icp
+; EXPECT: unknown
+(set-logic QF_NRA)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (and (< 1 y) (= y (+ x (* x x)))))
+(check-sat)