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)
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);