summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr_template.cpp8
-rw-r--r--src/smt/boolean_terms.cpp24
-rw-r--r--src/smt/boolean_terms.h7
-rw-r--r--src/smt/model_postprocessor.cpp3
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--src/smt/smt_engine.h2
-rw-r--r--src/theory/model.cpp7
-rw-r--r--test/regress/regress0/Makefile.am1
-rw-r--r--test/regress/regress0/boolean-terms.cvc16
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback