Sketch next

4 files changed, 25 insertions, 1 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index e96f23603..c2b5d31b1 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -34,6 +34,7 @@ const char* toString(PfRule id)
     case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
     case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
     case PfRule::THEORY_LEMMA: return "THEORY_LEMMA";
+    case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
     //================================================= Boolean rules
     case PfRule::SPLIT: return "SPLIT";
     case PfRule::AND_ELIM: return "AND_ELIM";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index d32206cb4..f45ff3544 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -173,6 +173,12 @@ enum class PfRule : uint32_t
   // 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.
   THEORY_LEMMA,
+  // ======== Theory preprocess
+  // Children: (F)
+  // Arguments: none
+  // ---------------------------------------------------------------
+  // Conclusion: TheoryEngine::preprocess(F).
+  THEORY_PREPROCESS,
 
   //================================================= Boolean rules
   // ======== Split
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;