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

1 files changed, 12 insertions, 8 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