diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/builtin/proof_kinds | 9 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 10 |
2 files changed, 18 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 diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 3b6ffd6de..09076d29e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1810,6 +1810,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, // Run theory preprocessing, maybe Node ppNode = preprocess ? this->preprocess(node) : Node(node); + + if (d_lazyProof!=nullptr) + { + // FIXME + } // Remove the ITEs Debug("ite") << "Remove ITE from " << ppNode << std::endl; @@ -1818,6 +1823,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, d_tform_remover.run(additionalLemmas.ref(), additionalLemmas.getIteSkolemMap()); Debug("ite") << "..done " << additionalLemmas[0] << std::endl; + + if (d_lazyProof!=nullptr) + { + // FIXME + } if(Debug.isOn("lemma-ites")) { Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl; |