Fix issues related to eliminating extended arithmetic operators (#5475)

This fixes 2 issues related to eliminating arithmetic operators:
(1) counterexample lemmas in CEGQI were not being preprocessed
(2) ensureLiteral was not doing term formula removal.
This corrects these two issues. Now ensureLiteral does full theory preprocessing on the term we are ensuring literal for, meaning this may trigger lemmas if the term contains extended arithmetic operators like div.

Fixes #5469, fixes #5470, fixes #5471.

This adds --sygus-inst to 2 of these benchmarks which moreover makes them solvable.

This also improves our assertions and trace messages.

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c77e64221b54aa85e4ac58b9cf00f1d032fb7da9..b5c0d1bd027c9e41f2e9ebe13c5a7ba857c31302 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -154,10 +154,15 @@ void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
   d_internal->ppStaticLearn(n, learned);
 }
 
-bool TheoryArith::preCheck(Effort level) { return d_internal->preCheck(level); }
+bool TheoryArith::preCheck(Effort level)
+{
+  Trace("arith-check") << "TheoryArith::preCheck " << level << std::endl;
+  return d_internal->preCheck(level);
+}
 
 void TheoryArith::postCheck(Effort level)
 {
+  Trace("arith-check") << "TheoryArith::postCheck " << level << std::endl;
   // check with the non-linear solver at last call
   if (level == Theory::EFFORT_LAST_CALL)
   {
@@ -191,6 +196,9 @@ void TheoryArith::postCheck(Effort level)
 bool TheoryArith::preNotifyFact(
     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 {
+  Trace("arith-check") << "TheoryArith::preNotifyFact: " << fact
+                       << ", isPrereg=" << isPrereg
+                       << ", isInternal=" << isInternal << std::endl;
   d_internal->preNotifyFact(atom, pol, fact);
   // We do not assert to the equality engine of arithmetic in the standard way,
   // hence we return "true" to indicate we are finished with this fact.

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 3bf3cc4259534ef25c4a915b36c7463d5a618293..561817aa8d48686c6a03b7a5511a3dfc4f987e69 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -603,7 +603,8 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
     ce_vars.push_back(tutil->getInstantiationConstant(q, i));
   }
   CegInstantiator* cinst = getInstantiator(q);
-  LemmaStatus status = d_quantEngine->getOutputChannel().lemma(lem);
+  LemmaStatus status =
+      d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
   Node ppLem = status.getRewrittenLemma();
   Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
                        << std::endl;

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 3a155b9ad3ce2407847360ef15f8af6a8788d8e6..d54538049d7dce345a226f5eafc982bdcc1c3770 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -312,6 +312,8 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
                       << std::endl;
       Assert(!expr::hasFreeVar(preprocessed));
+      // should not have witness
+      Assert(!expr::hasSubtermKind(kind::WITNESS, preprocessed));
 
       // Pre-register the terms in the atom
       theory::TheoryIdSet theories = NodeVisitor<PreRegisterVisitor>::run(
@@ -1172,8 +1174,15 @@ Node TheoryEngine::ensureLiteral(TNode n) {
   Debug("ensureLiteral") << "rewriting: " << n << std::endl;
   Node rewritten = Rewriter::rewrite(n);
   Debug("ensureLiteral") << "      got: " << rewritten << std::endl;
-  TrustNode tp = preprocess(rewritten);
-  Node preprocessed = tp.isNull() ? rewritten : tp.getNode();
+  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)
+  {
+    lemma(tnl, LemmaProperty::NONE);
+  }
+  Node preprocessed = tpn.isNull() ? rewritten : tpn.getNode();
   Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl;
   d_propEngine->ensureLiteral(preprocessed);
   return preprocessed;
@@ -1417,6 +1426,8 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
   Node node = tlemma.getNode();
   Node lemma = tlemma.getProven();
 
+  Assert(!expr::hasFreeVar(lemma));
+
   // when proofs are enabled, we ensure the trust node has a generator by
   // adding a trust step to the lazy proof maintained by this class
   if (isProofEnabled())

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 088e413bba630ba7754b1c7f02eda148b6563e6b..ee3611a5312ab68e5c33654a7ff7ce534c17f6c7 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -663,7 +663,9 @@ class TheoryEngine {
   Node getModelValue(TNode var);
 
   /**
-   * Takes a literal and returns an equivalent literal that is guaranteed to be a SAT literal
+   * Takes a literal and returns an equivalent literal that is guaranteed to be
+   * a SAT literal. This rewrites and preprocesses n, which notice may involve
+   * sending lemmas if preprocessing n involves introducing new skolems.
    */
   Node ensureLiteral(TNode n);
 
@@ -746,7 +748,6 @@ private:
    * This function is called from the smt engine's checkModel routine.
    */
   void checkTheoryAssertionsWithModel(bool hardFailure);
-
  private:
   IntStat d_arithSubstitutionsAdded;
 };/* class TheoryEngine */

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 42ac074ce5d5c51112c3e25c070e92aa15f9ec98..9ebf125775e914b71901dc9cb5bd39539f09813e 100644 (file)
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -89,9 +89,9 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
 {
   // In this method, all rewriting steps of node are stored in d_tpg.
 
-  Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: start " << node
-                           << ", doTheoryPreprocess=" << doTheoryPreprocess
-                           << std::endl;
+  Trace("tpp-debug") << "TheoryPreprocessor::preprocess: start " << node
+                     << ", doTheoryPreprocess=" << doTheoryPreprocess
+                     << std::endl;
   // Run theory preprocessing, maybe
   Node ppNode = node;
   if (doTheoryPreprocess)
@@ -121,23 +121,21 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   // in d_tpg, which maintains the fact that d_tpg can prove the rewrite.
   Node retNode = rewriteWithProof(rtfNode);
 
-  if (Trace.isOn("tpp-proof-debug"))
+  if (Trace.isOn("tpp-debug"))
   {
     if (node != ppNode)
     {
-      Trace("tpp-proof-debug")
-          << "after preprocessing : " << ppNode << std::endl;
+      Trace("tpp-debug") << "after preprocessing : " << ppNode << std::endl;
     }
     if (rtfNode != ppNode)
     {
-      Trace("tpp-proof-debug") << "after rtf : " << rtfNode << std::endl;
+      Trace("tpp-debug") << "after rtf : " << rtfNode << std::endl;
     }
     if (retNode != rtfNode)
     {
-      Trace("tpp-proof-debug") << "after rewriting : " << retNode << std::endl;
+      Trace("tpp-debug") << "after rewriting : " << retNode << std::endl;
     }
-    Trace("tpp-proof-debug")
-        << "TheoryPreprocessor::preprocess: finish" << std::endl;
+    Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl;
   }
   if (node == retNode)
   {
@@ -177,7 +175,7 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
       // we wil use the sequence generator
       tret = d_tspg->mkTrustRewriteSequence(cterms);
     }
-    tret.debugCheckClosed("tpp-proof-debug", "TheoryPreprocessor::lemma_ret");
+    tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret");
   }
   else
   {
@@ -185,14 +183,14 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   }
 
   // now, rewrite the lemmas
-  Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: process lemmas"
-                           << std::endl;
+  Trace("tpp-debug") << "TheoryPreprocessor::preprocess: process lemmas"
+                     << std::endl;
   for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
   {
     // get the trust node to process
     TrustNode trn = newLemmas[i];
     trn.debugCheckClosed(
-        "tpp-proof-debug", "TheoryPreprocessor::lemma_new_initial", false);
+        "tpp-debug", "TheoryPreprocessor::lemma_new_initial", false);
     Assert(trn.getKind() == TrustNodeKind::LEMMA);
     Node assertion = trn.getNode();
     // rewrite, which is independent of d_tpg, since additional lemmas
@@ -217,11 +215,9 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
       newLemmas[i] = TrustNode::mkTrustLemma(rewritten, d_lp.get());
     }
     Assert(!isProofEnabled() || newLemmas[i].getGenerator() != nullptr);
-    newLemmas[i].debugCheckClosed("tpp-proof-debug",
-                                  "TheoryPreprocessor::lemma_new");
+    newLemmas[i].debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_new");
   }
-  Trace("tpp-proof-debug") << "Preprocessed: " << node << " " << retNode
-                           << std::endl;
+  Trace("tpp-debug") << "Preprocessed: " << node << " " << retNode << std::endl;
   return tret;
 }
 
@@ -390,9 +386,8 @@ Node TheoryPreprocessor::rewriteWithProof(Node term)
     // may rewrite the same term more than once, thus check hasRewriteStep
     if (termr != term)
     {
-      Trace("tpp-proof-debug")
-          << "TheoryPreprocessor: addRewriteStep (rewriting) " << term << " -> "
-          << termr << std::endl;
+      Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) "
+                         << term << " -> " << termr << std::endl;
       // always use term context hash 0 (default)
       d_tpg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term});
     }
