diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-27 22:40:05 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-27 22:40:05 +0000 |
commit | 16d8379a9a87fe692c6f95a11300b43e4d2cba30 (patch) | |
tree | 7a97c484de035ff6268d2fc572a418cd8d48faca | |
parent | 551d1d37fe9c8ec25ddeac1e37b68d39158378ea (diff) |
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.)
-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; |