Functions and predicates over Boolean now work with --check-models and output correct

models for such functions (though they are somewhat ugly at present).

There's still a problem with model extraction, but it's not Boolean terms' fault.
Sometimes checkModel() can report that the model is just fine, but if a user extracts
values with getValue(), they find problems with the model (i.e., it doesn't satisfy some
assertions).  This appears to be due to an asymmetry between how checkModel() works and
how Model::getValue() works.  I'll open a bugzilla report to discuss this after thinking
some more on it.

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index bc7f0f47cf8839b8f197e810cdd16fc1bd74705b..ed643b830736e4512bfe1009777f62ffaa219e5c 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -53,8 +53,12 @@ std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) {
 }
 
 std::ostream& operator<<(std::ostream& out, const Expr& e) {
-  ExprManagerScope ems(*e.getExprManager());
-  return out << e.getNode();
+  if(e.isNull()) {
+    return out << "null";
+  } else {
+    ExprManagerScope ems(*e.getExprManager());
+    return out << e.getNode();
+  }
 }
 
 TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) throw() :

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index c332642f19f4593bc6e8ec53cae73817d49fc107..f90b5ff51b2af7912c51d167343015255f0a52b4 100644 (file)
--- 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 dea9adcf79cbe689a47961864819b68bf64b422a..e51a7bbb05578b2b3cf22dcf9cfb397bae5364c3 100644 (file)
--- 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 38fd3ab8b89b18656e3c616f2565bf3f70207a13..fb0ee808e517dac51e247d37b99d4225624e8966 100644 (file)
--- 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 92a339a45a8a43812cdf7269c85b2c92b55ee2c1..eaa1c1643bcbe2480002db43595510a4501e7f51 100644 (file)
--- 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 b6fb156f62cad61c7e85fe771b85b8232ec8511b..bbb0a95e96a7e7f5349af0868a9cd7a51dd7d11f 100644 (file)
--- 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

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 66f0c8824a07730cc57909269acb0b2591326e46..9a420ed024b62d75643422f0f1136050fc491e40 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -76,8 +76,11 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
 }
 
 Node TheoryModel::getModelValue( TNode n ) const{
-  Assert(n.getKind() != kind::FORALL && n.getKind() != kind::EXISTS && n.getKind() != kind::LAMBDA);
-  if( n.isConst() ) {
+  Assert(n.getKind() != kind::FORALL && n.getKind() != kind::EXISTS);
+  if(n.isConst()) {
+    return n;
+  }
+  if(n.getKind() == kind::LAMBDA) {
     return n;
   }
 

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 6af6fbf70d8965931cecc01861560555e2e75757..ffc9a420494cbc94aff571d79db42d6ce2ec9b2d 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -59,6 +59,7 @@ SMT2_TESTS = \
 CVC_TESTS = \
        boolean.cvc \
        boolean-prec.cvc \
+       boolean-terms.cvc \
        hole6.cvc \
        ite.cvc \
        let.cvc \

diff --git a/test/regress/regress0/boolean-terms.cvc b/test/regress/regress0/boolean-terms.cvc
new file mode 100644 (file)
index 0000000..5458f6c
--- /dev/null
+++ b/test/regress/regress0/boolean-terms.cvc
@@ -0,0 +1,16 @@
+% EXPECT: sat
+% EXIT: 10
+%OPTION "produce-models";
+
+f : BOOLEAN -> INT;
+x : INT;
+p : BOOLEAN -> BOOLEAN;
+
+ASSERT f(p(TRUE)) = x;
+ASSERT f(p(FALSE)) = x + 1;
+
+CHECKSAT;
+%GET_VALUE f(p(TRUE));
+%GET_VALUE f(p(TRUE)) = x;
+%GET_VALUE f(p(FALSE)) = x + 1;
+%COUNTERMODEL;