(proof-new) More features for SMT proof post-processor (#5246)

This updates the SMT proof postprocessor with additional stats. It also adds the feature to handle conjunctions as substitution, e.g. a child proof concluding (and (= x t) (= y s)) is interpreted as a substitution for x, y, whereas previously we insisted they must be provided separately.

4 files changed, 151 insertions, 39 deletions

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 0d5578734..0c2f8ccf8 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -376,6 +376,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
   }
   else if (id == PfRule::SUBS)
   {
+    NodeManager* nm = NodeManager::currentNM();
     // Notice that a naive way to reconstruct SUBS is to do a term conversion
     // proof for each substitution.
     // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
@@ -400,21 +401,41 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids);
     }
     std::vector<std::shared_ptr<CDProof>> pfs;
-    std::vector<Node> vvec;
-    std::vector<Node> svec;
+    std::vector<TNode> vsList;
+    std::vector<TNode> ssList;
+    std::vector<TNode> fromList;
     std::vector<ProofGenerator*> pgs;
+    // first, compute the entire substitution
     for (size_t i = 0, nchild = children.size(); i < nchild; i++)
     {
+      // get the substitution
+      builtin::BuiltinProofRuleChecker::getSubstitutionFor(
+          children[i], vsList, ssList, fromList, ids);
+      // ensure proofs for each formula in fromList
+      if (children[i].getKind() == AND && ids == MethodId::SB_DEFAULT)
+      {
+        for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi;
+             j++)
+        {
+          Node nodej = nm->mkConst(Rational(j));
+          cdp->addStep(
+              children[i][j], PfRule::AND_ELIM, {children[i]}, {nodej});
+        }
+      }
+    }
+    std::vector<Node> vvec;
+    std::vector<Node> svec;
+    for (size_t i = 0, nvs = vsList.size(); i < nvs; i++)
+    {
       // Note we process in forward order, since later substitution should be
       // applied to earlier ones, and the last child of a SUBS is processed
       // first.
-      // get the substitution
-      TNode var, subs;
-      builtin::BuiltinProofRuleChecker::getSubstitution(
-          children[i], var, subs, ids);
+      TNode var = vsList[i];
+      TNode subs = ssList[i];
+      TNode childFrom = fromList[i];
       Trace("smt-proof-pp-debug")
-          << "...process " << var << " -> " << subs << " (" << children[i]
-          << ", " << ids << ")" << std::endl;
+          << "...process " << var << " -> " << subs << " (" << childFrom << ", "
+          << ids << ")" << std::endl;
       // apply the current substitution to the range
       if (!vvec.empty())
       {
@@ -429,7 +450,13 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
           std::shared_ptr<CDProof> pf = std::make_shared<CDProof>(d_pnm);
           pfs.push_back(pf);
           // prove the updated substitution
-          TConvProofGenerator tcg(d_pnm, nullptr, TConvPolicy::ONCE);
+          TConvProofGenerator tcg(d_pnm,
+                                  nullptr,
+                                  TConvPolicy::ONCE,
+                                  TConvCachePolicy::NEVER,
+                                  "nested_SUBS_TConvProofGenerator",
+                                  nullptr,
+                                  true);
           // add previous rewrite steps
           for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
           {
@@ -442,11 +469,11 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
           Assert(pfn != nullptr);
           // add the proof
           pf->addProof(pfn);
-          // get proof for children[i] from cdp
-          pfn = cdp->getProofFor(children[i]);
+          // get proof for childFrom from cdp
+          pfn = cdp->getProofFor(childFrom);
           pf->addProof(pfn);
           // ensure we have a proof of var = subs
-          Node veqs = addProofForSubsStep(var, subs, children[i], pf.get());
+          Node veqs = addProofForSubsStep(var, subs, childFrom, pf.get());
           // transitivity
           pf->addStep(var.eqNode(ss), PfRule::TRANS, {veqs, seqss}, {});
           // add to the substitution
@@ -458,9 +485,9 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       }
       // Just use equality from CDProof, but ensure we have a proof in cdp.
       // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
-      // uses the assumption children[i] as a Boolean assignment (e.g.
-      // children[i] = true if we are using MethodId::SB_LITERAL).
-      addProofForSubsStep(var, subs, children[i], cdp);
+      // uses the assumption childFrom as a Boolean assignment (e.g.
+      // childFrom = true if we are using MethodId::SB_LITERAL).
+      addProofForSubsStep(var, subs, childFrom, cdp);
       vvec.push_back(var);
       svec.push_back(subs);
       pgs.push_back(cdp);
@@ -470,7 +497,13 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     if (ts != t)
     {
       // should be implied by the substitution now
-      TConvProofGenerator tcpg(d_pnm, nullptr, TConvPolicy::ONCE);
+      TConvProofGenerator tcpg(d_pnm,
+                               nullptr,
+                               TConvPolicy::ONCE,
+                               TConvCachePolicy::NEVER,
+                               "SUBS_TConvProofGenerator",
+                               nullptr,
+                               true);
       for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
       {
         // not necessarily closed, so we pass false to addRewriteStep.
@@ -523,7 +556,14 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       std::shared_ptr<ProofNode> pfn = trn.toProofNode();
       if (pfn == nullptr)
       {
+        Trace("smt-proof-pp-debug")
+            << "Use TRUST_REWRITE for " << eq << std::endl;
         // did not have a proof of rewriting, probably isExtEq is true
+        if (isExtEq)
+        {
+          // don't update
+          return Node::null();
+        }
         cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq});
       }
       else
@@ -644,23 +684,30 @@ ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
     ProofNodeManager* pnm)
     : d_ruleCount("finalProof::ruleCount"),
       d_totalRuleCount("finalProof::totalRuleCount", 0),
+      d_minPedanticLevel("finalProof::minPedanticLevel", 10),
+      d_numFinalProofs("finalProofs::numFinalProofs", 0),
       d_pnm(pnm),
       d_pedanticFailure(false)
 {
   smtStatisticsRegistry()->registerStat(&d_ruleCount);
   smtStatisticsRegistry()->registerStat(&d_totalRuleCount);
+  smtStatisticsRegistry()->registerStat(&d_minPedanticLevel);
+  smtStatisticsRegistry()->registerStat(&d_numFinalProofs);
 }
 
 ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
 {
   smtStatisticsRegistry()->unregisterStat(&d_ruleCount);
   smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount);
+  smtStatisticsRegistry()->unregisterStat(&d_minPedanticLevel);
+  smtStatisticsRegistry()->unregisterStat(&d_numFinalProofs);
 }
 
 void ProofPostprocessFinalCallback::initializeUpdate()
 {
   d_pedanticFailure = false;
   d_pedanticFailureOut.str("");
+  ++d_numFinalProofs;
 }
 
 bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
