From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 7 Oct 2020 14:13:41 +0000 (+0200)
Subject: Make sure conflicts are not rewritten (in arithmetic) (#5219)
X-Git-Tag: cvc5-1.0.0~2741
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eb4321c5040258ac1ac41eb955aa5b6b5199011e;p=cvc5.git

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 5a1c30966..7cae40bbb 100644
--- 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 d984e09f2..a0dc19d81 100644
--- 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 77f042d4d..656b5ed0d 100644
--- 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 43905d802..7f97d51b6 100644
--- 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 5d4501309..cc5c911ff 100644
--- 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
index 000000000..3c8a949ad
--- /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)