Ensure trusted steps are given for skolem lemmas when proofs are enabled (#8302)

Fixes cvc5/cvc5-projects#492.

diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp
index 782d4569de7aa52f7cad82a6a2ef0a148ca1619c..9ca1c82ce1f8ef2602d6854dd83ba0dea1c4cfa4 100644 (file)
--- a/src/preprocessing/passes/theory_rewrite_eq.cpp
+++ b/src/preprocessing/passes/theory_rewrite_eq.cpp
@@ -107,7 +107,9 @@ TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
       if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean())
       {
         // For example, (= x y) ---> (and (>= x y) (<= x y))
-        TrustNode trn = te->ppRewriteEquality(ret);
+        std::vector<SkolemLemma> lems;
+        TrustNode trn = te->ppRewrite(ret, lems);
+        Assert(lems.empty());
         // can make proof producing by using proof generator from trn
         if (!trn.isNull() && trn.getNode() != ret)
         {

diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index 5028cba1b3dbb60f922f3d107477f4fc21cb8393..76f8f54d618dd40b95e425dabfc6ad327af38de7 100644 (file)
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -225,6 +225,22 @@ enum class PfRule : uint32_t
   // the quantifiers rewriter involves constructing new bound variables that are
   // not guaranteed to be consistent on each call.
   THEORY_REWRITE,
+  // ======== Theory Preprocess
+  // Children: none
+  // Arguments: (F, tid)
+  // ----------------------------------------
+  // Conclusion: F
+  // where F is an equality of the form t = Theory::ppRewrite(t) for the theory
+  // with identifier tid. Notice this is a "trusted" rule.
+  THEORY_PREPROCESS,
+  // ======== Theory Preprocess
+  // Children: none
+  // Arguments: (F, tid)
+  // ----------------------------------------
+  // Conclusion: F
+  // where F was added as a new assertion by theory preprocessing from the
+  // theory with identifier tid.
+  THEORY_PREPROCESS_LEMMA,
   // The remaining rules in this section have the signature of a "trusted rule":
   //
   // Children: ?
@@ -240,11 +256,6 @@ enum class PfRule : uint32_t
   PREPROCESS,
   // where F was added as a new assertion by some preprocessing pass.
   PREPROCESS_LEMMA,
-  // where F is an equality of the form t = Theory::ppRewrite(t) for some
-  // theory. Notice this is a "trusted" rule.
-  THEORY_PREPROCESS,
-  // where F was added as a new assertion by theory preprocessing.
-  THEORY_PREPROCESS_LEMMA,
   // where F is an equality of the form t = t' where t was replaced by t'
   // based on theory expand definitions.
   THEORY_EXPAND_DEF,

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 067dc8b0c6a633935e39efa81c49a883624712c2..cc705109e5e0a299f44c05d3592a3318895d4b87 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -743,13 +743,36 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(
   return solveStatus;
 }
 
-TrustNode TheoryEngine::ppRewriteEquality(TNode eq)
+TrustNode TheoryEngine::ppRewrite(TNode term,
+                                  std::vector<theory::SkolemLemma>& lems)
 {
-  Assert(eq.getKind() == kind::EQUAL);
-  std::vector<SkolemLemma> lems;
-  TrustNode trn = theoryOf(eq)->ppRewrite(eq, lems);
-  // should never introduce a skolem to eliminate an equality
   Assert(lems.empty());
+  TheoryId tid = d_env.theoryOf(term);
+  TrustNode trn = d_theoryTable[tid]->ppRewrite(term, lems);
+  // should never introduce a skolem to eliminate an equality
+  Assert(lems.empty() || term.getKind() != kind::EQUAL);
+  if (!isProofEnabled())
+  {
+    return trn;
+  }
+  Assert(d_lazyProof != nullptr);
+  // if proofs are enabled, must ensure we have proofs for all the skolem lemmas
+  for (SkolemLemma& skl : lems)
+  {
+    TrustNode tskl = skl.d_lemma;
+    Assert(tskl.getKind() == TrustNodeKind::LEMMA);
+    if (tskl.getGenerator() == nullptr)
+    {
+      Node proven = tskl.getProven();
+      Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid);
+      d_lazyProof->addStep(
+          proven, PfRule::THEORY_PREPROCESS_LEMMA, {}, {proven, tidn});
+      skl.d_lemma = TrustNode::mkTrustLemma(proven, d_lazyProof.get());
+    }
+  }
+  // notice that we don't ensure proofs are processed for the returned (rewrite)
+  // trust node, this is the responsibility of the caller, i.e. theory
+  // preprocessor.
   return trn;
 }
 
@@ -1798,7 +1821,10 @@ TrustNode TheoryEngine::getExplanation(
   return TrustNode::mkTrustPropExp(conclusion, expNode, nullptr);
 }
 
-bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }
+bool TheoryEngine::isProofEnabled() const
+{
+  return d_env.isTheoryProofProducing();
+}
 
 void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
   bool hasFailure = false;

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index c107ef1a9153009a97e4f6836e189247cfd8e7bb..75defade53e3affb5506c4a82342a98218288537 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -171,10 +171,15 @@ class TheoryEngine : protected EnvObj
   }
 
   /**
-   * Preprocess rewrite equality, called by the preprocessor to rewrite
-   * equalities appearing in the input.
+   * Preprocess rewrite, called:
+   * (1) on equalities by the preprocessor to rewrite equalities appearing in
+   * the input,
+   * (2) on non-equalities by the theory preprocessor.
+   *
+   * Calls the ppRewrite of the theory of term and adds the associated skolem
+   * lemmas to lems, for details see Theory::ppRewrite.
    */