@@ -687,6 +734,11 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
       }
     }
   }
+  uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
+  if (plevel != 0)
+  {
+    d_minPedanticLevel.minAssign(plevel);
+  }
   // record stats for the rule
   d_ruleCount << r;
   ++d_totalRuleCount;
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index d7186ea74..3c0d4fbaa 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -173,6 +173,10 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
   HistogramStat<PfRule> d_ruleCount;
   /** Total number of postprocessed rule applications */
   IntStat d_totalRuleCount;
+  /** The minimum pedantic level of any rule encountered */
+  IntStat d_minPedanticLevel;
+  /** The total number of final proofs */
+  IntStat d_numFinalProofs;
   /** Proof node manager (used for pedantic checking) */
   ProofNodeManager* d_pnm;
   /** Was there a pedantic failure? */
@@ -198,6 +202,7 @@ class ProofPostproccess
   void process(std::shared_ptr<ProofNode> pf);
   /** set eliminate rule */
   void setEliminateRule(PfRule rule);
+
  private:
   /** The proof node manager */
   ProofNodeManager* d_pnm;
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 8824859d4..6fc4671ee 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -69,11 +69,11 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this);
   // trusted rules
   pc->registerTrustedChecker(PfRule::THEORY_LEMMA, this, 1);
-  pc->registerTrustedChecker(PfRule::PREPROCESS, this, 2);
-  pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 2);
-  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 2);
-  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 2);
-  pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 2);
+  pc->registerTrustedChecker(PfRule::PREPROCESS, this, 3);
+  pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 3);
+  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 3);
+  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 3);
+  pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3);
   pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
   pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
 }
@@ -117,10 +117,10 @@ Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
   return n;
 }
 
