From: Guy <katz911@gmail.com>
Date: Thu, 28 Jul 2016 02:03:13 +0000 (-0700)
Subject: Proper instrumentation of the preprocessing phase
X-Git-Tag: cvc5-1.0.0~6040^2~20
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4835c73a86d00bf20a88b9fc71964ac13ca08ef0;p=cvc5.git

Proper instrumentation of the preprocessing phase
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 123b0bffc..e4b4756bf 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -84,7 +84,7 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
   d_engine->d_outputChannelUsed = true;
 
   PROOF({
-      registerLemmaRecipe(lemma, lemma, d_theory);
+      registerLemmaRecipe(lemma, lemma, preprocess, d_theory);
     });
 
   theory::LemmaStatus result = d_engine->lemma(lemma,
@@ -96,13 +96,15 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
   return result;
 }
 
-void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node originalLemma, theory::TheoryId theoryId) {
+void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, theory::TheoryId theoryId) {
   // During CNF conversion, conjunctions will be broken down into
   // multiple lemmas. In order for the recipes to match, we have to do
   // the same here.
-
   NodeManager* nm = NodeManager::currentNM();
 
+  if (preprocess)
+    lemma = d_engine->preprocess(lemma);
+
   bool negated = (lemma.getKind() == kind::NOT);
   if (negated)
     lemma = lemma[0];
@@ -112,26 +114,26 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori
   case kind::AND:
     Assert(!negated); // TODO
     for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
-      registerLemmaRecipe(lemma[i], originalLemma, theoryId);
+      registerLemmaRecipe(lemma[i], originalLemma, false, theoryId);
     break;
 
   case kind::IFF:
     if (!negated) {
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1].negate()), originalLemma, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1].negate()), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, false, theoryId);
     } else {
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1]), originalLemma, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1]), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, false, theoryId);
     }
     break;
 
   case kind::ITE:
     if (!negated) {
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2]), originalLemma, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2]), originalLemma, false, theoryId);
     } else {
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2].negate()), originalLemma, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2].negate()), originalLemma, false, theoryId);
     }
     break;
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index ea8628f9c..9316066a5 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -328,7 +328,7 @@ class TheoryEngine {
     /**
      * A helper function for registering lemma recipes with the proof engine
      */
-    void registerLemmaRecipe(Node lemma, Node originalLemma, theory::TheoryId theoryId);
+    void registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, theory::TheoryId theoryId);
   };/* class TheoryEngine::EngineOutputChannel */
 
   /**