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

2 files changed, 78 insertions, 23 deletions

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