diff options
30 files changed, 896 insertions, 169 deletions
@@ -15,5 +15,6 @@ Changes since 1.0 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 diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 5159f6b5a..eab41ee38 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -936,7 +936,7 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr ("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"); } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 5f813dbe8..bd3827f47 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -713,6 +713,10 @@ public: 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); @@ -902,6 +906,16 @@ NodeBuilder<nchild_thresh>::operator Node() const { } 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; " "attempt to access it after conversion"); diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 236f48017..7522b8110 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -94,15 +94,32 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { 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; } @@ -125,15 +142,32 @@ bool TypeNode::isComparableTo(TypeNode t) const { 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 { diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 2cfeaafc1..524344612 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -817,7 +817,7 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t 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) { @@ -1068,7 +1068,18 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr 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) { diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 35184e42e..09d8fcbd4 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -21,6 +21,8 @@ #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" @@ -31,10 +33,56 @@ 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: @@ -63,27 +111,51 @@ static inline bool isBoolean(TNode top, unsigned i) { } } -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); } @@ -91,22 +163,107 @@ const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype } 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) { @@ -134,11 +291,21 @@ static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TN } } -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; } @@ -147,22 +314,24 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st 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; } @@ -176,19 +345,19 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st 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; @@ -200,9 +369,10 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st 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", @@ -216,7 +386,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st 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; } @@ -226,105 +396,112 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st 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; } } @@ -385,11 +562,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st } } 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; } } @@ -400,15 +578,20 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st 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(); @@ -416,17 +599,21 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st } 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() */ diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index c53eadfa0..06f25f9ef 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -38,35 +38,64 @@ typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr; 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 */ diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index 26f5c9c60..fb80b27f7 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -17,37 +17,170 @@ #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() */ - diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h index 08e6168d9..f727a3483 100644 --- a/src/smt/model_postprocessor.h +++ b/src/smt/model_postprocessor.h @@ -25,9 +25,12 @@ namespace CVC4 { 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(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e98bffc1e..147cea85b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -63,6 +63,8 @@ #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" @@ -586,11 +588,13 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : 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 @@ -2636,10 +2640,26 @@ void SmtEnginePrivate::processAssertions() { 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; } @@ -3046,10 +3066,14 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log 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) { @@ -3071,7 +3095,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep // 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(); } @@ -3093,7 +3117,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L } 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(); } @@ -3140,8 +3164,10 @@ Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, TypeCheckingExcep 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())); @@ -3356,7 +3382,9 @@ void SmtEngine::checkModel(bool hardFailure) { // 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.) @@ -3391,6 +3419,7 @@ void SmtEngine::checkModel(bool hardFailure) { } // (3) checks complete, add the substitution + Debug("boolean-terms") << "cm: adding subs " << func << " :=> " << val << endl; substitutions.addSubstitution(func, val); } } @@ -3408,7 +3437,9 @@ void SmtEngine::checkModel(bool hardFailure) { 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. diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index fecfba14a..525f90ffe 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -249,7 +249,7 @@ class CVC4_PUBLIC SmtEngine { * 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 diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index 8cb32de18..9d58ffa75 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -13,7 +13,10 @@ libbooleans_la_SOURCES = \ 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 diff --git a/src/theory/booleans/boolean_term_conversion_mode.cpp b/src/theory/booleans/boolean_term_conversion_mode.cpp new file mode 100644 index 000000000..f9d80835c --- /dev/null +++ b/src/theory/booleans/boolean_term_conversion_mode.cpp @@ -0,0 +1,41 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/booleans/boolean_term_conversion_mode.h b/src/theory/booleans/boolean_term_conversion_mode.h new file mode 100644 index 000000000..6ca908df4 --- /dev/null +++ b/src/theory/booleans/boolean_term_conversion_mode.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/booleans/options b/src/theory/booleans/options index ae14de58b..6c571f30e 100644 --- a/src/theory/booleans/options +++ b/src/theory/booleans/options @@ -5,4 +5,7 @@ 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 diff --git a/src/theory/booleans/options_handlers.h b/src/theory/booleans/options_handlers.h new file mode 100644 index 000000000..2bf53b3d2 --- /dev/null +++ b/src/theory/booleans/options_handlers.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 352868f7b..a369fb572 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -79,7 +79,7 @@ class EqualityTypeRule { 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; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9e4f0de75..a3bec7af0 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -24,6 +24,7 @@ #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> @@ -311,15 +312,28 @@ Node TheoryDatatypes::ppRewrite(TNode in) { 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())) { diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 2a74f6d15..a4facdefe 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -176,7 +176,7 @@ class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> { 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]); } } @@ -205,9 +205,7 @@ public: 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]); } } } @@ -292,9 +290,7 @@ public: 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]); } } } diff --git a/src/theory/model.cpp b/src/theory/model.cpp index bbc51c9e0..42a5380e4 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -57,7 +57,7 @@ Node TheoryModel::getValue( TNode n ) const{ 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 */ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 18ecbc316..574a57f19 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -820,7 +820,18 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { // 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 << " "; diff --git a/src/util/datatype.h b/src/util/datatype.h index de38d8835..4b6894ef8 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -450,7 +450,7 @@ public: * 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 @@ -620,7 +620,7 @@ inline Datatype::Datatype(std::string name) : 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(), diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 08462d51b..8e992c03e 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -38,6 +38,12 @@ TESTS = \ 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 \ @@ -48,6 +54,7 @@ TESTS = \ wrong-sel-simp.cvc FAILING_TESTS = \ + pair-real-bool.smt2 \ datatype-dump.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/datatypes/boolean-terms-datatype.cvc b/test/regress/regress0/datatypes/boolean-terms-datatype.cvc new file mode 100644 index 000000000..490574b35 --- /dev/null +++ b/test/regress/regress0/datatypes/boolean-terms-datatype.cvc @@ -0,0 +1,12 @@ +% EXPECT: sat +% EXIT: 10 + +DATATYPE List = + cons(car:BOOLEAN, cdr:List) | nil +END; + +x : List; + +ASSERT x /= nil; + +CHECKSAT; diff --git a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc new file mode 100644 index 000000000..b667d0bbc --- /dev/null +++ b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc @@ -0,0 +1,13 @@ +% 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; diff --git a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc new file mode 100644 index 000000000..b667d0bbc --- /dev/null +++ b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc @@ -0,0 +1,13 @@ +% 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; diff --git a/test/regress/regress0/datatypes/boolean-terms-record.cvc b/test/regress/regress0/datatypes/boolean-terms-record.cvc new file mode 100644 index 000000000..ec757d042 --- /dev/null +++ b/test/regress/regress0/datatypes/boolean-terms-record.cvc @@ -0,0 +1,8 @@ +% EXPECT: sat +% EXIT: 10 + +x : [# i:INT, b:BOOLEAN #]; + +ASSERT x /= (# i := 0, b := FALSE #); + +CHECKSAT; diff --git a/test/regress/regress0/datatypes/boolean-terms-tuple.cvc b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc new file mode 100644 index 000000000..c2d95ce8f --- /dev/null +++ b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc @@ -0,0 +1,8 @@ +% EXPECT: sat +% EXIT: 10 + +x : [ INT, BOOLEAN ]; + +ASSERT x /= ( 0, FALSE ); + +CHECKSAT; diff --git a/test/regress/regress0/datatypes/pair-real-bool.smt2 b/test/regress/regress0/datatypes/pair-real-bool.smt2 new file mode 100644 index 000000000..5d028d723 --- /dev/null +++ b/test/regress/regress0/datatypes/pair-real-bool.smt2 @@ -0,0 +1,25 @@ +;(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) diff --git a/test/regress/regress0/datatypes/some-boolean-tests.cvc b/test/regress/regress0/datatypes/some-boolean-tests.cvc new file mode 100644 index 000000000..ac6ef1137 --- /dev/null +++ b/test/regress/regress0/datatypes/some-boolean-tests.cvc @@ -0,0 +1,12 @@ +% 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; |