diff options
| author | Lachnitt <lachnitt@stanford.edu> | 2021-09-23 15:08:31 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-23 22:08:31 +0000 |
| commit | 1e9c3deaf16c1fefd7d8344b9e6b6ddb9a19756e (patch) | |
| tree | c9eba48e2143eed524f01fa8c0a47fe9855c2530 /src/theory/builtin/proof_checker.cpp | |
| parent | 6c67ed5a2521012d523eb3f11ff344bf7062ee6e (diff) | |
[proofs] Alethe: Translate THEORY_REWRITE (#7236)
Implementation of the translation of THEORY_REWRITE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
Diffstat (limited to 'src/theory/builtin/proof_checker.cpp')
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 1309a05f9..d5b856456 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -57,6 +57,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS_EQ, this, 3); pc->registerTrustedChecker(PfRule::THEORY_INFERENCE, this, 3); + pc->registerChecker(PfRule::ALETHE_RULE, this); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( |