Updates to theory preprocess equality (#5776)

This makes 3 changes related to arithmetic preprocessing of equalities which revert to the original behavior of master before a129c57.

For background, the commit a129c57 unintentionally changed the default behavior slightly in 3 ways (each corrected in this PR), which led a performance regression on QF_LIA in current master.

The 3 fixes are:
(1) Rewrite equalities should be applied as a post-rewrite, not a pre-rewrite in the theory-rewrite-eq preprocessing pass. This is particularly important for equalities between ITE terms that contain other equalities recursively.
(2) theory-rewrite-eq should apply after rewriting and just before the normal theory preprocessing.
(3) The arith-brab test should call ppRewrite on the arithmetic equality it introduces, as it has a choice of whether to eliminate the equality before the lemma is sent out.

diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp
index 190b336842d210da066c040702301955bdfe7131..68de75194145d71609014f8275f2f46cdfd71c85 100644 (file)
--- a/src/preprocessing/passes/theory_rewrite_eq.cpp
+++ b/src/preprocessing/passes/theory_rewrite_eq.cpp
@@ -59,13 +59,9 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
 
     if (it == visited.end())
     {
-      // don't consider Boolean equality
-      if (cur.getKind() == kind::EQUAL && !cur[0].getType().isBoolean())
+      if (cur.getNumChildren()==0)
       {
-        // For example, (= x y) ---> (and (>= x y) (<= x y))
-        theory::TrustNode trn = te->ppRewriteEquality(cur);
-        // can make proof producing by using proof generator from trn
-        visited[cur] = trn.isNull() ? Node(cur) : trn.getNode();
+        visited[cur] = cur;
       }
       else
       {
@@ -95,6 +91,13 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
       {
         ret = nm->mkNode(cur.getKind(), children);
       }
+      if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean())
+      {
+        // For example, (= x y) ---> (and (>= x y) (<= x y))
+        theory::TrustNode trn = te->ppRewriteEquality(ret);
+        // can make proof producing by using proof generator from trn
+        ret = trn.isNull() ? Node(ret) : trn.getNode();
+      }
       visited[cur] = ret;
     }
   } while (!visit.empty());

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 0bbc2eeae868e257c220f436163f74b1655c9bba..6d6c81e3cbc5b52742510ad4cc877e0dad3e497b 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -317,10 +317,7 @@ bool ProcessAssertions::apply(Assertions& as)
   {
     d_passes["ho-elim"]->apply(&assertions);
   }
-
-  // rewrite equalities based on theory-specific rewriting
-  d_passes["theory-rewrite-eq"]->apply(&assertions);
-
+  
   // begin: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 
@@ -332,6 +329,8 @@ bool ProcessAssertions::apply(Assertions& as)
 
   // ensure rewritten
   d_passes["rewrite"]->apply(&assertions);
+  // rewrite equalities based on theory-specific rewriting
+  d_passes["theory-rewrite-eq"]->apply(&assertions);
   // apply theory preprocess, which includes ITE removal
   d_passes["theory-preprocess"]->apply(&assertions);
   // This is needed because when solving incrementally, removeITEs may

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index d1068c6acfa996d5f9de0e19afa706a6e96ea4c9..7b0096f3079187a52b454e6e3f93736d63ed16a2 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3694,6 +3694,13 @@ Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const {
     lem = nm->mkNode(kind::OR, ub, lb);
     Node eq = Rewriter::rewrite(
         nm->mkNode(kind::EQUAL, var, mkRationalNode(nearest)));
+    // Also preprocess it before we send it out. This is important since
+    // arithmetic may prefer eliminating equalities.
+    if (Theory::theoryOf(eq) == THEORY_ARITH)
+    {
+      TrustNode teq = d_containing.ppRewrite(eq);
+      eq = teq.isNull() ? eq : teq.getNode();
+    }
     Node literal = d_containing.getValuation().ensureLiteral(eq);
     d_containing.getOutputChannel().requirePhase(literal, true);
     lem = nm->mkNode(kind::OR, literal, lem);

diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index cb346d02d980324c208c75fc29543fbb02a14ce0..0aa56a381db75dc09a5f651af6f2fd7a3b3535b5 100644 (file)
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -69,7 +69,7 @@ void EngineOutputChannel::safePoint(ResourceManager::Resource r)
 
 theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
 {
-  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
+  Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
                          << lemma << ")"
                          << ", properties = " << p << std::endl;
   ++d_statistics.lemmas;
@@ -86,12 +86,12 @@ theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
 
 theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
 {
-  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
+  Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
                          << lemma << ")" << std::endl;
   ++d_statistics.lemmas;
   d_engine->d_outputChannelUsed = true;
 
-  Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )"
+  Trace("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )"
                        << std::endl;
   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
   LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE;
@@ -101,7 +101,7 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
 
 bool EngineOutputChannel::propagate(TNode literal)
 {
-  Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
+  Trace("theory::propagate") << "EngineOutputChannel<" << d_theory
                              << ">::propagate(" << literal << ")" << std::endl;
   ++d_statistics.propagations;
   d_engine->d_outputChannelUsed = true;
@@ -134,7 +134,7 @@ void EngineOutputChannel::demandRestart()
 
 void EngineOutputChannel::requirePhase(TNode n, bool phase)
 {
-  Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase
+  Trace("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase
                   << ")" << std::endl;
   ++d_statistics.requirePhase;
   d_engine->getPropEngine()->requirePhase(n, phase);
@@ -174,7 +174,7 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf)
 
 LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
 {
-  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
+  Trace("theory::lemma") << "EngineOutputChannel<" << d_theory
                          << ">::trustedLemma(" << plem << ")" << std::endl;
   Assert(plem.getKind() == TrustNodeKind::LEMMA);
   if (plem.getGenerator() != nullptr)