1 files changed, 14 insertions, 3 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c19bdda91..77a768152 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -69,6 +69,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   }
   Rewriter::init();
   StatisticsRegistry::registerStat(&d_combineTheoriesTime);
+  d_true = NodeManager::currentNM()->mkConst<bool>(true);
+  d_false = NodeManager::currentNM()->mkConst<bool>(false);
 }
 
 TheoryEngine::~TheoryEngine() {
@@ -318,7 +320,7 @@ void TheoryEngine::combineTheories() {
 
     if (carePair.a.isConst() && carePair.b.isConst()) {
       // TODO: equality engine should auto-detect these as disequal
-      d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), NodeManager::currentNM()->mkConst<bool>(true));
+      d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), d_true);
       continue;
     }
 
@@ -332,7 +334,7 @@ void TheoryEngine::combineTheories() {
       
       if (isTrivial) {
         value = normalizedEquality.getConst<bool>();
-        normalizedEquality = NodeManager::currentNM()->mkConst<bool>(true);
+        normalizedEquality = d_true;
       }
       else {
         d_sharedLiteralsIn[normalizedEquality] = theory::THEORY_LAST;
@@ -875,7 +877,7 @@ Node TheoryEngine::explain(ExplainTask toExplain)
 #endif
 
   // No need to explain "true"
-  explained.insert(ExplainTask(NodeManager::currentNM()->mkConst<bool>(true), SHARED_DATABASE_EXPLANATION));
+  explained.insert(ExplainTask(d_true, SHARED_DATABASE_EXPLANATION));
 
   while (true) {
 
@@ -1011,3 +1013,12 @@ void TheoryEngine::sharedConflict(TNode conflict) {
   Debug("theory") << "TheoryEngine::sharedConflict(" << conflict << "): " << fullConflict << std::endl;
   lemma(fullConflict, true, false);
 }
+
+
+Node TheoryEngine::ppSimpITE(TNode assertion)
+{
+  Node result = d_iteSimplifier.simpITE(assertion);
+  result = d_iteSimplifier.simplifyWithCare(result);
+  result = Rewriter::rewrite(result);
+  return result;
+}