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.)
}
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() :
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;
}
return n;
}
}
- }/* else if(t.isRecord()) {
- Unimplemented();
- }*/
+ }
return top;
}
switch(k) {
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;
public:
+ BooleanTermConverter(SmtEngine& smt) :
+ d_smt(smt) {
+ }
+
/**
* We rewrite Boolean terms in assertions as bitvectors of length 1.
*/
**/
#include "smt/model_postprocessor.h"
+#include "smt/boolean_terms.h"
using namespace CVC4;
using namespace CVC4::smt;
}
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
d_assertionsToPreprocess(),
d_nonClausalLearnedLiterals(),
d_realAssertionsEnd(0),
- d_booleanTermConverter(),
+ d_booleanTermConverter(d_smt),
d_propagator(d_nonClausalLearnedLiterals, true, true),
d_assertionsToCheck(),
d_fakeContext(),
class SmtEngineStatistics;
class SmtEnginePrivate;
class SmtScope;
+ class BooleanTermConverter;
void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
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
}
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;
}
CVC_TESTS = \
boolean.cvc \
boolean-prec.cvc \
+ boolean-terms.cvc \
hole6.cvc \
ite.cvc \
let.cvc \
--- /dev/null
+% 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;