5 files changed, 33 insertions, 5 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index c332642f1..f90b5ff51 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -110,11 +110,29 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw
           vector<TypeNode> argTypes = t.getArgTypes();
           replace(argTypes.begin(), argTypes.end(), t[i], nm->mkBitVectorType(1));
           TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType());
-          Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "_bt",
+          Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__",
                                 newType, "a function introduced by Boolean-term conversion",
                                 NodeManager::SKOLEM_EXACT_NAME);
           Debug("boolean-terms") << "constructed func: " << n << " of type " << newType << endl;
           top.setAttribute(BooleanTermAttr(), n);
+          NodeBuilder<> boundVarsBuilder(kind::BOUND_VAR_LIST);
+          NodeBuilder<> bodyBuilder(kind::APPLY_UF);
+          bodyBuilder << n;
+          for(unsigned j = 0; j < t.getNumChildren() - 1; ++j) {
+            Node var = nm->mkBoundVar(t[j]);
+            boundVarsBuilder << var;
+            if(t[j].isBoolean()) {
+              bodyBuilder << nm->mkNode(kind::ITE, var, nm->mkConst(BitVector(1u, 1u)),
+                                        nm->mkConst(BitVector(1u, 0u)));
+            } else {
+              bodyBuilder << var;
+            }
+          }
+          Node boundVars = boundVarsBuilder;
+          Node body = bodyBuilder;
+          Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
+          Debug("boolean-terms") << "substituting " << top << " ==> " << lam << std::endl;
+          d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
           d_booleanTermCache[make_pair(top, boolParent)] = n;
           return n;
         }
@@ -205,9 +223,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw
           return n;
         }
       }
-    }/* else if(t.isRecord()) {
-      Unimplemented();
-    }*/
+    }
     return top;
   }
   switch(k) {
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index dea9adcf7..e51a7bbb0 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -41,6 +41,9 @@ class BooleanTermConverter {
                          PairHashFunction< Node, bool,
                                            NodeHashFunction, std::hash<int> > > BooleanTermCache;
 
+  /** The SmtEngine to which we're associated */
+  SmtEngine& d_smt;
+
   /** The cache used during Boolean term conversion */
   BooleanTermCache d_booleanTermCache;
 
@@ -51,6 +54,10 @@ class BooleanTermConverter {
 
 public:
 
+  BooleanTermConverter(SmtEngine& smt) :
+    d_smt(smt) {
+  }
+
   /**
    * We rewrite Boolean terms in assertions as bitvectors of length 1.
    */
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 38fd3ab8b..fb0ee808e 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "smt/model_postprocessor.h"
+#include "smt/boolean_terms.h"
 
 using namespace CVC4;
 using namespace CVC4::smt;
@@ -43,6 +44,8 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     }
     d_nodes[current] = b;
     Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
+  } else if(current.hasAttribute(smt::BooleanTermAttr())) {
+    Debug("boolean-terms") << "found bool-term attr on: " << current << std::endl;
   } else {
     Debug("tuprec") << "returning self" << std::endl;
     // rewrite to self
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 92a339a45..eaa1c1643 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -343,7 +343,7 @@ public:
     d_assertionsToPreprocess(),
     d_nonClausalLearnedLiterals(),
     d_realAssertionsEnd(0),
-    d_booleanTermConverter(),
+    d_booleanTermConverter(d_smt),
     d_propagator(d_nonClausalLearnedLiterals, true, true),
     d_assertionsToCheck(),
     d_fakeContext(),
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index b6fb156f6..bbb0a95e9 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -80,6 +80,7 @@ namespace smt {
   class SmtEngineStatistics;
   class SmtEnginePrivate;
   class SmtScope;
+  class BooleanTermConverter;
 
   void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
 
@@ -308,6 +309,7 @@ class CVC4_PUBLIC SmtEngine {
 
   friend class ::CVC4::smt::SmtEnginePrivate;
   friend class ::CVC4::smt::SmtScope;
+  friend class ::CVC4::smt::BooleanTermConverter;
   friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*);
   friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
   // to access d_modelCommands