diff options
-rw-r--r-- | src/expr/expr_template.cpp | 8 | ||||
-rw-r--r-- | src/smt/boolean_terms.cpp | 24 | ||||
-rw-r--r-- | src/smt/boolean_terms.h | 7 | ||||
-rw-r--r-- | src/smt/model_postprocessor.cpp | 3 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 | ||||
-rw-r--r-- | src/theory/model.cpp | 7 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/boolean-terms.cvc | 16 |
9 files changed, 61 insertions, 9 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index bc7f0f47c..ed643b830 100644 --- 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 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 diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 66f0c8824..9a420ed02 100644 --- 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 6af6fbf70..ffc9a4204 100644 --- 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 index 000000000..5458f6c63 --- /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; |