diff options
Diffstat (limited to 'src/theory/builtin/proof_kinds')
| -rw-r--r-- | src/theory/builtin/proof_kinds | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/builtin/proof_kinds b/src/theory/builtin/proof_kinds index eb9643ec3..4daec3a90 100644 --- a/src/theory/builtin/proof_kinds +++ b/src/theory/builtin/proof_kinds @@ -146,7 +146,7 @@ macro MACRO_SR_PRED_TRANSFORM 1: 1:2 { (TRUE_INTRO <children>[0]))) } -// ======== Untrustworthy theory lemma +// ======== Theory lemma // Children: none // Arguments: (F, tid) // --------------------------------------------------------------- @@ -155,3 +155,10 @@ macro MACRO_SR_PRED_TRANSFORM 1: 1:2 { // This is a "coarse-grained" rule that is used as a placeholder if a theory // did not provide a proof for a lemma or conflict. proofrule THEORY_LEMMA 0 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker + +// ======== Theory preprocess +// Children: (F) +// Arguments: none +// --------------------------------------------------------------- +// Conclusion: TheoryEngine::preprocess(F). +proofrule THEORY_PREPROCESS 0 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker |