use -q. Previously, this would silence all output (including "sat" or
"unsat") as well. Now, single -q silences messages and warnings, and
double -qq silences all output (except on exception or signal).
+* Boolean term support in datatypes
--- Morgan Deters <mdeters@cs.nyu.edu> Wed, 20 Feb 2013 18:31:50 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu> Wed, 20 Mar 2013 20:03:50 -0400
("export of types belonging to theory of DATATYPES kinds unsupported");
}
if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
- n.getKind() != kind::SORT_TYPE) {
+ n.getKind() != kind::SORT_TYPE) {
throw ExportUnsupportedException
("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
}
operator Node();
operator Node() const;
+ // similarly for TypeNode
+ operator TypeNode();
+ operator TypeNode() const;
+
NodeBuilder<nchild_thresh>& operator&=(TNode);
NodeBuilder<nchild_thresh>& operator|=(TNode);
NodeBuilder<nchild_thresh>& operator+=(TNode);
return constructNode();
}
+template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator TypeNode() {
+ return constructTypeNode();
+}
+
+template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator TypeNode() const {
+ return constructTypeNode();
+}
+
template <unsigned nchild_thresh>
expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
Assert(!isUsed(), "NodeBuilder is one-shot only; "
if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
return true;
}
- if(isTuple() != t.isTuple() || isRecord() != t.isRecord() ||
- getNumChildren() != t.getNumChildren()) {
+ if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
return false;
}
- // children must be subtypes of t's, in order
- for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
- if(!(*i).isSubtypeOf(*j)) {
+ if(isTuple()) {
+ if(getNumChildren() != t.getNumChildren()) {
return false;
}
+ // children must be subtypes of t's, in order
+ for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
+ if(!(*i).isSubtypeOf(*j)) {
+ return false;
+ }
+ }
+ } else {
+ const Record& r1 = getConst<Record>();
+ const Record& r2 = t.getConst<Record>();
+ if(r1.getNumFields() != r2.getNumFields()) {
+ return false;
+ }
+ // r1's fields must be subtypes of r2's, in order
+ // names must match also
+ for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) {
+ if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) {
+ return false;
+ }
+ }
}
return true;
}
NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
return true;
}
- if(isTuple() != t.isTuple() || isRecord() != t.isRecord() ||
- getNumChildren() != t.getNumChildren()) {
+ if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
return false;
}
- // children must be comparable to t's, in order
- for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
- if(!(*i).isComparableTo(*j)) {
+ if(isTuple()) {
+ if(getNumChildren() != t.getNumChildren()) {
+ return false;
+ }
+ // children must be comparable to t's, in order
+ for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
+ if(!(*i).isComparableTo(*j)) {
+ return false;
+ }
+ }
+ } else {
+ const Record& r1 = getConst<Record>();
+ const Record& r2 = t.getConst<Record>();
+ if(r1.getNumFields() != r2.getNumFields()) {
return false;
}
+ // r1's fields must be comparable to r2's, in order
+ // names must match also
+ for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) {
+ if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) {
+ return false;
+ }
+ }
}
return true;
} else {
TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
if( options::modelUninterpDtEnum() && tn.isSort() &&
tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- out << "DATATYPE " << std::endl;
+ out << "DATATYPE" << std::endl;
out << " " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " = ";
for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
if (i>0) {
out << ',' << endl;
}
const Datatype& dt = (*i).getDatatype();
- out << " " << dt.getName() << " = ";
+ out << " " << dt.getName();
+ if(dt.isParametric()) {
+ out << '[';
+ for(size_t j = 0; j < dt.getNumParameters(); ++j) {
+ if(j > 0) {
+ out << ',';
+ }
+ out << dt.getParameter(j);
+ }
+ out << ']';
+ }
+ out << " = ";
bool firstConstructor = true;
for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
if(! firstConstructor) {
#include "smt/smt_engine.h"
#include "theory/theory_engine.h"
#include "theory/model.h"
+#include "theory/booleans/boolean_term_conversion_mode.h"
+#include "theory/booleans/options.h"
#include "expr/kind.h"
#include "util/hash.h"
#include "util/bool.h"
using namespace std;
using namespace CVC4::theory;
+using namespace CVC4::theory::booleans;
namespace CVC4 {
namespace smt {
+BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) :
+ d_smt(smt),
+ d_ff(),
+ d_tt(),
+ d_ffDt(),
+ d_ttDt(),
+ d_termCache(),
+ d_typeCache() {
+
+ // set up our "false" and "true" conversions based on command-line option
+ if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS ||
+ options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_NATIVE) {
+ d_ff = NodeManager::currentNM()->mkConst(BitVector(1u, 0u));
+ d_tt = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+ }
+ if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS) {
+ d_ffDt = d_ff;
+ d_ttDt = d_tt;
+ } else {
+ Datatype spec("BooleanTerm");
+ // don't change the order; false is assumed to come first by the model postprocessor
+ spec.addConstructor(DatatypeConstructor("BT_False"));
+ spec.addConstructor(DatatypeConstructor("BT_True"));
+ const Datatype& dt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(spec).getDatatype();
+ d_ffDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_False"].getConstructor()));
+ d_ttDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_True"].getConstructor()));
+ // mark this datatype type as being special for Boolean term conversion
+ TypeNode::fromType(dt.getDatatypeType()).setAttribute(BooleanTermAttr(), Node::null());
+ if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_DATATYPES) {
+ Assert(d_ff.isNull() && d_tt.isNull());
+ d_ff = d_ffDt;
+ d_tt = d_ttDt;
+ }
+ }
+
+ // assert that we set it up correctly
+ Assert(!d_ff.isNull() && !d_tt.isNull());
+ Assert(!d_ffDt.isNull() && !d_ttDt.isNull());
+ Assert(d_ff != d_tt);
+ Assert(d_ff.getType() == d_tt.getType());
+ Assert(d_ffDt != d_ttDt);
+ Assert(d_ffDt.getType() == d_ttDt.getType());
+
+}/* BooleanTermConverter::BooleanTermConverter() */
+
static inline bool isBoolean(TNode top, unsigned i) {
switch(top.getKind()) {
case kind::NOT:
}
}
-const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype& dt) throw() {
- return dt;
- // boolean terms not supported in datatypes, yet
+const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() {
+ const Datatype*& out = d_datatypeCache[&dt];
+ if(out != NULL) {
+ return *out;
+ }
- Debug("boolean-terms") << "booleanTermsConvertDatatype: considering " << dt.getName() << endl;
+ Debug("boolean-terms") << "convertDatatype: considering " << dt.getName() << endl;
for(Datatype::const_iterator c = dt.begin(); c != dt.end(); ++c) {
TypeNode t = TypeNode::fromType((*c).getConstructor().getType());
for(TypeNode::const_iterator a = t.begin(); a != t.end(); ++a) {
- if((*a).isBoolean()) {
- Datatype newDt(dt.getName() + "'");
+ TypeNode converted = convertType(*a, true);
+ Debug("boolean-terms") << "GOT: " << converted << ":" << converted.getId() << endl;
+ if(*a != converted) {
+ SortConstructorType mySelfType;
+ set<Type> unresolvedTypes;
+ if(dt.isParametric()) {
+ mySelfType = NodeManager::currentNM()->toExprManager()->mkSortConstructor(dt.getName() + "'", dt.getNumParameters());
+ unresolvedTypes.insert(mySelfType);
+ }
+ vector<Datatype> newDtVector;
+ if(dt.isParametric()) {
+ newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters()));
+ } else {
+ newDtVector.push_back(Datatype(dt.getName() + "'"));
+ }
+ Datatype& newDt = newDtVector.front();
Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl;
for(c = dt.begin(); c != dt.end(); ++c) {
DatatypeConstructor ctor((*c).getName() + "'", (*c).getTesterName() + "'");
t = TypeNode::fromType((*c).getConstructor().getType());
for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
- if((*a).getType().getRangeType().isBoolean()) {
- ctor.addArg((*a).getName() + "'", NodeManager::currentNM()->mkBitVectorType(1).toType());
- } else {
- Type argType = (*a).getType().getRangeType();
- if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) {
+ Type argType = (*a).getType().getRangeType();
+ if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) {
+ Debug("boolean-terms") << "argtype " << argType << " is self" << endl;
+ if(dt.isParametric()) {
+ Debug("boolean-terms") << "is-parametric self is " << mySelfType << endl;
+ ctor.addArg((*a).getName() + "'", mySelfType.instantiate(DatatypeType(argType).getDatatype().getParameters()));
+ } else {
ctor.addArg((*a).getName() + "'", DatatypeSelfType());
+ }
+ } else {
+ Debug("boolean-terms") << "argtype " << argType << " is NOT self" << endl;
+ converted = convertType(TypeNode::fromType(argType), true);
+ if(TypeNode::fromType(argType) != converted) {
+ ctor.addArg((*a).getName() + "'", converted.toType());
} else {
ctor.addArg((*a).getName() + "'", argType);
}
}
newDt.addConstructor(ctor);
}
- DatatypeType newDtt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(newDt);
+ vector<DatatypeType> newDttVector =
+ NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes);
+ DatatypeType& newDtt = newDttVector.front();
const Datatype& newD = newDtt.getDatatype();
for(c = dt.begin(); c != dt.end(); ++c) {
Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl;
- d_booleanTermCache[make_pair(Node::fromExpr((*c).getConstructor()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
- d_booleanTermCache[make_pair(Node::fromExpr((*c).getTester()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
+ Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr?
+ Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl;
+ d_termCache[make_pair(Node::fromExpr((*c).getConstructor()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
+ d_termCache[make_pair(Node::fromExpr((*c).getTester()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
- d_booleanTermCache[make_pair(Node::fromExpr((*a).getSelector()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
+ d_termCache[make_pair(Node::fromExpr((*a).getSelector()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
}
}
+ out = &newD;
return newD;
}
}
}
+
+ out = &dt;
return dt;
-}/* BooleanTermConverter::booleanTermsConvertDatatype() */
+
+}/* BooleanTermConverter::convertDatatype() */
+
+TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext) {
+ Debug("boolean-terms") << "CONVERT-TYPE[" << type << ":" << type.getId() << ", " << datatypesContext << "]" << endl;
+ // This function recursively converts the type.
+ if(type.isBoolean()) {
+ return datatypesContext ? d_ttDt.getType() : d_tt.getType();
+ }
+ const pair<TypeNode, bool> cacheKey(type, datatypesContext);
+ if(d_typeCache.find(cacheKey) != d_typeCache.end()) {
+ TypeNode out = d_typeCache[cacheKey];
+ return out.isNull() ? type : out;
+ }
+ TypeNode& outNode = d_typeCache[cacheKey];
+ if(type.getKind() == kind::DATATYPE_TYPE ||
+ type.getKind() == kind::PARAMETRIC_DATATYPE) {
+ bool parametric = (type.getKind() == kind::PARAMETRIC_DATATYPE);
+ const Datatype& dt = parametric ? type[0].getConst<Datatype>() : type.getConst<Datatype>();
+ TypeNode out = TypeNode::fromType(convertDatatype(dt).getDatatypeType());
+ Debug("boolean-terms") << "AFTER, got "<< out << " param:" << parametric << endl;
+ if(parametric) {
+ // re-parameterize the translation
+ vector<TypeNode> params = type.getParamTypes();
+ for(size_t i = 0; i < params.size(); ++i) {
+ Debug("boolean-terms") << "in loop, got "<< params[i] << endl;
+ params[i] = convertType(params[i], true);
+ Debug("boolean-terms") << "in loop, convert to "<< params[i] << endl;
+ }
+ params.insert(params.begin(), out[0]);
+ out = NodeManager::currentNM()->mkTypeNode(kind::PARAMETRIC_DATATYPE, params);
+ Debug("boolean-terms") << "got OUT: " << out << endl;
+ }
+ if(out != type) {
+ outNode = out;// cache it
+ Debug("boolean-terms") << "OUT is same as TYPE" << endl;
+ } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl;
+ return out;
+ }
+ if(type.isRecord()) {
+ const Record& rec = type.getConst<Record>();
+ vector< pair<string, Type> > flds;
+ for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) {
+ TypeNode converted = convertType(TypeNode::fromType((*i).second), true);
+ if(TypeNode::fromType((*i).second) != converted) {
+ flds.push_back(make_pair((*i).first, converted.toType()));
+ } else {
+ flds.push_back(*i);
+ }
+ }
+ TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds));
+ Debug("tuprec") << "converted " << type << " to " << newRec << endl;
+ if(newRec != type) {
+ outNode = newRec;// cache it
+ }
+ return newRec;
+ }
+ if(type.getNumChildren() > 0) {
+ Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl;
+ // This should handle tuples and arrays ok.
+ // Might handle function types too, but they can't go
+ // in other types, so it doesn't matter.
+ NodeBuilder<> b(type.getKind());
+ if(type.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ b << type.getOperator();
+ }
+ for(TypeNode::iterator i = type.begin(); i != type.end(); ++i) {
+ b << convertType(*i, false);
+ }
+ TypeNode out = b;
+ if(out != type) {
+ outNode = out;// cache it
+ }
+ Debug("boolean-terms") << "here at B, returning " << out << ":" << out.getId() << endl;
+ return out;
+ }
+ // leave the cache at Null
+ return type;
+}/* BooleanTermConverter::convertType() */
// look for vars from "vars" that occur in a term-context in n; transfer them to output.
static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TNode>& output, bool boolParent, std::hash_set< std::pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> >& alreadySeen) {
}
}
-Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, std::map<TNode, Node>& quantBoolVars) throw() {
- Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - boolParent=" << boolParent << endl;
+Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw() {
+ Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl;
+
+ // we only distinguish between datatypes, booleans, and "other", and we
+ // don't even distinguish datatypes except when in "native" conversion
+ // mode
+ if(parentTheory != theory::THEORY_BOOL) {
+ if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE ||
+ parentTheory != theory::THEORY_DATATYPES) {
+ parentTheory = theory::THEORY_BUILTIN;
+ }
+ }
- BooleanTermCache::iterator i = d_booleanTermCache.find(make_pair<Node, bool>(top, boolParent));
- if(i != d_booleanTermCache.end()) {
+ BooleanTermCache::iterator i = d_termCache.find(make_pair<Node, theory::TheoryId>(top, parentTheory));
+ if(i != d_termCache.end()) {
return (*i).second.isNull() ? Node(top) : (*i).second;
}
NodeManager* nm = NodeManager::currentNM();
- Node one = nm->mkConst(BitVector(1u, 1u));
- Node zero = nm->mkConst(BitVector(1u, 0u));
-
if(quantBoolVars.find(top) != quantBoolVars.end()) {
// this Bool variable is quantified over and we're changing it to a BitVector var
- if(boolParent) {
- return quantBoolVars[top].eqNode(one);
+ if(parentTheory == theory::THEORY_BOOL) {
+ return quantBoolVars[top].eqNode(d_tt);
} else {
return quantBoolVars[top];
}
}
- if(!boolParent && top.getType().isBoolean()) {
+ if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) {
// still need to rewrite e.g. function applications over boolean
- Node topRewritten = rewriteBooleanTermsRec(top, true, quantBoolVars);
- Node n = nm->mkNode(kind::ITE, topRewritten, one, zero);
+ Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars);
+ Node n;
+ if(parentTheory == theory::THEORY_DATATYPES) {
+ n = nm->mkNode(kind::ITE, topRewritten, d_ttDt, d_ffDt);
+ } else {
+ n = nm->mkNode(kind::ITE, topRewritten, d_tt, d_ff);
+ }
Debug("boolean-terms") << "constructed ITE: " << n << endl;
return n;
}
if(constituentType.isBoolean()) {
// we have store_all(true) or store_all(false)
// just turn it into store_all(1) or store_all(0)
- Node newConst = nm->mkConst(BitVector(1u, asa.getExpr().getConst<bool>() ? 1u : 0u));
if(indexType.isBoolean()) {
// change index type to BV(1) also
- indexType = nm->mkBitVectorType(1);
+ indexType = d_tt.getType();
}
- ArrayStoreAll asaRepl(nm->mkArrayType(indexType, nm->mkBitVectorType(1)).toType(), newConst.toExpr());
+ ArrayStoreAll asaRepl(nm->mkArrayType(indexType, d_tt.getType()).toType(),
+ (asa.getExpr().getConst<bool>() ? d_tt : d_ff).toExpr());
Node n = nm->mkConst(asaRepl);
Debug("boolean-terms") << " returning new store_all: " << n << endl;
return n;
}
if(indexType.isBoolean()) {
// must change index type to BV(1)
- indexType = nm->mkBitVectorType(1);
+ indexType = d_tt.getType();
ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr());
Node n = nm->mkConst(asaRepl);
Debug("boolean-terms") << " returning new store_all: " << n << endl;
TypeNode t = top.getType();
if(t.isFunction()) {
for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) {
- if(t[i].isBoolean()) {
+ TypeNode newType = convertType(t[i], false);
+ if(newType != t[i]) {
vector<TypeNode> argTypes = t.getArgTypes();
- replace(argTypes.begin(), argTypes.end(), t[i], nm->mkBitVectorType(1));
+ replace(argTypes.begin(), argTypes.end(), t[i], d_tt.getType());
TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType());
Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__",
newType, "a function introduced by Boolean-term conversion",
Node var = nm->mkBoundVar(t[j]);
boundVarsBuilder << var;
if(t[j].isBoolean()) {
- bodyBuilder << nm->mkNode(kind::ITE, var, one, zero);
+ bodyBuilder << nm->mkNode(kind::ITE, var, d_tt, d_ff);
} else {
bodyBuilder << var;
}
Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
- d_booleanTermCache[make_pair(top, boolParent)] = n;
+ d_termCache[make_pair(top, parentTheory)] = n;
return n;
}
}
} else if(t.isArray()) {
- TypeNode indexType = t.getArrayIndexType();
- TypeNode constituentType = t.getArrayConstituentType();
- bool rewrite = false;
- if(indexType.isBoolean()) {
- indexType = nm->mkBitVectorType(1);
- rewrite = true;
- }
- if(constituentType.isBoolean()) {
- constituentType = nm->mkBitVectorType(1);
- rewrite = true;
- }
- if(rewrite) {
+ TypeNode indexType = convertType(t.getArrayIndexType(), false);
+ TypeNode constituentType = convertType(t.getArrayConstituentType(), false);
+ if(indexType != t.getArrayIndexType() || constituentType != t.getArrayConstituentType()) {
TypeNode newType = nm->mkArrayType(indexType, constituentType);
- Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
+ Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
newType, "an array variable introduced by Boolean-term conversion",
NodeManager::SKOLEM_EXACT_NAME);
top.setAttribute(BooleanTermAttr(), n);
Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
- Node n_zero = nm->mkNode(kind::SELECT, n, zero);
- Node n_one = nm->mkNode(kind::SELECT, n, one);
+ Node n_ff = nm->mkNode(kind::SELECT, n, d_ff);
+ Node n_tt = nm->mkNode(kind::SELECT, n, d_tt);
Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr()));
Node repl = nm->mkNode(kind::STORE,
nm->mkNode(kind::STORE, base, nm->mkConst(false),
- nm->mkNode(kind::EQUAL, n_zero, one)), nm->mkConst(true),
- nm->mkNode(kind::EQUAL, n_one, one));
+ nm->mkNode(kind::EQUAL, n_ff, d_tt)), nm->mkConst(true),
+ nm->mkNode(kind::EQUAL, n_tt, d_tt));
Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
- d_booleanTermCache[make_pair(top, boolParent)] = n;
+ d_termCache[make_pair(top, parentTheory)] = n;
return n;
}
- d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+ d_termCache[make_pair(top, parentTheory)] = Node::null();
return top;
- } else if(t.isTuple()) {
- return top;
- } else if(t.isRecord()) {
+ } else if(t.isTuple() || t.isRecord()) {
+ TypeNode newType = convertType(t, true);
+ if(t != newType) {
+ Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
+ newType, "a tuple/record variable introduced by Boolean-term conversion",
+ NodeManager::SKOLEM_EXACT_NAME);
+ top.setAttribute(BooleanTermAttr(), n);
+ n.setAttribute(BooleanTermAttr(), top);
+ Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
+ d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
+ Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+ d_termCache[make_pair(top, parentTheory)] = n;
+ return n;
+ }
+ d_termCache[make_pair(top, parentTheory)] = Node::null();
return top;
- } else if(t.isDatatype()) {
- return top;// no support for datatypes at present
- const Datatype& dt = t.getConst<Datatype>();
- const Datatype& dt2 = booleanTermsConvertDatatype(dt);
- if(dt != dt2) {
- Assert(d_booleanTermCache.find(make_pair(top, boolParent)) == d_booleanTermCache.end(),
+ } else if(t.isDatatype() || t.isParametricDatatype()) {
+ Debug("boolean-terms") << "found a var of datatype type" << endl;
+ TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
+ if(t != newT) {
+ Assert(d_termCache.find(make_pair(top, parentTheory)) == d_termCache.end(),
"Node `%s' already in cache ?!", top.toString().c_str());
- Assert(top.isVar());
- TypeNode newType = TypeNode::fromType(dt2.getDatatypeType());
- Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
- newType, "an array variable introduced by Boolean-term conversion",
+ Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
+ newT, "a datatype variable introduced by Boolean-term conversion",
NodeManager::SKOLEM_EXACT_NAME);
+ Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
top.setAttribute(BooleanTermAttr(), n);
- Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
- d_booleanTermCache[make_pair(top, boolParent)] = n;
+ d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
+ Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl;
+ d_termCache[make_pair(top, parentTheory)] = n;
return n;
} else {
- d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+ d_termCache[make_pair(top, parentTheory)] = Node::null();
return top;
}
} else if(t.isConstructor()) {
- return top;// no support for datatypes at present
- Assert(!boolParent);
- const Datatype& dt = t[t.getNumChildren() - 1].getConst<Datatype>();
- const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+ Assert(parentTheory != theory::THEORY_BOOL);
+ Assert(t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ||
+ t[t.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE);
+ const Datatype& dt = t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ?
+ t[t.getNumChildren() - 1].getConst<Datatype>() :
+ t[t.getNumChildren() - 1][0].getConst<Datatype>();
+ TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
+ const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
if(dt != dt2) {
- Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(),
+ Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
"constructor `%s' not in cache", top.toString().c_str());
- return d_booleanTermCache[make_pair(top, boolParent)];
- } else {
- d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
- return top;
+ return d_termCache[make_pair(top, parentTheory)];
}
+ d_termCache[make_pair(top, parentTheory)] = Node::null();
+ return top;
} else if(t.isTester() || t.isSelector()) {
- return top;// no support for datatypes at present
- Assert(!boolParent);
- const Datatype& dt = t[0].getConst<Datatype>();
- const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+ Assert(parentTheory != theory::THEORY_BOOL);
+ const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ?
+ t[0].getConst<Datatype>() :
+ t[0][0].getConst<Datatype>();
+ TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
+ const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
if(dt != dt2) {
- Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(),
+ Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
"tester or selector `%s' not in cache", top.toString().c_str());
- return d_booleanTermCache[make_pair(top, boolParent)];
+ return d_termCache[make_pair(top, parentTheory)];
} else {
- d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+ d_termCache[make_pair(top, parentTheory)] = Node::null();
return top;
}
} else if(t.getNumChildren() > 0) {
for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
if((*i).isBoolean()) {
vector<TypeNode> argTypes(t.begin(), t.end());
- replace(argTypes.begin(), argTypes.end(), *i, nm->mkBitVectorType(1));
+ replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType());
TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
newType, "a variable introduced by Boolean-term conversion",
NodeManager::SKOLEM_EXACT_NAME);
Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
top.setAttribute(BooleanTermAttr(), n);
- d_booleanTermCache[make_pair(top, boolParent)] = n;
+ d_termCache[make_pair(top, parentTheory)] = n;
return n;
}
}
}
}
Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars);
- Node body = rewriteBooleanTermsRec(top[1], true, quantBoolVars);
+ Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars);
Node quant = nm->mkNode(top.getKind(), boundVarList, body);
Debug("bt") << "rewrote quantifier to -> " << quant << endl;
- d_booleanTermCache[make_pair(top, true)] = quant;
- d_booleanTermCache[make_pair(top, false)] = quant.iteNode(one, zero);
+ d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant;
+ d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff);
+ d_termCache[make_pair(top, theory::THEORY_DATATYPES)] = quant.iteNode(d_tt, d_ff);
return quant;
}
}
NodeBuilder<> b(k);
Debug("bt") << "looking at: " << top << endl;
if(mk == kind::metakind::PARAMETERIZED) {
- if(kindToTheoryId(k) != THEORY_BV &&
- k != kind::APPLY_TYPE_ASCRIPTION &&
- k != kind::TUPLE_SELECT &&
- k != kind::TUPLE_UPDATE &&
- k != kind::RECORD_SELECT &&
- k != kind::RECORD_UPDATE &&
- k != kind::RECORD) {
+ if(k == kind::RECORD) {
+ b << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES);
+ } else if(k == kind::APPLY_TYPE_ASCRIPTION) {
+ Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
+ b << asc;
+ Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl;
+ asc.setAttribute(BooleanTermAttr(), top.getOperator());
+ } else if(kindToTheoryId(k) != THEORY_BV &&
+ k != kind::TUPLE_SELECT &&
+ k != kind::TUPLE_UPDATE &&
+ k != kind::RECORD_SELECT &&
+ k != kind::RECORD_UPDATE) {
Debug("bt") << "rewriting: " << top.getOperator() << endl;
- b << rewriteBooleanTermsRec(top.getOperator(), false, quantBoolVars);
+ b << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
Debug("bt") << "got: " << b.getOperator() << endl;
} else {
b << top.getOperator();
}
for(unsigned i = 0; i < top.getNumChildren(); ++i) {
Debug("bt") << "rewriting: " << top[i] << endl;
- b << rewriteBooleanTermsRec(top[i], isBoolean(top, i), quantBoolVars);
+ b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars);
Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
}
Node n = b;
Debug("boolean-terms") << "constructed: " << n << endl;
- if(boolParent &&
- n.getType().isBitVector() &&
- n.getType().getBitVectorSize() == 1) {
- n = nm->mkNode(kind::EQUAL, n, one);
+ if(parentTheory == theory::THEORY_BOOL) {
+ if(n.getType().isBitVector() &&
+ n.getType().getBitVectorSize() == 1) {
+ n = nm->mkNode(kind::EQUAL, n, d_tt);
+ } else if(n.getType().isDatatype() &&
+ n.getType().hasAttribute(BooleanTermAttr())) {
+ n = nm->mkNode(kind::EQUAL, n, d_ttDt);
+ }
}
- d_booleanTermCache[make_pair(top, boolParent)] = n;
+ d_termCache[make_pair(top, parentTheory)] = n;
return n;
}
}/* BooleanTermConverter::rewriteBooleanTermsRec() */
class BooleanTermConverter {
/** The type of the Boolean term conversion cache */
- typedef std::hash_map< std::pair<Node, bool>, Node,
+ typedef std::hash_map< std::pair<Node, theory::TheoryId>, Node,
PairHashFunction< Node, bool,
- NodeHashFunction, std::hash<int> > > BooleanTermCache;
+ NodeHashFunction, std::hash<size_t> > > BooleanTermCache;
+ /** The type of the Boolean term conversion type cache */
+ typedef std::hash_map< std::pair<TypeNode, bool>, TypeNode,
+ PairHashFunction< TypeNode, bool,
+ TypeNodeHashFunction, std::hash<int> > > BooleanTermTypeCache;
+ /** The type of the Boolean term conversion datatype cache */
+ typedef std::hash_map<const Datatype*, const Datatype*, DatatypeHashFunction> BooleanTermDatatypeCache;
/** The SmtEngine to which we're associated */
SmtEngine& d_smt;
+ /** The conversion for "false." */
+ Node d_ff;
+ /** The conversion for "true." */
+ Node d_tt;
+ /** The conversion for "false" when in datatypes contexts. */
+ Node d_ffDt;
+ /** The conversion for "true" when in datatypes contexts. */
+ Node d_ttDt;
+
/** The cache used during Boolean term conversion */
- BooleanTermCache d_booleanTermCache;
+ BooleanTermCache d_termCache;
+ /** The cache used during Boolean term type conversion */
+ BooleanTermTypeCache d_typeCache;
+ /** The cache used during Boolean term datatype conversion */
+ BooleanTermDatatypeCache d_datatypeCache;
/**
* Scan a datatype for and convert as necessary.
*/
- const Datatype& booleanTermsConvertDatatype(const Datatype& dt) throw();
+ const Datatype& convertDatatype(const Datatype& dt) throw();
+
+ /**
+ * Convert a type.
+ */
+ TypeNode convertType(TypeNode type, bool datatypesContext);
- Node rewriteBooleanTermsRec(TNode n, bool boolParent, std::map<TNode, Node>& quantBoolVars) throw();
+ Node rewriteBooleanTermsRec(TNode n, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw();
public:
- BooleanTermConverter(SmtEngine& smt) :
- d_smt(smt) {
- }
+ /**
+ * Construct a Boolean-term converter associated to the given
+ * SmtEngine.
+ */
+ BooleanTermConverter(SmtEngine& smt);
/**
- * We rewrite Boolean terms in assertions as bitvectors of length 1.
+ * Rewrite Boolean terms under a node. The node itself is not converted
+ * if boolParent is true, but its Boolean subterms appearing in a
+ * non-Boolean context will be rewritten.
*/
- Node rewriteBooleanTerms(TNode n, bool boolParent = true) throw() {
+ Node rewriteBooleanTerms(TNode n, bool boolParent = true, bool dtParent = false) throw() {
std::map<TNode, Node> quantBoolVars;
- return rewriteBooleanTermsRec(n, boolParent, quantBoolVars);
+ Assert(!(boolParent && dtParent));
+ return rewriteBooleanTermsRec(n, boolParent ? theory::THEORY_BOOL : (dtParent ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars);
}
};/* class BooleanTermConverter */
#include "smt/model_postprocessor.h"
#include "smt/boolean_terms.h"
+using namespace std;
using namespace CVC4;
using namespace CVC4::smt;
+Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
+ if(n.getType().isSubtypeOf(asType)) {
+ // good to go, we have the right type
+ return n;
+ }
+ if(!n.isConst()) {
+ // we don't handle non-const right now
+ return n;
+ }
+ if(asType.isBoolean()) {
+ if(n.getType().isBitVector(1u)) {
+ // type mismatch: should only happen for Boolean-term conversion under
+ // datatype constructor applications; rewrite from BV(1) back to Boolean
+ bool tf = (n.getConst<BitVector>().getValue() == 1);
+ return NodeManager::currentNM()->mkConst(tf);
+ }
+ if(n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())) {
+ // type mismatch: should only happen for Boolean-term conversion under
+ // datatype constructor applications; rewrite from datatype back to Boolean
+ Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
+ Assert(n.getNumChildren() == 0);
+ // we assume (by construction) false is first; see boolean_terms.cpp
+ bool tf = (Datatype::indexOf(n.getOperator().toExpr()) == 1);
+ Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << " ==> " << tf << endl;
+ return NodeManager::currentNM()->mkConst(tf);
+ }
+ }
+ Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl;
+ if(n.getType().isArray()) {
+ Assert(asType.isArray());
+ if(n.getKind() == kind::STORE) {
+ return NodeManager::currentNM()->mkNode(kind::STORE,
+ rewriteAs(n[0], asType),
+ rewriteAs(n[1], asType[0]),
+ rewriteAs(n[2], asType[1]));
+ }
+ Assert(n.getKind() == kind::STORE_ALL);
+ const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
+ Node val = rewriteAs(asa.getExpr(), asType[1]);
+ return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr()));
+ }
+ if(asType.getNumChildren() != n.getNumChildren() ||
+ n.getMetaKind() == kind::metakind::CONSTANT) {
+ return n;
+ }
+ NodeBuilder<> b(n.getKind());
+ TypeNode::iterator t = asType.begin();
+ for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) {
+ Assert(t != asType.end());
+ b << rewriteAs(*i, *t);
+ }
+ Assert(t == asType.end());
+ Debug("boolean-terms") << "+++ constructing " << b << endl;
+ Node out = b;
+ return out;
+}
+
void ModelPostprocessor::visit(TNode current, TNode parent) {
- Debug("tuprec") << "visiting " << current << std::endl;
+ Debug("tuprec") << "visiting " << current << endl;
Assert(!alreadyVisited(current, TNode::null()));
if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) {
Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
+ TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr());
NodeBuilder<> b(kind::TUPLE);
- for(TNode::iterator i = current.begin(); i != current.end(); ++i) {
+ TypeNode::iterator t = expectType.begin();
+ for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
Assert(alreadyVisited(*i, TNode::null()));
+ Assert(t != expectType.end());
TNode n = d_nodes[*i];
- b << (n.isNull() ? *i : n);
+ n = n.isNull() ? *i : n;
+ if(!n.getType().isSubtypeOf(*t)) {
+ Assert(n.getType().isBitVector(1u) ||
+ (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
+ Assert(n.isConst());
+ Assert((*t).isBoolean());
+ if(n.getType().isBitVector(1u)) {
+ b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
+ } else {
+ // we assume (by construction) false is first; see boolean_terms.cpp
+ b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
+ }
+ } else {
+ b << n;
+ }
}
+ Assert(t == expectType.end());
d_nodes[current] = b;
- Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
+ Debug("tuprec") << "returning " << d_nodes[current] << endl;
+ Assert(d_nodes[current].getType() == expectType);
} else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) {
Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
+ TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr());
+ const Record& expectRec = expectType.getConst<Record>();
NodeBuilder<> b(kind::RECORD);
b << current.getType().getAttribute(expr::DatatypeRecordAttr());
- for(TNode::iterator i = current.begin(); i != current.end(); ++i) {
+ Record::const_iterator t = expectRec.begin();
+ for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
Assert(alreadyVisited(*i, TNode::null()));
+ Assert(t != expectRec.end());
TNode n = d_nodes[*i];
- b << (n.isNull() ? *i : n);
+ n = n.isNull() ? *i : n;
+ if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) {
+ Assert(n.getType().isBitVector(1u) ||
+ (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
+ Assert(n.isConst());
+ Assert((*t).second.isBoolean());
+ if(n.getType().isBitVector(1u)) {
+ b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
+ } else {
+ // we assume (by construction) false is first; see boolean_terms.cpp
+ b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
+ }
+ } else {
+ b << n;
+ }
}
+ Assert(t == expectRec.end());
d_nodes[current] = b;
- Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
+ Debug("tuprec") << "returning " << d_nodes[current] << endl;
+ Assert(d_nodes[current].getType() == expectType);
+ } else if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
+ ( current.getOperator().hasAttribute(BooleanTermAttr()) ||
+ ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION &&
+ current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) {
+ NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
+ Node realOp;
+ if(current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION) {
+ TNode oldAsc = current.getOperator().getOperator();
+ Debug("boolean-terms") << "old asc: " << oldAsc << endl;
+ Node newCons = current.getOperator()[0].getAttribute(BooleanTermAttr());
+ Node newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().toType()));
+ Debug("boolean-terms") << "new asc: " << newAsc << endl;
+ if(newCons.getType().getRangeType().isParametricDatatype()) {
+ vector<TypeNode> oldParams = TypeNode::fromType(oldAsc.getConst<AscriptionType>().getType()).getRangeType().getParamTypes();
+ vector<TypeNode> newParams = newCons.getType().getRangeType().getParamTypes();
+ Assert(oldParams.size() == newParams.size() && oldParams.size() > 0);
+ newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().substitute(newParams.begin(), newParams.end(), oldParams.begin(), oldParams.end()).toType()));
+ }
+ realOp = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, newAsc, newCons);
+ } else {
+ realOp = current.getOperator().getAttribute(BooleanTermAttr());
+ }
+ b << realOp;
+ Debug("boolean-terms") << "+ op " << b.getOperator() << endl;
+ TypeNode::iterator j = realOp.getType().begin();
+ for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++j) {
+ Assert(j != realOp.getType().end());
+ Assert(alreadyVisited(*i, TNode::null()));
+ TNode repl = d_nodes[*i];
+ repl = repl.isNull() ? *i : repl;
+ Debug("boolean-terms") << "+ adding " << repl << " expecting " << *j << endl;
+ b << rewriteAs(repl, *j);
+ }
+ Node n = b;
+ Debug("boolean-terms") << "model-post: " << current << endl
+ << "- returning " << n << endl;
+ d_nodes[current] = n;
} else {
- Debug("tuprec") << "returning self" << std::endl;
+ Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
// rewrite to self
d_nodes[current] = Node::null();
}
}/* ModelPostprocessor::visit() */
-
namespace smt {
class ModelPostprocessor {
+ std::hash_map<TNode, Node, TNodeHashFunction> d_nodes;
+
public:
typedef Node return_type;
- std::hash_map<TNode, Node, TNodeHashFunction> d_nodes;
+
+ Node rewriteAs(TNode n, TypeNode asType);
bool alreadyVisited(TNode current, TNode parent) {
return d_nodes.find(current) != d_nodes.end();
#include "theory/logic_info.h"
#include "theory/options.h"
#include "theory/booleans/circuit_propagator.h"
+#include "theory/booleans/boolean_term_conversion_mode.h"
+#include "theory/booleans/options.h"
#include "util/ite_removal.h"
#include "theory/model.h"
#include "printer/printer.h"
d_cumulativeTimeUsed(0),
d_cumulativeResourceUsed(0),
d_status(),
- d_private(new smt::SmtEnginePrivate(*this)),
- d_statisticsRegistry(new StatisticsRegistry()),
+ d_private(NULL),
+ d_statisticsRegistry(NULL),
d_stats(NULL) {
SmtScope smts(this);
+ d_private = new smt::SmtEnginePrivate(*this);
+ d_statisticsRegistry = new StatisticsRegistry();
d_stats = new SmtEngineStatistics();
// We have mutual dependency here, so we add the prop engine to the theory
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
Node n = d_booleanTermConverter.rewriteBooleanTerms(d_assertionsToPreprocess[i]);
- if(n != d_assertionsToPreprocess[i] && !d_smt.d_logic.isTheoryEnabled(theory::THEORY_BV)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(theory::THEORY_BV);
- d_smt.d_logic.lock();
+ if(n != d_assertionsToPreprocess[i]) {
+ switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) {
+ case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
+ case booleans::BOOLEAN_TERM_CONVERT_NATIVE:
+ if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_BV)) {
+ d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+ d_smt.d_logic.enableTheory(theory::THEORY_BV);
+ d_smt.d_logic.lock();
+ }
+ break;
+ case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
+ if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
+ d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+ d_smt.d_logic.enableTheory(theory::THEORY_DATATYPES);
+ d_smt.d_logic.lock();
+ }
+ break;
+ default:
+ Unhandled(mode);
+ }
}
d_assertionsToPreprocess[i] = n;
}
return quickCheck().asValidityResult();
}
-Node SmtEngine::postprocess(TNode node) {
+Node SmtEngine::postprocess(TNode node, TypeNode expectedType) {
ModelPostprocessor mpost;
NodeVisitor<ModelPostprocessor> visitor;
- return visitor.run(mpost, node);
+ Node value = visitor.run(mpost, node);
+ Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl;
+ Node realValue = mpost.rewriteAs(value, expectedType);
+ Debug("boolean-terms") << "postproc: realval " << realValue << " expect type " << expectedType << endl;
+ return realValue;
}
Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) {
// Make sure all preprocessing is done
d_private->processAssertions();
Node n = d_private->simplify(Node::fromExpr(e));
- n = postprocess(n);
+ n = postprocess(n, TypeNode::fromType(e.getType()));
return n.toExpr();
}
}
hash_map<Node, Node, NodeHashFunction> cache;
Node n = d_private->expandDefinitions(Node::fromExpr(e), cache);
- n = postprocess(n);
+ n = postprocess(n, TypeNode::fromType(e.getType()));
return n.toExpr();
}
resultNode = m->getValue(n);
}
Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
- resultNode = postprocess(resultNode);
+ resultNode = postprocess(resultNode, n.getType());
Trace("smt") << "--- model-post returned " << resultNode << endl;
+ Trace("smt") << "--- model-post returned " << resultNode.getType() << endl;
+ Trace("smt") << "--- model-post expected " << n.getType() << endl;
// type-check the result we got
Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType()));
// function symbol (since then the definition is recursive)
if (val.getKind() == kind::LAMBDA) {
// first apply the model substitutions we have so far
+ Debug("boolean-terms") << "applying subses to " << val[1] << endl;
Node n = substitutions.apply(val[1]);
+ Debug("boolean-terms") << "++ got " << n << endl;
// now check if n contains func by doing a substitution
// [func->func2] and checking equality of the Nodes.
// (this just a way to check if func is in n.)
}
// (3) checks complete, add the substitution
+ Debug("boolean-terms") << "cm: adding subs " << func << " :=> " << val << endl;
substitutions.addSubstitution(func, val);
}
}
Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
// Apply our model value substitutions.
+ Debug("boolean-terms") << "applying subses to " << n << endl;
n = substitutions.apply(n);
+ Debug("boolean-terms") << "++ got " << n << endl;
Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl;
// Simplify the result.
* like turning datatypes back into tuples, length-1-bitvectors back
* into booleans, etc.
*/
- Node postprocess(TNode n);
+ Node postprocess(TNode n, TypeNode expectedType);
/**
* This is something of an "init" procedure, but is idempotent; call
theory_bool_rewriter.h \
theory_bool_rewriter.cpp \
circuit_propagator.h \
- circuit_propagator.cpp
+ circuit_propagator.cpp \
+ boolean_term_conversion_mode.h \
+ boolean_term_conversion_mode.cpp
EXTRA_DIST = \
- kinds
+ kinds \
+ options_handlers.h
--- /dev/null
+/********************* */
+/*! \file boolean_term_conversion_mode.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <iostream>
+#include "theory/booleans/boolean_term_conversion_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) {
+ switch(mode) {
+ case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
+ out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS";
+ break;
+ case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
+ out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES";
+ break;
+ case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE:
+ out << "BOOLEAN_TERM_CONVERT_NATIVE";
+ break;
+ default:
+ out << "BooleanTermConversionMode!UNKNOWN";
+ }
+
+ return out;
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file boolean_term_conversion_mode.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
+#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+typedef enum {
+ /**
+ * Convert Boolean terms to bitvectors of size 1.
+ */
+ BOOLEAN_TERM_CONVERT_TO_BITVECTORS,
+ /**
+ * Convert Boolean terms to enumerations in the Datatypes theory.
+ */
+ BOOLEAN_TERM_CONVERT_TO_DATATYPES,
+ /**
+ * Convert Boolean terms to enumerations in the Datatypes theory IF
+ * used in a datatypes context, otherwise to a bitvector of size 1.
+ */
+ BOOLEAN_TERM_CONVERT_NATIVE
+
+} BooleanTermConversionMode;
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */
module BOOLEANS "theory/booleans/options.h" Boolean theory
+option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "theory/booleans/boolean_term_conversion_mode.h" :handler CVC4::theory::booleans::stringToBooleanTermConversionMode :handler-include "theory/booleans/options_handlers.h"
+ policy for converting Boolean terms
+
endmodule
--- /dev/null
+/********************* */
+/*! \file options_handlers.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H
+
+#include <string>
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+static const std::string booleanTermConversionModeHelp = "\
+Boolean term conversion modes currently supported by the\n\
+--boolean-term-conversion-mode option:\n\
+\n\
+bitvectors [default]\n\
++ Boolean terms are converted to bitvectors of size 1.\n\
+\n\
+datatypes\n\
++ Boolean terms are converted to enumerations in the Datatype theory.\n\
+\n\
+native\n\
++ Boolean terms are converted in a \"natural\" way depending on where they\n\
+ are used. If in a datatype context, they are converted to an enumeration.\n\
+ Elsewhere, they are converted to a bitvector of size 1.\n\
+";
+
+inline BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ if(optarg == "bitvectors") {
+ return BOOLEAN_TERM_CONVERT_TO_BITVECTORS;
+ } else if(optarg == "datatypes") {
+ return BOOLEAN_TERM_CONVERT_TO_DATATYPES;
+ } else if(optarg == "native") {
+ return BOOLEAN_TERM_CONVERT_NATIVE;
+ } else if(optarg == "help") {
+ puts(booleanTermConversionModeHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") +
+ optarg + "'. Try --boolean-term-conversion-mode help.");
+ }
+}
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H */
if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) {
std::stringstream ss;
- ss << "Subtypes must have a common type:" << std::endl;
+ ss << "Subexpressions must have a common base type:" << std::endl;
ss << "Equation: " << n << std::endl;
ss << "Type 1: " << lhsType << std::endl;
ss << "Type 2: " << rhsType << std::endl;
#include "theory/datatypes/theory_datatypes_type_rules.h"
#include "theory/model.h"
#include "smt/options.h"
+#include "smt/boolean_terms.h"
#include "theory/quantifiers/options.h"
#include <map>
return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
}
+ TypeNode t = in.getType();
+
// we only care about tuples and records here
if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE &&
in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) {
+ if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
+ Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
+ Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl;
+ if(t.isTuple()) {
+ Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl;
+ Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl;
+ NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
+ } else {
+ Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl;
+ Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl;
+ NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
+ }
+ }
// nothing to do
return in;
}
- TypeNode t = in.getType();
-
if(t.hasAttribute(expr::DatatypeTupleAttr())) {
t = t.getAttribute(expr::DatatypeTupleAttr());
} else if(t.hasAttribute(expr::DatatypeRecordAttr())) {
void newEnumerators() {
d_enumerators = new TypeEnumerator*[getType().getNumChildren()];
for(size_t i = 0; i < getType().getNumChildren(); ++i) {
- d_enumerators[i] = NULL;
+ d_enumerators[i] = new TypeEnumerator(getType()[i]);
}
}
if(te.d_enumerators != NULL) {
newEnumerators();
for(size_t i = 0; i < getType().getNumChildren(); ++i) {
- if(te.d_enumerators[i] != NULL) {
- d_enumerators[i] = new TypeEnumerator(*te.d_enumerators[i]);
- }
+ *d_enumerators[i] = TypeEnumerator(*te.d_enumerators[i]);
}
}
}
if(re.d_enumerators != NULL) {
newEnumerators();
for(size_t i = 0; i < getType().getNumChildren(); ++i) {
- if(re.d_enumerators[i] != NULL) {
- d_enumerators[i] = new TypeEnumerator(*re.d_enumerators[i]);
- }
+ *d_enumerators[i] = TypeEnumerator(*re.d_enumerators[i]);
}
}
}
Expr TheoryModel::getValue( Expr expr ) const{
Node n = Node::fromExpr( expr );
Node ret = getValue( n );
- return d_smt.postprocess(ret).toExpr();
+ return d_smt.postprocess(ret, TypeNode::fromType(expr.getType())).toExpr();
}
/** get cardinality for sort */
// can only output datatypes in the CVC4 native language
Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
- os << "DATATYPE " << dt.getName() << " =" << endl;
+ os << "DATATYPE " << dt.getName();
+ if(dt.isParametric()) {
+ os << '[';
+ for(size_t i = 0; i < dt.getNumParameters(); ++i) {
+ if(i > 0) {
+ os << ',';
+ }
+ os << dt.getParameter(i);
+ }
+ os << ']';
+ }
+ os << " =" << endl;
Datatype::const_iterator i = dt.begin(), i_end = dt.end();
if(i != i_end) {
os << " ";
* Create a new Datatype of the given name, with the given
* parameterization.
*/
- inline Datatype(std::string name, std::vector<Type>& params);
+ inline Datatype(std::string name, const std::vector<Type>& params);
/**
* Add a constructor to this Datatype. Constructor names need not
d_self() {
}
-inline Datatype::Datatype(std::string name, std::vector<Type>& params) :
+inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
d_name(name),
d_params(params),
d_constructors(),
typed_v2l30079.cvc \
typed_v3l20092.cvc \
typed_v5l30069.cvc \
+ boolean-terms-datatype.cvc \
+ boolean-terms-parametric-datatype-1.cvc \
+ boolean-terms-parametric-datatype-2.cvc \
+ boolean-terms-tuple.cvc \
+ boolean-terms-record.cvc \
+ some-boolean-tests.cvc \
v10l40099.cvc \
v2l40025.cvc \
v3l60006.cvc \
wrong-sel-simp.cvc
FAILING_TESTS = \
+ pair-real-bool.smt2 \
datatype-dump.cvc
EXTRA_DIST = $(TESTS)
--- /dev/null
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE List =
+ cons(car:BOOLEAN, cdr:List) | nil
+END;
+
+x : List;
+
+ASSERT x /= nil;
+
+CHECKSAT;
--- /dev/null
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE RightistTree[T] =
+ node(left:BOOLEAN, right:RightistTree[T]) |
+ leaf(data:T)
+END;
+
+x : RightistTree[INT];
+
+ASSERT x /= leaf(0);
+
+CHECKSAT;
--- /dev/null
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE RightistTree[T] =
+ node(left:BOOLEAN, right:RightistTree[T]) |
+ leaf(data:T)
+END;
+
+x : RightistTree[INT];
+
+ASSERT x /= leaf(0);
+
+CHECKSAT;
--- /dev/null
+% EXPECT: sat
+% EXIT: 10
+
+x : [# i:INT, b:BOOLEAN #];
+
+ASSERT x /= (# i := 0, b := FALSE #);
+
+CHECKSAT;
--- /dev/null
+% EXPECT: sat
+% EXIT: 10
+
+x : [ INT, BOOLEAN ];
+
+ASSERT x /= ( 0, FALSE );
+
+CHECKSAT;
--- /dev/null
+;(set-option :produce-models true)
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () (
+ ( RealTree
+ ( Node
+ (left RealTree)
+ (elem Real)
+ (right RealTree))
+ (Leaf)
+ )
+))
+
+(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
+
+( declare-fun SumeAndPositiveTree ( RealTree ) (Pair Real Bool) )
+
+(declare-fun l1 () RealTree)
+(declare-fun l2 () RealTree)
+(declare-const result (Pair Real Bool))
+(assert (= l1 (Node l2 5.0 l2)))
+(assert (= result (SumeAndPositiveTree l1)))
+(assert (= (first result) 5))
+(assert (= (second result) true))
+(check-sat)
--- /dev/null
+% EXPECT: sat
+% EXIT: 10
+DATATYPE list[T] = cons(car:T, care:BOOLEAN, cdr:list[T]) | nil END;
+x : list[REAL];
+
+y : [INT,BOOLEAN,INT];
+ASSERT y = (5,TRUE,4);
+
+ASSERT y.1;
+
+ASSERT x = cons(1.1,TRUE,nil::list[REAL])::list[REAL];
+CHECKSAT;
projects / cvc5.git / commitdiff