(proof-new) Proof rule checkers run on skolem forms (#4660)

Previously, the proof rule checkers were run on witness form for convenience. However, it is more flexible for the sake of the internal calculus to run on Skolem forms. The main reason is that the conversion to/from witness form does not preserve terms that contain witness. Our preprocessing steps rely on using witness terms. This design change additionally simplifies a lot of the code of the builtin proof rule checker.

Instead, witness forms can be queried on an as-needed basis, e.g. in MACRO_SR_PRED_TRANSFORM.

2 files changed, 70 insertions, 93 deletions

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index df6109b1d..f6b41104a 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -61,46 +61,17 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
 }
 
-Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
-{
-  Node nk = SkolemManager::getSkolemForm(n);
-  Node nkr = applyRewriteExternal(nk, idr);
-  return SkolemManager::getWitnessForm(nkr);
-}
-
-Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
-{
-  if (exp.isNull() || exp.getKind() != EQUAL)
-  {
-    return Node::null();
-  }
-  Node nk = SkolemManager::getSkolemForm(n);
-  Node nks = applySubstitutionExternal(nk, exp, ids);
-  return SkolemManager::getWitnessForm(nks);
-}
-
-Node BuiltinProofRuleChecker::applySubstitution(Node n,
-                                                const std::vector<Node>& exp,
-                                                MethodId ids)
-{
-  Node nk = SkolemManager::getSkolemForm(n);
-  Node nks = applySubstitutionExternal(nk, exp, ids);
-  return SkolemManager::getWitnessForm(nks);
-}
-
 Node BuiltinProofRuleChecker::applySubstitutionRewrite(
     Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr)
 {
-  Node nk = SkolemManager::getSkolemForm(n);
-  Node nks = applySubstitutionExternal(nk, exp, ids);
-  Node nksr = applyRewriteExternal(nks, idr);
-  return SkolemManager::getWitnessForm(nksr);
+  Node nks = applySubstitution(n, exp, ids);
+  return applyRewrite(nks, idr);
 }
 
-Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr)
+Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
 {
   Trace("builtin-pfcheck-debug")
-      << "applyRewriteExternal (" << idr << "): " << n << std::endl;
+      << "applyRewrite (" << idr << "): " << n << std::endl;
   if (idr == MethodId::RW_REWRITE)
   {
     return Rewriter::rewrite(n);
@@ -111,50 +82,62 @@ Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr)
     return n;
   }
   // unknown rewriter
-  Assert(false)
-      << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for "
-      << idr << std::endl;
+  Assert(false) << "BuiltinProofRuleChecker::applyRewrite: no rewriter for "
+                << idr << std::endl;
   return n;
 }
 
-Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n,
-                                                        Node exp,
-                                                        MethodId ids)
+bool BuiltinProofRuleChecker::getSubstitution(Node exp,
+                                              TNode& var,
+                                              TNode& subs,
+                                              MethodId ids)
 {
-  Assert(!exp.isNull());
-  Node expk = SkolemManager::getSkolemForm(exp);
-  TNode var, subs;
   if (ids == MethodId::SB_DEFAULT)
   {
-    if (expk.getKind() != EQUAL)
+    if (exp.getKind() != EQUAL)
     {
-      return Node::null();
+      return false;
     }
-    var = expk[0];
-    subs = expk[1];
+    var = exp[0];
+    subs = exp[1];
   }
   else if (ids == MethodId::SB_LITERAL)
   {
-    bool polarity = expk.getKind() != NOT;
-    var = polarity ? expk : expk[0];
+    bool polarity = exp.getKind() != NOT;
+    var = polarity ? exp : exp[0];
     subs = NodeManager::currentNM()->mkConst(polarity);
   }
   else if (ids == MethodId::SB_FORMULA)
   {
-    var = expk;
+    var = exp;
     subs = NodeManager::currentNM()->mkConst(true);
   }
   else
   {
-    Assert(false) << "BuiltinProofRuleChecker::applySubstitutionExternal: no "
+    Assert(false) << "BuiltinProofRuleChecker::applySubstitution: no "
                      "substitution for "
                   << ids << std::endl;
+    return false;
+  }
+  return true;
+}
+
+Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
+{
+  TNode var, subs;
+  if (!getSubstitution(exp, var, subs, ids))
+  {
+    return Node::null();
   }
+  Trace("builtin-pfcheck-debug")
+      << "applySubstitution (" << ids << "): " << var << " -> " << subs
+      << " (from " << exp << ")" << std::endl;
   return n.substitute(var, subs);
 }
 
