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

3 files changed, 25 insertions, 25 deletions

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.