-bool BuiltinProofRuleChecker::getSubstitution(Node exp,
-                                              TNode& var,
-                                              TNode& subs,
-                                              MethodId ids)
+bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
+                                                    TNode& var,
+                                                    TNode& subs,
+                                                    MethodId ids)
 {
   if (ids == MethodId::SB_DEFAULT)
   {
@@ -152,17 +152,57 @@ bool BuiltinProofRuleChecker::getSubstitution(Node exp,
   return true;
 }
 
+bool BuiltinProofRuleChecker::getSubstitutionFor(Node exp,
+                                                 std::vector<TNode>& vars,
+                                                 std::vector<TNode>& subs,
+                                                 std::vector<TNode>& from,
+                                                 MethodId ids)
+{
+  TNode v;
+  TNode s;
+  if (exp.getKind() == AND && ids == MethodId::SB_DEFAULT)
+  {
+    for (const Node& ec : exp)
+    {
+      // non-recursive, do not use nested AND
+      if (!getSubstitutionForLit(ec, v, s, ids))
+      {
+        return false;
+      }
+      vars.push_back(v);
+      subs.push_back(s);
+      from.push_back(ec);
+    }
+    return true;
+  }
+  bool ret = getSubstitutionForLit(exp, v, s, ids);
+  vars.push_back(v);
+  subs.push_back(s);
+  from.push_back(exp);
+  return ret;
+}
+
 Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
 {
-  TNode var, subs;
-  if (!getSubstitution(exp, var, subs, ids))
+  std::vector<TNode> vars;
+  std::vector<TNode> subs;
+  std::vector<TNode> from;
+  if (!getSubstitutionFor(exp, vars, subs, from, ids))
   {
     return Node::null();
   }
-  Trace("builtin-pfcheck-debug")
-      << "applySubstitution (" << ids << "): " << var << " -> " << subs
-      << " (from " << exp << ")" << std::endl;
-  return n.substitute(var, subs);
+  Node ns = n;
+  // apply substitution one at a time, in reverse order
+  for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
+  {
+    TNode v = vars[nvars - 1 - i];
+    TNode s = subs[nvars - 1 - i];
+    Trace("builtin-pfcheck-debug")
+        << "applySubstitution (" << ids << "): " << v << " -> " << s
+        << " (from " << exp << ")" << std::endl;
+    ns = ns.substitute(v, s);
+  }
+  return ns;
 }
 
 Node BuiltinProofRuleChecker::applySubstitution(Node n,
@@ -212,6 +252,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   }
   else if (id == PfRule::SCOPE)
   {
+    NodeManager * nm = NodeManager::currentNM();
     Assert(children.size() == 1);
     if (args.empty())
     {
@@ -224,7 +265,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     {
       return ant.notNode();
     }
-    return NodeManager::currentNM()->mkNode(IMPLIES, ant, children[0]);
+    return nm->mkNode(IMPLIES, ant, children[0]);
   }
   else if (id == PfRule::SUBS)
   {
@@ -270,7 +311,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     {
       return Node::null();
     }
-    Node res = applySubstitutionRewrite(args[0], children, idr);
+    Node res = applySubstitutionRewrite(args[0], children, ids, idr);
     return args[0].eqNode(res);
   }
   else if (id == PfRule::MACRO_SR_PRED_INTRO)
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index d1c3309c3..66b04de45 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -84,13 +84,27 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    */
   Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
   /**
-   * Get substitution. Updates vars/subs to the substitution specified by
-   * exp for the substitution method ids.
+   * Get substitution for literal exp. Updates vars/subs to the substitution
+   * specified by exp for the substitution method ids.
    */
-  static bool getSubstitution(Node exp,
-                              TNode& var,
-                              TNode& subs,
-                              MethodId ids = MethodId::SB_DEFAULT);
+  static bool getSubstitutionForLit(Node exp,
+                                    TNode& var,
+                                    TNode& subs,
+                                    MethodId ids = MethodId::SB_DEFAULT);
+  /**
+   * Get substitution for formula exp. Adds to vars/subs to the substitution
+   * specified by exp for the substitution method ids, which may be multiple
+   * substitutions if exp is of kind AND and ids is SB_DEFAULT (note the other
+   * substitution types always interpret applications of AND as a formula).
+   * The vector "from" are the literals from exp that each substitution in
+   * vars/subs are based on. For example, if exp is (and (= x t) (= y s)), then
+   * vars = { x, y }, subs = { t, s }, from = { (= x y), (= y s) }.
+   */
+  static bool getSubstitutionFor(Node exp,
+                                 std::vector<TNode>& vars,
+                                 std::vector<TNode>& subs,
+                                 std::vector<TNode>& from,
+                                 MethodId ids = MethodId::SB_DEFAULT);
 
   /**
    * Apply substitution on n in skolem form. This encapsulates the exact