@@ -420,10 +415,9 @@ Node TheoryPreprocessor::preprocessWithProof(Node term)
   {
     if (trn.getGenerator() != nullptr)
     {
-      Trace("tpp-proof-debug")
-          << "TheoryPreprocessor: addRewriteStep (generator) " << term << " -> "
-          << termr << std::endl;
-      trn.debugCheckClosed("tpp-proof-debug",
+      Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) "
+                         << term << " -> " << termr << std::endl;
+      trn.debugCheckClosed("tpp-debug",
                            "TheoryPreprocessor::preprocessWithProof");
       // always use term context hash 0 (default)
       d_tpg->addRewriteStep(
@@ -431,9 +425,8 @@ Node TheoryPreprocessor::preprocessWithProof(Node term)
     }
     else
     {
-      Trace("tpp-proof-debug")
-          << "TheoryPreprocessor: addRewriteStep (trusted) " << term << " -> "
-          << termr << std::endl;
+      Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (trusted) "
+                         << term << " -> " << termr << std::endl;
       // small step trust
       d_tpg->addRewriteStep(
           term, termr, PfRule::THEORY_PREPROCESS, {}, {term.eqNode(termr)});

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b12876a5cc27aaf8d63c2b9b0edbe7aaae988dd2..9935adf59306fc357214b98a2a876dce6fe6d2cc 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1609,6 +1609,9 @@ set(regress_1_tests
   regress1/quantifiers/issue4620-erq-witness-unsound.smt2
   regress1/quantifiers/issue4685-wrewrite.smt2
   regress1/quantifiers/issue5019-cegqi-i.smt2
+  regress1/quantifiers/issue5469-aext.smt2
+  regress1/quantifiers/issue5470-aext.smt2
+  regress1/quantifiers/issue5471-aext.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2

diff --git a/test/regress/regress1/quantifiers/issue5469-aext.smt2 b/test/regress/regress1/quantifiers/issue5469-aext.smt2
new file mode 100644 (file)
index 0000000..d66afb9
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5469-aext.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --sygus-inst --strings-exp --no-check-models
+; EXPECT: sat
+(set-logic NIA)
+(set-option :sygus-inst true)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun d () Int)
+(assert (forall ((g Int)) (or (> 1 g) (> g (div 1 d)))))
+(assert (not (= d 0)))
+(check-sat)

diff --git a/test/regress/regress1/quantifiers/issue5470-aext.smt2 b/test/regress/regress1/quantifiers/issue5470-aext.smt2
new file mode 100644 (file)
index 0000000..500ef6d
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5470-aext.smt2
@@ -0,0 +1,6 @@
+(set-logic NIA)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun b () Int)
+(assert (exists ((c Int)) (< 0 c (div 0 b))))
+(check-sat)

diff --git a/test/regress/regress1/quantifiers/issue5471-aext.smt2 b/test/regress/regress1/quantifiers/issue5471-aext.smt2
new file mode 100644 (file)
index 0000000..c420359
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5471-aext.smt2
@@ -0,0 +1,10 @@
+(set-logic NRA)
+(set-option :sygus-inst true)
+(set-option :strings-exp true)
+(set-info :status unsat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun c () Real)
+(assert (forall ((d Real)) (= (> d 0) (<= (+ d (/ a c)) 0))))
+(assert (<= (* b b) 0))
+(check-sat)