Fix remove term formula policy for terms beneath quantifiers (#5497)

Now that extended arithmetic symbols are not eliminated during expandDefinitions, this allowed for a chain of events that would not apply theory preprocessing on certain terms.

In particular, a term t would not have theory preprocessing applied to it if it was a strict subterm of ITE-term s that occurred in a term position in a quantified formula body, and s did not have free variables. In this case, term formula removal would add a lemma corresponding to the ITE skolem definition, whose subterms did not have theory preprocessing applied. This meant that a (div a d) term was not being preprocessed in #5482, leading to solution unsoundness.

This changes the policy in term formula removal to be in sync with theory preprocessing: term formula removal and theory preprocessing only apply to terms that are not beneath quantifiers. In particular, this means that ground terms in quantifier bodies are left untouched until they are introduced e.g. by instantiation.

This fixes the solution soundness issue (fixes #5482).

3 files changed, 18 insertions, 8 deletions

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 46135f12a..f3e0d0bd6 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -200,9 +200,11 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
   // in the "non-variable Boolean term within term" case below.
   if (node.getKind() == kind::ITE && !nodeType.isBoolean())
   {
-    // Here, we eliminate the ITE if we are not Boolean and if we do not contain
-    // a free variable.
-    if (!inQuant || !expr::hasFreeVar(node))
+    // Here, we eliminate the ITE if we are not Boolean and if we are
+    // not in a quantified formula. This policy should be in sync with
+    // the policy for when to apply theory preprocessing to terms, see PR
+    // #5497.
+    if (!inQuant)
     {
       skolem = getSkolemForNode(node);
       if (skolem.isNull())
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index dc59cbbf5..e771f8bb8 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -24,7 +24,6 @@
 #include "expr/attribute.h"
 #include "expr/lazy_proof.h"
 #include "expr/node.h"
-#include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
 #include "expr/node_visitor.h"
 #include "options/bv_options.h"
@@ -1171,19 +1170,21 @@ Node TheoryEngine::getModelValue(TNode var) {
 
 
 Node TheoryEngine::ensureLiteral(TNode n) {
-  Debug("ensureLiteral") << "rewriting: " << n << std::endl;
+  Trace("ensureLiteral") << "ensureLiteral rewriting: " << n << std::endl;
   Node rewritten = Rewriter::rewrite(n);
-  Debug("ensureLiteral") << "      got: " << rewritten << std::endl;
+  Trace("ensureLiteral") << "  got: " << rewritten << std::endl;
   std::vector<TrustNode> newLemmas;
   std::vector<Node> newSkolems;
   TrustNode tpn = d_tpp.preprocess(n, newLemmas, newSkolems, true);
   // send lemmas corresponding to the skolems introduced by preprocessing n
   for (const TrustNode& tnl : newLemmas)
   {
+    Trace("ensureLiteral") << "  lemma: " << tnl.getNode() << std::endl;
     lemma(tnl, LemmaProperty::NONE);
   }
   Node preprocessed = tpn.isNull() ? rewritten : tpn.getNode();
-  Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl;
+  Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed
+                         << std::endl;
   d_propEngine->ensureLiteral(preprocessed);
   return preprocessed;
 }
@@ -1400,6 +1401,7 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
   // get the node
   Node node = tlemma.getNode();
   Node lemma = tlemma.getProven();
+  Trace("te-lemma") << "Lemma, input: " << lemma << std::endl;
 
   Assert(!expr::hasFreeVar(lemma));
 
@@ -1528,9 +1530,12 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
   }
 
   // now, send the lemmas to the prop engine
+  Trace("te-lemma") << "Lemma, output: " << tlemma.getProven() << std::endl;
   d_propEngine->assertLemma(tlemma.getProven(), false, removable);
   for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
   {
+    Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven()
+                      << std::endl;
     d_propEngine->assertLemma(newLemmas[i].getProven(), false, removable);
   }
 
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 9ebf12577..3b68a33ca 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -139,6 +139,8 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   }
   if (node == retNode)
   {
+    Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change"
+                       << std::endl;
     // no change
     Assert(newLemmas.empty());
     return TrustNode::null();
@@ -217,7 +219,8 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
     Assert(!isProofEnabled() || newLemmas[i].getGenerator() != nullptr);
     newLemmas[i].debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_new");
   }
-  Trace("tpp-debug") << "Preprocessed: " << node << " " << retNode << std::endl;
+  Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
+                     << tret.getNode() << std::endl;
   return tret;
 }