(proof-new) Generalize single step helper in eager proof generator (#5046)

This allows single step proofs to have premises, closed by a SCOPE. This will be useful for array lemmas.

diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index c390a4b251bb14b43ae9cf2badcff131c7bd0507..81c3e78160a53e5d18b3919ee06485dec86d594f 100644 (file)
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -63,15 +63,15 @@ void CombinationCareGraph::combineTheories()
     Debug("combineTheories")
         << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
 
-    Node split = equality.orNode(equality.notNode());
     TrustNode tsplit;
     if (isProofEnabled())
     {
       // make proof of splitting lemma
-      tsplit = d_cmbsPg->mkTrustNode(split, PfRule::SPLIT, {equality});
+      tsplit = d_cmbsPg->mkTrustNodeSplit(equality);
     }
     else
     {
+      Node split = equality.orNode(equality.notNode());
       tsplit = TrustNode::mkTrustLemma(split, nullptr);
     }
     sendLemma(tsplit, carePair.d_theory);

diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp
index 09f02708bfbe1164dfaf3ce07a2d3f07f902de73..ddf1a4d3a9a707f544eb30b680f8c5d8b63981bc 100644 (file)
--- a/src/theory/eager_proof_generator.cpp
+++ b/src/theory/eager_proof_generator.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/eager_proof_generator.h"
 
+#include "expr/proof.h"
 #include "expr/proof_node_manager.h"
 
 namespace CVC4 {
@@ -93,13 +94,27 @@ TrustNode EagerProofGenerator::mkTrustNode(Node n,
   return TrustNode::mkTrustLemma(n, this);
 }
 
-TrustNode EagerProofGenerator::mkTrustNode(Node n,
+TrustNode EagerProofGenerator::mkTrustNode(Node conc,
                                            PfRule id,
+                                           const std::vector<Node>& exp,
                                            const std::vector<Node>& args,
                                            bool isConflict)
 {
-  std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, n);
-  return mkTrustNode(n, pf, isConflict);
+  // if no children, its easy
+  if (exp.empty())
+  {
+    std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, conc);
+    return mkTrustNode(conc, pf, isConflict);
+  }
+  // otherwise, we use CDProof + SCOPE
+  CDProof cdp(d_pnm);
+  cdp.addStep(conc, id, exp, args);
+  std::shared_ptr<ProofNode> pf = cdp.getProofFor(conc);
+  // We use mkNode instead of mkScope, since there is no reason to check
+  // whether the free assumptions of pf are in exp, since they are by the
+  // construction above.
+  std::shared_ptr<ProofNode> pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp);
+  return mkTrustNode(pfs->getResult(), pfs, isConflict);
 }
 
 TrustNode EagerProofGenerator::mkTrustedPropagation(
@@ -117,7 +132,7 @@ TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
 {
   // make the lemma
   Node lem = f.orNode(f.notNode());
-  return mkTrustNode(lem, PfRule::SPLIT, {f}, false);
+  return mkTrustNode(lem, PfRule::SPLIT, {}, {f}, false);
 }
 
 std::string EagerProofGenerator::identify() const { return d_name; }

diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h
index 226750a91c894008c84b4b22d4db419d2378de9f..018bf7aeaf889222b80f724124b221f52597e695 100644 (file)
--- a/src/theory/eager_proof_generator.h
+++ b/src/theory/eager_proof_generator.h
@@ -116,20 +116,21 @@ class EagerProofGenerator : public ProofGenerator
                         std::shared_ptr<ProofNode> pf,
                         bool isConflict = false);
   /**
-   * Make trust node from a single step proof (with no premises). This is a
-   * convenience function that avoids the need to explictly construct ProofNode
-   * by the caller.
+   * Make trust node from a single step proof. This is a convenience function
+   * that avoids the need to explictly construct ProofNode by the caller.
    *
-   * @param n The proven node,
-   * @param id The rule of the proof concluding n
-   * @param args The arguments to the proof concluding n,
+   * @param conc The conclusion of the rule,
+   * @param id The rule of the proof concluding conc
+   * @param exp The explanation (premises) to the proof concluding conc,
+   * @param args The arguments to the proof concluding conc,
    * @param isConflict Whether the returned trust node is a conflict (otherwise
    * it is a lemma),
    * @return The trust node corresponding to the fact that this generator has
-   * a proof of n.
+   * a proof of (children => exp), or of exp if children is empty.
    */
-  TrustNode mkTrustNode(Node n,
+  TrustNode mkTrustNode(Node conc,
                         PfRule id,
+                        const std::vector<Node>& exp,
                         const std::vector<Node>& args,
                         bool isConflict = false);
   /**

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 3e6f66b7383302681e34c2fdafaf155aa6c6bc14..080349f734dd83c542824899af01ec72ef421a9d 100644 (file)
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -52,7 +52,11 @@ TermRegistry::TermRegistry(SolverState& s,
       d_proxyVar(s.getUserContext()),
       d_proxyVarToLength(s.getUserContext()),
       d_lengthLemmaTermsCache(s.getUserContext()),
-      d_epg(nullptr)
+      d_epg(pnm ? new EagerProofGenerator(
+                      pnm,
+                      s.getUserContext(),
+                      "strings::TermRegistry::EagerProofGenerator")
+                : nullptr)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_zero = nm->mkConst(Rational(0));
@@ -282,7 +286,7 @@ void TermRegistry::registerTerm(Node n, int effort)
       if (d_epg != nullptr)
       {
         regTermLem = d_epg->mkTrustNode(
-            eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {n});
+            eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {}, {n});
       }
       else
       {
@@ -384,7 +388,7 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n)
   // it is a simple rewrite to justify this
   if (d_epg != nullptr)
   {
-    return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {ret});
+    return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {}, {ret});
   }
   return TrustNode::mkTrustLemma(ret, nullptr);
 }
@@ -508,7 +512,7 @@ TrustNode TermRegistry::getRegisterTermAtomicLemma(
 
   if (d_epg != nullptr)
   {
-    return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {n});
+    return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {}, {n});
   }
   return TrustNode::mkTrustLemma(lenLemma, nullptr);
 }