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

6 files changed, 97 insertions, 120 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5cddccc58..9c95163bc 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -367,13 +367,13 @@ libcvc4_add_sources(
   theory/booleans/theory_bool_rewriter.h
   theory/booleans/theory_bool_type_rules.h
   theory/booleans/type_enumerator.h
+  theory/builtin/proof_checker.cpp
+  theory/builtin/proof_checker.h
   theory/builtin/theory_builtin.cpp
   theory/builtin/theory_builtin.h
   theory/builtin/theory_builtin_rewriter.cpp
   theory/builtin/theory_builtin_rewriter.h
   theory/builtin/theory_builtin_type_rules.h
-  theory/builtin/proof_checker.cpp
-  theory/builtin/proof_checker.h
   theory/builtin/type_enumerator.cpp
   theory/builtin/type_enumerator.h
   theory/bv/abstraction.cpp
diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index acbf6ee49..8f786052b 100644
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -25,14 +25,8 @@ Node ProofRuleChecker::check(PfRule id,
                              const std::vector<Node>& children,
                              const std::vector<Node>& args)
 {
-  // convert to witness form
-  std::vector<Node> childrenw = children;
-  std::vector<Node> argsw = args;
-  SkolemManager::convertToWitnessFormVec(childrenw);
-  SkolemManager::convertToWitnessFormVec(argsw);
-  Node res = checkInternal(id, childrenw, argsw);
-  // res is in terms of witness form, convert back to Skolem form
-  return SkolemManager::getSkolemForm(res);
+  // call instance-specific checkInternal method
+  return checkInternal(id, children, args);
 }
 
 Node ProofRuleChecker::checkChildrenArg(PfRule id,
@@ -259,4 +253,14 @@ void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc)
   d_checker[id] = psc;
 }
 
+ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id)
+{
+  std::map<PfRule, ProofRuleChecker*>::const_iterator it = d_checker.find(id);
+  if (it == d_checker.end())
+  {
+    return nullptr;
+  }
+  return it->second;
+}
+
 }  // namespace CVC4
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index d6d77df2b..65ad9f24d 100644
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -40,8 +40,8 @@ class ProofRuleChecker
    * premises and arguments, or null if such a proof node is not well-formed.
    *
    * Note that the input/output of this method expects to be terms in *Skolem
-   * form*. To facilitate checking, this method converts to/from witness
-   * form, calling the subprocedure checkInternal below.
+   * form*, which is passed to checkInternal below. Rule checkers may
+   * convert premises to witness form when necessary.
    *
    * @param id The id of the proof node to check
    * @param children The premises of the proof node to check. These are nodes
@@ -75,17 +75,15 @@ class ProofRuleChecker
 
  protected:
   /**
-   * This checks a single step in a proof. It is identical to check above
-   * except that children and args have been converted to "witness form"
-   * (see SkolemManager). Likewise, its output should be in witness form.
+   * This checks a single step in a proof.
    *
    * @param id The id of the proof node to check
    * @param children The premises of the proof node to check. These are nodes
    * corresponding to the conclusion (ProofNode::getResult) of the children
-   * of the proof node we are checking, in witness form.
+   * of the proof node we are checking.
    * @param args The arguments of the proof node to check
-   * @return The conclusion of the proof node, in witness form, if successful or
-   * null if such a proof node is malformed.
+   * @return The conclusion of the proof node if successful or null if such a
+   * proof node is malformed.
    */
   virtual Node checkInternal(PfRule id,
                              const std::vector<Node>& children,
@@ -158,6 +156,8 @@ class ProofChecker
                   const char* traceTag);
   /** Indicate that psc is the checker for proof rule id */
   void registerChecker(PfRule id, ProofRuleChecker* psc);
+  /** get checker for */
+  ProofRuleChecker* getCheckerFor(PfRule id);
 
  private:
   /** statistics class */
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index ec589a16e..a15d8a2d2 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -102,12 +102,8 @@ enum class PfRule : uint32_t
   // Conclusion: (= t t')
   // where
   //   t' is
-  //   toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)))
-  //   toSkolem(...) converts terms from witness form to Skolem form,
-  //   toWitness(...) converts terms from Skolem form to witness form.
+  //   Rewriter{idr}(t*sigma{ids}(Fn)*...*sigma{ids}(F1))
   //
-  // Notice that:
-  //   toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))
   // In other words, from the point of view of Skolem forms, this rule
   // transforms t to t' by standard substitution + rewriting.
   //
@@ -125,7 +121,7 @@ enum class PfRule : uint32_t
   // ---------------------------------------------------------------
   // Conclusion: F
   // where
-  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
+  //   Rewriter{idr}(toWitness(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
   // where ids and idr are method identifiers.
   //
   // Notice that we apply rewriting on the witness form of F, meaning that this
@@ -145,7 +141,7 @@ enum class PfRule : uint32_t
   // Conclusion: F'
   // where
   //   F' is
-  //   toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)).
+  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)).
   // where ids and idr are method identifiers.
   //
   // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
@@ -161,8 +157,8 @@ enum class PfRule : uint32_t
   // ----------------------------------------
   // Conclusion: G
   // where
-  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
-  //   Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
+  //   Rewriter{idr}(toWitness(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
+  //   Rewriter{idr}(toWitness(G)*sigma{ids}(Fn)*...*sigma{ids}(F1))
   //
   // Notice that we apply rewriting on the witness form of F and G, similar to
   // MACRO_SR_PRED_INTRO.
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