From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 14 Mar 2022 16:56:52 +0000 (-0500)
Subject: Run preprocess rewrite on equalities until fixed point (#8291)
X-Git-Tag: cvc5-1.0.0~264
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8699e3e95075e262852b57ea9a298648d5caa26c;p=cvc5.git

Run preprocess rewrite on equalities until fixed point (#8291)

Previously we were only running once, while strings assumed this was run on what it returned.

This should significantly improve our performance on the benchmarks from SMT-LIB that involving looping word equations.
---

diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp
index 93ba2b7cd..782d4569d 100644
--- a/src/preprocessing/passes/theory_rewrite_eq.cpp
+++ b/src/preprocessing/passes/theory_rewrite_eq.cpp
@@ -50,6 +50,7 @@ TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
   NodeManager* nm = NodeManager::currentNM();
   TheoryEngine* te = d_preprocContext->getTheoryEngine();
   std::unordered_map<TNode, Node> visited;
+  std::unordered_map<TNode, Node> rewrittenTo;
   std::unordered_map<TNode, Node>::iterator it;
   std::vector<TNode> visit;
   TNode cur;
@@ -57,24 +58,32 @@ TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
   do
   {
     cur = visit.back();
-    visit.pop_back();
     it = visited.find(cur);
 
     if (it == visited.end())
     {
       if (cur.getNumChildren()==0)
       {
+        visit.pop_back();
         visited[cur] = cur;
       }
       else
       {
         visited[cur] = Node::null();
-        visit.push_back(cur);
         visit.insert(visit.end(), cur.begin(), cur.end());
       }
     }
     else if (it->second.isNull())
     {
+      it = rewrittenTo.find(cur);
+      if (it != rewrittenTo.end())
+      {
+        // rewritten form is the rewritten form of what it was rewritten to
+        Assert(visited.find(it->second) != visited.end());
+        visited[cur] = visited[it->second];
+        visit.pop_back();
+        continue;
+      }
       Node ret = cur;
       bool childChanged = false;
       std::vector<Node> children;
@@ -94,14 +103,32 @@ TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
       {
         ret = nm->mkNode(cur.getKind(), children);
       }
+      bool wasRewritten = false;
       if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean())
       {
         // For example, (= x y) ---> (and (>= x y) (<= x y))
         TrustNode trn = te->ppRewriteEquality(ret);
         // can make proof producing by using proof generator from trn
-        ret = trn.isNull() ? Node(ret) : trn.getNode();
+        if (!trn.isNull() && trn.getNode() != ret)
+        {
+          Trace("pp-rewrite-eq") << "Rewrite equality " << ret << " to "
+                                 << trn.getNode() << std::endl;
+          wasRewritten = true;
+          Node retr = trn.getNode();
+          rewrittenTo[cur] = retr;
+          rewrittenTo[ret] = retr;
+          visit.push_back(retr);
+        }
+      }
+      if (!wasRewritten)
+      {
+        visit.pop_back();
+        visited[cur] = ret;
       }
-      visited[cur] = ret;
+    }
+    else
+    {
+      visit.pop_back();
     }
   } while (!visit.empty());
   Assert(visited.find(n) != visited.end());
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6b73f506e..ba1ebb1af 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1379,6 +1379,8 @@ set(regress_0_tests
   regress0/strings/proj-issue316-regexp-ite.smt2
   regress0/strings/proj-issue390-update-rev-rewrite.smt2
   regress0/strings/proj-issue409-re-loop-none.smt2
+  regress0/strings/quad-028-2-2-unsat.smt2
+  regress0/strings/quad-138-4-2-unsat.smt2
   regress0/strings/re_diff.smt2
   regress0/strings/re-in-rewrite.smt2
   regress0/strings/re-syntax.smt2
@@ -3032,8 +3034,6 @@ set(regression_disabled_tests
   regress0/bv/test00.smtv1.smt2
   # timeout after fixing upwards closure for relations
   regress0/rels/rel_tc_7.cvc.smt2
-  # timeout after changes to equality rewriting policy in strings
-  regress0/strings/quad-028-2-2-unsat.smt2
   # FIXME #1649
   regress0/datatypes/datatype-dump.cvc.smt2
   # no longer support overloaded symbols across multiple parametric datatypes
diff --git a/test/regress/regress0/strings/quad-138-4-2-unsat.smt2 b/test/regress/regress0/strings/quad-138-4-2-unsat.smt2
new file mode 100644
index 000000000..249ae2639
--- /dev/null
+++ b/test/regress/regress0/strings/quad-138-4-2-unsat.smt2
@@ -0,0 +1,11 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun  x1 () String )
+(declare-fun  x2 () String )
+(declare-fun  z1 () String )
+(declare-fun  z2 () String )
+(declare-fun  t1 () String )
+(declare-fun  t2 () String )
+(assert ( =( str.++( str.++( str.++( str.++ x1  "abdc"  )  x2  ) ( str.++ "ac"  z1  )  ) ( str.++( str.++ "cd"  z2  )  t2  )  ) ( str.++( str.++( str.++( str.++ x2  "dcba"  )  x1  ) ( str.++ z1  "ba"  )  ) ( str.++( str.++ z2  "dc"  )  t1  )  )  ) )
+(check-sat)