(proof-new) Theory preprocessor proof producing (#4807)
[cvc5.git] / src / theory / builtin / proof_checker.cpp
index 05c17dedf4a900bfc3d062777e62d7064eee0619..7521d116e7c3ec5a57fc3bfd3c8cba8218363d1f 100644 (file)
@@ -61,9 +61,13 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
   pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
   pc->registerChecker(PfRule::THEORY_REWRITE, this);
-  pc->registerChecker(PfRule::PREPROCESS, this);
-  pc->registerChecker(PfRule::WITNESS_AXIOM, this);
   pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this);
+  // trusted rules
+  pc->registerTrustedChecker(PfRule::PREPROCESS, this, 2);
+  pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 2);
+  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 2);
+  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 2);
+  pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 2);
 }
 
 Node BuiltinProofRuleChecker::applyTheoryRewrite(Node n, bool preRewrite)
@@ -330,7 +334,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     Assert(args.size() == 1);
     return RemoveTermFormulas::getAxiomFor(args[0]);
   }
-  else if (id == PfRule::PREPROCESS || id == PfRule::WITNESS_AXIOM)
+  else if (id == PfRule::PREPROCESS || id == PfRule::PREPROCESS_LEMMA
+           || id == PfRule::THEORY_PREPROCESS
+           || id == PfRule::THEORY_PREPROCESS_LEMMA
+           || id == PfRule::WITNESS_AXIOM)
   {
     Assert(children.empty());
     Assert(args.size() == 1);