Improve accuracy of stats for sygus sampler (#1755)

1 files changed, 4 insertions, 17 deletions

diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index cb7379910..00e527aba 100644
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -31,39 +31,26 @@ DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe)
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 }
 
-bool DynamicRewriter::addRewrite(Node a, Node b)
+void DynamicRewriter::addRewrite(Node a, Node b)
 {
   Trace("dyn-rewrite") << "Dyn-Rewriter : " << a << " == " << b << std::endl;
   if (a == b)
   {
-    Trace("dyn-rewrite") << "...fail, equal." << std::endl;
-    return false;
+    Trace("dyn-rewrite") << "...equal." << std::endl;
+    return;
   }
 
   // add to the equality engine
   Node ai = toInternal(a);
   Node bi = toInternal(b);
   Trace("dyn-rewrite-debug") << "Internal : " << ai << " " << bi << std::endl;
-  d_equalityEngine.addTerm(ai);
-  d_equalityEngine.addTerm(bi);
-
-  Trace("dyn-rewrite-debug") << "get reps..." << std::endl;
-  // may already be equal by congruence
-  Node air = d_equalityEngine.getRepresentative(ai);
-  Node bir = d_equalityEngine.getRepresentative(bi);
-  Trace("dyn-rewrite-debug") << "Reps : " << air << " " << bir << std::endl;
-  if (air == bir)
-  {
-    Trace("dyn-rewrite") << "...fail, congruent." << std::endl;
-    return false;
-  }
 
   Trace("dyn-rewrite-debug") << "assert eq..." << std::endl;
   Node eq = ai.eqNode(bi);
   d_rewrites.push_back(eq);
   d_equalityEngine.assertEquality(eq, true, eq);
+  Assert(d_equalityEngine.consistent());
   Trace("dyn-rewrite-debug") << "Finished" << std::endl;
-  return true;
 }
 
 bool DynamicRewriter::areEqual(Node a, Node b)