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.

4 files changed, 11 insertions, 8 deletions

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);
       }
     }
   }