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.