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).

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 46135f12a5303d65e4111dba0b66dfe998257cd3..f3e0d0bd6d16cff26f2de6a19d888274aca39e27 100644 (file)
--- 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 dc59cbbf586631861265de0707b19def57f696e7..e771f8bb81c64fcf51ae445f43b2c6656f740b58 100644 (file)
--- 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 9ebf125775e914b71901dc9cb5bd39539f09813e..3b68a33ca2acd561131fbc0c5d43c4487cf8ad09 100644 (file)
--- 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;
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cb37b428ec943db5774628a80e2d1c13590c40c7..af238db1839bfa9749d008e8c6f00fb79c67e849 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1616,6 +1616,7 @@ set(regress_1_tests
   regress1/quantifiers/issue5469-aext.smt2
   regress1/quantifiers/issue5470-aext.smt2
   regress1/quantifiers/issue5471-aext.smt2
+  regress1/quantifiers/issue5482-rtf-no-fv.smt2
   regress1/quantifiers/issue5484-qe.smt2
   regress1/quantifiers/issue5484b-qe.smt2
   regress1/quantifiers/issue993.smt2

diff --git a/test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2 b/test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2
new file mode 100644 (file)
index 0000000..b1e6911
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5482-rtf-no-fv.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: unsat
+(set-logic AUFNIA)
+(declare-fun a () Int)
+(declare-fun b () (Array Int Int))
+(declare-fun c () (Array Int Int))
+(declare-fun d () Int)
+(assert
+ (exists ((e Int))
+ (and (<= e 0)
+  (exists ((f Int))
+  (and (<= 0 f e)
+   (> (select (store b 0 (select c (div a d))) f)
+   (select (store b 0 (select c (div a d))) e)))))))
+(check-sat)