-  TrustNode ppRewriteEquality(TNode eq);
+  TrustNode ppRewrite(TNode term, std::vector<theory::SkolemLemma>& lems);
   /** Notify (preprocessed) assertions. */
   void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
 

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index e92722a2addefc7b0fc438f502b15756a20f2165..26f9e759f67d8a4dc63186ee17bcc056028d4b7d 100644 (file)
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -440,9 +440,11 @@ Node TheoryPreprocessor::preprocessWithProof(Node term,
     return term;
   }
   // call ppRewrite for the given theory
-  TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term, lems);
+  std::vector<SkolemLemma> newLems;
+  TrustNode trn = d_engine.ppRewrite(term, newLems);
   Trace("tpp-debug2") << "preprocessWithProof returned " << trn
-                      << ", #lems = " << lems.size() << std::endl;
+                      << ", #lems = " << newLems.size() << std::endl;
+  lems.insert(lems.end(), newLems.begin(), newLems.end());
   if (trn.isNull())
   {
     // no change, return

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5a1d8f832588fae3c45b27460161a1a77fd27b1f..32604095fc0a78a49bc7e873a36683682f4f9cca 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -950,6 +950,7 @@ set(regress_0_tests
   regress0/proofs/proj-issue342-eager-checking-no-proof-checking.smt2
   regress0/proofs/proj-issue430-coverings-double-negation.smt2
   regress0/proofs/proj-issue462-sat-proof-option.smt2
+  regress0/proofs/proj-issue492-skolem-lemma-pf.smt2
   regress0/proofs/qgu-fuzz-1-bool-sat.smt2
   regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2
   regress0/proofs/qgu-fuzz-3-chainres-checking.smt2

diff --git a/test/regress/regress0/proofs/proj-issue492-skolem-lemma-pf.smt2 b/test/regress/regress0/proofs/proj-issue492-skolem-lemma-pf.smt2
new file mode 100644 (file)
index 0000000..b21a447
--- /dev/null
+++ b/test/regress/regress0/proofs/proj-issue492-skolem-lemma-pf.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(set-option :produce-proofs true)
+(assert (exists ((x (Set (_ BitVec 16)))) (set.member (set.choose (set.inter x x)) (set.inter x x))))
+(check-sat)