Proper handling for lemmas that are conjuncts:

Record a separate recipe for each conjunct, but have as the "original lemma" in this recipe the complete conjunction, so that we can report this to the theory solver later, if asked.

Refactoring: instead of propagating the proof recipes from the theory engine to the prop engine and cnf stream to be registered there, just register them at the theory engine - as the prop engine and cnf stream don't change them.

1 files changed, 8 insertions, 2 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index eed58864a..ea8628f9c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -322,6 +322,13 @@ class TheoryEngine {
     void handleUserAttribute( const char* attr, theory::Theory* t ){
       d_engine->handleUserAttribute( attr, t );
     }
+
+  private:
+
+    /**
+     * A helper function for registering lemma recipes with the proof engine
+     */
+    void registerLemmaRecipe(Node lemma, Node originalLemma, theory::TheoryId theoryId);
   };/* class TheoryEngine::EngineOutputChannel */
 
   /**
@@ -429,8 +436,7 @@ class TheoryEngine {
                             bool negated,
                             bool removable,
                             bool preprocess,
-                            theory::TheoryId atomsTo,
-                            LemmaProofRecipe* proofRecipe);
+                            theory::TheoryId atomsTo);
 
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);