-Node BuiltinProofRuleChecker::applySubstitutionExternal(
-    Node n, const std::vector<Node>& exp, MethodId ids)
+Node BuiltinProofRuleChecker::applySubstitution(Node n,
+                                                const std::vector<Node>& exp,
+                                                MethodId ids)
 {
   Node curr = n;
   // apply substitution one at a time, in reverse order
@@ -164,7 +147,7 @@ Node BuiltinProofRuleChecker::applySubstitutionExternal(
     {
       return Node::null();
     }
-    curr = applySubstitutionExternal(curr, exp[nexp - 1 - i], ids);
+    curr = applySubstitution(curr, exp[nexp - 1 - i], ids);
     if (curr.isNull())
     {
       break;
@@ -233,12 +216,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   {
     Assert(children.empty());
     Assert(1 <= args.size() && args.size() <= 2);
-    MethodId ids = MethodId::RW_REWRITE;
-    if (args.size() == 2 && !getMethodId(args[1], ids))
+    MethodId idr = MethodId::RW_REWRITE;
+    if (args.size() == 2 && !getMethodId(args[1], idr))
     {
       return Node::null();
     }
-    Node res = applyRewrite(args[0]);
+    Node res = applyRewrite(args[0], idr);
     return args[0].eqNode(res);
   }
   else if (id == PfRule::MACRO_SR_EQ_INTRO)
@@ -269,7 +252,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     }
     // **** NOTE: can rewrite the witness form here. This enables certain lemmas
     // to be provable, e.g. (= k t) where k is a purification Skolem for t.
-    res = Rewriter::rewrite(res);
+    res = Rewriter::rewrite(SkolemManager::getWitnessForm(res));
     if (!res.isConst() || !res.getConst<bool>())
     {
       Trace("builtin-pfcheck")
@@ -311,14 +294,18 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     exp.insert(exp.end(), children.begin() + 1, children.end());
     Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr);
     Node res2 = applySubstitutionRewrite(args[0], exp, ids, idr);
-    // can rewrite the witness forms
-    res1 = Rewriter::rewrite(res1);
-    res2 = Rewriter::rewrite(res2);
-    if (res1.isNull() || res1 != res2)
+    // if not already equal, do rewriting
+    if (res1 != res2)
     {
-      Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
-      Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl;
-      return Node::null();
+      // can rewrite the witness forms
+      res1 = Rewriter::rewrite(SkolemManager::getWitnessForm(res1));
+      res2 = Rewriter::rewrite(SkolemManager::getWitnessForm(res2));
+      if (res1.isNull() || res1 != res2)
+      {
+        Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
+        Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl;
+        return Node::null();
+      }
     }
     return args[0];
   }
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index a2ec8b715..6dc7023d5 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -67,24 +67,31 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
   BuiltinProofRuleChecker() {}
   ~BuiltinProofRuleChecker() {}
   /**
-   * Apply rewrite on n (in witness form). This encapsulates the exact behavior
-   * of a REWRITE step in a proof. Rewriting is performed on the Skolem form of
-   * n.
+   * Apply rewrite on n (in skolem form). This encapsulates the exact behavior
+   * of a REWRITE step in a proof.
    *
-   * @param n The node (in witness form) to rewrite,
+   * @param n The node to rewrite,
    * @param idr The method identifier of the rewriter, by default RW_REWRITE
    * specifying a call to Rewriter::rewrite.
    * @return The rewritten form of n.
    */
   static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
   /**
-   * Apply substitution on n (in witness form). This encapsulates the exact
-   * behavior of a SUBS step in a proof. Substitution is on the Skolem form of
-   * n.
+   * Get substitution. Updates vars/subs to the substitution specified by
+   * exp (e.g. as an equality) for the substitution method ids.
+   */
+  static bool getSubstitution(Node exp,
+                              TNode& var,
+                              TNode& subs,
+                              MethodId ids = MethodId::SB_DEFAULT);
+
+  /**
+   * Apply substitution on n in skolem form. This encapsulates the exact
+   * behavior of a SUBS step in a proof.
    *
-   * @param n The node (in witness form) to substitute,
-   * @param exp The (set of) equalities (in witness form) corresponding to the
-   * substitution
+   * @param n The node to substitute,
+   * @param exp The (set of) equalities/literals/formulas that the substitution
+   * is derived from
    * @param ids The method identifier of the substitution, by default SB_DEFAULT
    * specifying that lhs/rhs of equalities are interpreted as a substitution.
    * @return The substituted form of n.
@@ -99,9 +106,8 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    *
    * Combines the above two steps.
    *
-   * @param n The node (in witness form) to substitute and rewrite,
-   * @param exp The (set of) equalities (in witness form) corresponding to the
-   * substitution
+   * @param n The node to substitute and rewrite,
+   * @param exp The (set of) equalities corresponding to the substitution
    * @param ids The method identifier of the substitution.
    * @param idr The method identifier of the rewriter.
    * @return The substituted, rewritten form of n.
@@ -129,27 +135,11 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
 
   /** Register all rules owned by this rule checker into pc. */
   void registerTo(ProofChecker* pc) override;
-
  protected:
   /** Return the conclusion of the given proof step, or null if it is invalid */
   Node checkInternal(PfRule id,
                      const std::vector<Node>& children,
                      const std::vector<Node>& args) override;
-  /**
-   * Apply rewrite (on Skolem form). id is the identifier of the rewriter.
-   */
-  static Node applyRewriteExternal(Node n, MethodId idr = MethodId::RW_REWRITE);
-  /**
-   * Apply substitution for n (on Skolem form), where exp is an equality
-   * (or set of equalities) in Witness form. Returns the result of
-   * n * sigma{ids}(exp), where sigma{ids} is a substitution based on method
-   * identifier ids.
-   */
-  static Node applySubstitutionExternal(Node n, Node exp, MethodId ids);
-  /** Same as above, for a list of substitutions in exp */
-  static Node applySubstitutionExternal(Node n,
-                                        const std::vector<Node>& exp,
-                                        MethodId ids);
 };
 
 }  // namespace builtin