diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/builtin/kinds | 10 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 65 | ||||
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 83 | ||||
-rw-r--r-- | src/theory/datatypes/kinds | 68 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 100 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 236 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.h | 140 | ||||
-rw-r--r-- | src/theory/model.cpp | 3 | ||||
-rw-r--r-- | src/theory/type_enumerator.h | 36 |
10 files changed, 657 insertions, 86 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index bcf787f6b..e3bc506e2 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -296,7 +296,6 @@ operator DISTINCT 2: "disequality" variable VARIABLE "variable" variable BOUND_VARIABLE "bound variable" variable SKOLEM "skolem var" -operator TUPLE 1: "a tuple" operator SEXPR 0: "a symbolic expression" operator LAMBDA 2 "lambda" @@ -313,14 +312,6 @@ cardinality FUNCTION_TYPE \ "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" well-founded FUNCTION_TYPE false -operator TUPLE_TYPE 1: "tuple type" -cardinality TUPLE_TYPE \ - "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \ - "theory/builtin/theory_builtin_type_rules.h" -well-founded TUPLE_TYPE \ - "::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \ - "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \ - "theory/builtin/theory_builtin_type_rules.h" operator SEXPR_TYPE 0: "symbolic expression type" cardinality SEXPR_TYPE \ "::CVC4::theory::builtin::SExprProperties::computeCardinality(%TYPE%)" \ @@ -350,7 +341,6 @@ typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule -typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 720e55be3..4aa7c0982 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -115,19 +115,6 @@ public: } };/* class DistinctTypeRule */ -class TupleTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - std::vector<TypeNode> types; - for(TNode::iterator child_it = n.begin(), child_it_end = n.end(); - child_it != child_it_end; - ++child_it) { - types.push_back((*child_it).getType(check)); - } - return nodeManager->mkTupleType(types); - } -};/* class TupleTypeRule */ - class SExprTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { @@ -269,58 +256,6 @@ public: } };/* class FuctionProperties */ -class TupleProperties { -public: - inline static Cardinality computeCardinality(TypeNode type) { - // Don't assert this; allow other theories to use this cardinality - // computation. - // - // Assert(type.getKind() == kind::TUPLE_TYPE); - - Cardinality card(1); - for(TypeNode::iterator i = type.begin(), - i_end = type.end(); - i != i_end; - ++i) { - card *= (*i).getCardinality(); - } - - return card; - } - - inline static bool isWellFounded(TypeNode type) { - // Don't assert this; allow other theories to use this - // wellfoundedness computation. - // - // Assert(type.getKind() == kind::TUPLE_TYPE); - - for(TypeNode::iterator i = type.begin(), - i_end = type.end(); - i != i_end; - ++i) { - if(! (*i).isWellFounded()) { - return false; - } - } - - return true; - } - - inline static Node mkGroundTerm(TypeNode type) { - Assert(type.getKind() == kind::TUPLE_TYPE); - - std::vector<Node> children; - for(TypeNode::iterator i = type.begin(), - i_end = type.end(); - i != i_end; - ++i) { - children.push_back((*i).mkGroundTerm()); - } - - return NodeManager::currentNM()->mkNode(kind::TUPLE, children); - } -};/* class TupleProperties */ - class SExprProperties { public: inline static Cardinality computeCardinality(TypeNode type) { diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 42b999561..f9fb00a75 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -54,6 +54,43 @@ public: } } } + if(in.getKind() == kind::TUPLE_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { + return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]); + } + if(in.getKind() == kind::RECORD_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { + const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst<Record>(); + return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst<RecordSelect>().getField())]); + } + if(in.getKind() == kind::APPLY_SELECTOR && + (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) { + // These strange (half-tuple-converted) terms can be created by + // the system if you have something like "foo.1" for a tuple + // term foo. The select is rewritten to "select_1(foo)". If + // foo gets a value in the model from the TypeEnumerator, you + // then have a select of a tuple, and we should flatten that + // here. Ditto for records, below. + Expr selectorExpr = in.getOperator().toExpr(); + const Datatype& dt CVC4_UNUSED = Datatype::datatypeOf(selectorExpr); + TypeNode dtt CVC4_UNUSED = TypeNode::fromType(dt.getDatatypeType()); + size_t selectorIndex = Datatype::indexOf(selectorExpr); + Debug("tuprec") << "looking at " << in << ", got selector index " << selectorIndex << std::endl; +#ifdef CVC4_ASSERTIONS + // sanity checks: tuple- and record-converted datatypes should have one constructor + Assert(NodeManager::currentNM()->getDatatypeForTupleRecord(in[0].getType()) == dtt); + if(in[0].getKind() == kind::TUPLE) { + Assert(dtt.hasAttribute(expr::DatatypeTupleAttr())); + Assert(dtt.getAttribute(expr::DatatypeTupleAttr()) == in[0].getType()); + } else { + Assert(dtt.hasAttribute(expr::DatatypeRecordAttr())); + Assert(dtt.getAttribute(expr::DatatypeRecordAttr()) == in[0].getType()); + } + Assert(dt.getNumConstructors() == 1); + Assert(dt[0].getNumArgs() > selectorIndex); + Assert(dt[0][selectorIndex].getSelector() == selectorExpr); +#endif /* CVC4_ASSERTIONS */ + Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl; + return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); + } if(in.getKind() == kind::APPLY_SELECTOR && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { // Have to be careful not to rewrite well-typed expressions @@ -90,6 +127,45 @@ public: } } } + if(in.getKind() == kind::TUPLE_SELECT && + in[0].getKind() == kind::TUPLE) { + return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]); + } + if(in.getKind() == kind::TUPLE_UPDATE && + in[0].getKind() == kind::TUPLE) { + size_t ix = in.getOperator().getConst<TupleUpdate>().getIndex(); + NodeBuilder<> b(kind::TUPLE); + for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) { + if(ix == 0) { + b << in[1]; + } else { + b << *i; + } + } + Node n = b; + Assert(n.getType().isSubtypeOf(in.getType())); + return RewriteResponse(REWRITE_DONE, n); + } + if(in.getKind() == kind::RECORD_SELECT && + in[0].getKind() == kind::RECORD) { + return RewriteResponse(REWRITE_DONE, in[0][in[0].getOperator().getConst<Record>().getIndex(in.getOperator().getConst<RecordSelect>().getField())]); + } + if(in.getKind() == kind::RECORD_UPDATE && + in[0].getKind() == kind::RECORD) { + size_t ix = in[0].getOperator().getConst<Record>().getIndex(in.getConst<RecordUpdate>().getField()); + NodeBuilder<> b(kind::RECORD); + b << in[0].getOperator(); + for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) { + if(ix == 0) { + b << in[1]; + } else { + b << *i; + } + } + Node n = b; + Assert(n.getType().isSubtypeOf(in.getType())); + return RewriteResponse(REWRITE_DONE, n); + } if(in.getKind() == kind::EQUAL && in[0] == in[1]) { return RewriteResponse(REWRITE_DONE, @@ -113,7 +189,9 @@ public: static inline void shutdown() {} static bool checkClash( Node n1, Node n2 ) { - if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) { + if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) || + (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) || + (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) { if( n1.getOperator() != n2.getOperator() ) { return true; } else { @@ -137,7 +215,8 @@ public: /** is this term a datatype */ static bool isTermDatatype( Node n ){ TypeNode tn = n.getType(); - return tn.isDatatype() || tn.isParametricDatatype(); + return tn.isDatatype() || tn.isParametricDatatype() || + tn.isTuple() || tn.isRecord(); } };/* class DatatypesRewriter */ diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index eac3d6eac..d1fbf82bc 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -84,4 +84,72 @@ typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionType # constructor applications are constant if they are applied only to constants construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule +operator TUPLE_TYPE 1: "tuple type" +cardinality TUPLE_TYPE \ + "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \ + "theory/datatypes/theory_datatypes_type_rules.h" +well-founded TUPLE_TYPE \ + "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::datatypes::TupleProperties::mkGroundTerm(%TYPE%)" \ + "theory/datatypes/theory_datatypes_type_rules.h" +enumerator TUPLE_TYPE \ + "::CVC4::theory::datatypes::TupleEnumerator" \ + "theory/datatypes/type_enumerator.h" + +operator TUPLE 1: "a tuple" +typerule TUPLE ::CVC4::theory::datatypes::TupleTypeRule +construle TUPLE ::CVC4::theory::datatypes::TupleProperties + +constant TUPLE_SELECT_OP \ + ::CVC4::TupleSelect \ + ::CVC4::TupleSelectHashFunction \ + "util/tuple.h" \ + "operator for a tuple select" +parameterized TUPLE_SELECT TUPLE_SELECT_OP 1 "tuple select" +typerule TUPLE_SELECT ::CVC4::theory::datatypes::TupleSelectTypeRule + +constant TUPLE_UPDATE_OP \ + ::CVC4::TupleUpdate \ + ::CVC4::TupleUpdateHashFunction \ + "util/tuple.h" \ + "operator for a tuple update" +parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update" +typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule + +constant RECORD_TYPE \ + ::CVC4::Record \ + "::CVC4::RecordHashFunction" \ + "util/record.h" \ + "record type" +cardinality RECORD_TYPE \ + "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \ + "theory/datatypes/theory_datatypes_type_rules.h" +well-founded RECORD_TYPE \ + "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::datatypes::RecordProperties::mkGroundTerm(%TYPE%)" \ + "theory/datatypes/theory_datatypes_type_rules.h" +enumerator RECORD_TYPE \ + "::CVC4::theory::datatypes::RecordEnumerator" \ + "theory/datatypes/type_enumerator.h" + +parameterized RECORD RECORD_TYPE 1: "a record" +typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule +construle RECORD ::CVC4::theory::datatypes::RecordProperties + +constant RECORD_SELECT_OP \ + ::CVC4::RecordSelect \ + ::CVC4::RecordSelectHashFunction \ + "util/record.h" \ + "operator for a record select" +parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select" +typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule + +constant RECORD_UPDATE_OP \ + ::CVC4::RecordUpdate \ + ::CVC4::RecordUpdateHashFunction \ + "util/record.h" \ + "operator for a record update" +parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update" +typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule + endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 8ec45efb9..6273eb2c2 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -22,6 +22,7 @@ #include "util/cvc4_assert.h" #include "theory/datatypes/theory_datatypes_instantiator.h" #include "theory/datatypes/datatypes_rewriter.h" +#include "theory/datatypes/theory_datatypes_type_rules.h" #include "theory/model.h" #include "smt/options.h" @@ -94,6 +95,19 @@ void TheoryDatatypes::check(Effort e) { Assertion assertion = get(); TNode fact = assertion.assertion; Trace("datatypes-assert") << "Assert " << fact << std::endl; + + TNode atom CVC4_UNUSED = fact.getKind() == kind::NOT ? fact[0] : fact; + + // extra debug check to make sure that the rewriter did its job correctly + Assert( atom.getKind() != kind::EQUAL || + ( atom[0].getKind() != kind::TUPLE && atom[1].getKind() != kind::TUPLE && + atom[0].getKind() != kind::RECORD && atom[1].getKind() != kind::RECORD && + atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE && + atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE && + atom[0].getKind() != kind::TUPLE_SELECT && atom[1].getKind() != kind::TUPLE_SELECT && + atom[0].getKind() != kind::RECORD_SELECT && atom[1].getKind() != kind::RECORD_SELECT ), + "tuple/record escaped into datatypes decision procedure; should have been rewritten away" ); + //assert the fact assertFact( fact, fact ); flushPendingFacts(); @@ -275,6 +289,90 @@ void TheoryDatatypes::presolve() { Debug("datatypes") << "TheoryDatatypes::presolve()" << endl; } +Node TheoryDatatypes::ppRewrite(TNode in) { + Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl; + + if(in.getKind() == kind::TUPLE_SELECT) { + TypeNode t = in[0].getType(); + if(t.hasAttribute(expr::DatatypeTupleAttr())) { + t = t.getAttribute(expr::DatatypeTupleAttr()); + } + TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); + const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]); + } else if(in.getKind() == kind::RECORD_SELECT) { + TypeNode t = in[0].getType(); + if(t.hasAttribute(expr::DatatypeRecordAttr())) { + t = t.getAttribute(expr::DatatypeRecordAttr()); + } + TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); + const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]); + } + + // 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) { + // 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())) { + t = t.getAttribute(expr::DatatypeRecordAttr()); + } + + // if the type doesn't have an associated datatype, then make one for it + TypeNode dtt = (t.isTuple() || t.isRecord()) ? NodeManager::currentNM()->getDatatypeForTupleRecord(t) : t; + + const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); + + // now rewrite the expression + Node n; + if(in.getKind() == kind::TUPLE || in.getKind() == kind::RECORD) { + NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); + b << Node::fromExpr(dt[0].getConstructor()); + b.append(in.begin(), in.end()); + n = b; + } else if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) { + NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); + b << Node::fromExpr(dt[0].getConstructor()); + size_t size, updateIndex; + if(in.getKind() == kind::TUPLE_UPDATE) { + size = t.getNumChildren(); + updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex(); + } else { // kind::RECORD_UPDATE + const Record& record = t.getConst<Record>(); + size = record.getNumFields(); + updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField()); + } + Debug("tuprec") << "expr is " << in << std::endl; + Debug("tuprec") << "updateIndex is " << updateIndex << std::endl; + Debug("tuprec") << "t is " << t << std::endl; + Debug("tuprec") << "t has arity " << size << std::endl; + for(size_t i = 0; i < size; ++i) { + if(i == updateIndex) { + b << in[1]; + Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl; + } else { + b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]); + Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl; + } + } + Debug("tuprec") << "builder says " << b << std::endl; + n = b; + } + + Assert(!n.isNull()); + + Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl; + + return n; +} + void TheoryDatatypes::addSharedTerm(TNode t) { Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): " << t << endl; @@ -719,7 +817,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); collectTerms( n_ic ); //add type ascription for ambiguous constructor types - if( n_ic.getType()!=n.getType() ){ + if(!n_ic.getType().isComparableTo(n.getType())) { Assert( dt.isParametric() ); Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl; Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 5cda9eeae..4380eca58 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -52,6 +52,7 @@ private: /** inferences */ NodeList d_infer; NodeList d_infer_exp; + private: //notification class for equality engine class NotifyClass : public eq::EqualityEngineNotify { @@ -202,6 +203,7 @@ public: void check(Effort e); void preRegisterTerm(TNode n); + Node ppRewrite(TNode n); void presolve(); void addSharedTerm(TNode t); EqualityStatus getEqualityStatus(TNode a, TNode b); diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index eb50def01..ade9ffc26 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -20,6 +20,7 @@ #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H #include "util/matcher.h" +#include "expr/attribute.h" namespace CVC4 { @@ -70,7 +71,7 @@ struct DatatypeConstructorTypeRule { TypeNode childType = (*child_it).getType(check); Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl; TypeNode argumentType = *tchild_it; - if(!childType.isSubtypeOf(argumentType)) { + if(!childType.isComparableTo(argumentType)) { std::stringstream ss; ss << "bad type for constructor argument:\nexpected: " << argumentType << "\ngot : " << childType; throw TypeCheckingExceptionPrivate(n, ss.str()); @@ -127,7 +128,7 @@ struct DatatypeSelectorTypeRule { Debug("typecheck-idt") << "typecheck sel: " << n << std::endl; Debug("typecheck-idt") << "sel type: " << selType << std::endl; TypeNode childType = n[0].getType(check); - if(selType[0] != childType) { + if(!selType[0].isComparableTo(childType)) { Debug("typecheck-idt") << "ERROR: " << selType[0].getKind() << " " << childType.getKind() << std::endl; throw TypeCheckingExceptionPrivate(n, "bad type for selector argument"); } @@ -150,16 +151,16 @@ struct DatatypeTesterTypeRule { Type t = testType[0].toType(); Assert( t.isDatatype() ); DatatypeType dt = DatatypeType(t); - if( dt.isParametric() ){ + if(dt.isParametric()) { Debug("typecheck-idt") << "typecheck parameterized tester: " << n << std::endl; Matcher m( dt ); if( !m.doMatching( testType[0], childType ) ){ throw TypeCheckingExceptionPrivate(n, "matching failed for tester argument of parameterized datatype"); } - }else{ + } else { Debug("typecheck-idt") << "typecheck test: " << n << std::endl; Debug("typecheck-idt") << "test type: " << testType << std::endl; - if(testType[0] != childType) { + if(!testType[0].isComparableTo(childType)) { throw TypeCheckingExceptionPrivate(n, "bad type for tester argument"); } } @@ -265,6 +266,231 @@ struct ConstructorProperties { } };/* struct ConstructorProperties */ +struct TupleTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::TUPLE); + std::vector<TypeNode> types; + for(TNode::iterator child_it = n.begin(), child_it_end = n.end(); + child_it != child_it_end; + ++child_it) { + types.push_back((*child_it).getType(check)); + } + return nodeManager->mkTupleType(types); + } +};/* struct TupleTypeRule */ + +struct TupleSelectTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::TUPLE_SELECT); + const TupleSelect& ts = n.getOperator().getConst<TupleSelect>(); + TypeNode tupleType = n[0].getType(check); + if(!tupleType.isTuple()) { + if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) { + throw TypeCheckingExceptionPrivate(n, "Tuple-select expression formed over non-tuple"); + } + tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr()); + } + if(ts.getIndex() >= tupleType.getNumChildren()) { + std::stringstream ss; + ss << "Tuple-select expression index `" << ts.getIndex() + << "' is not a valid index; tuple type only has " + << tupleType.getNumChildren() << " fields"; + throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); + } + return tupleType[ts.getIndex()]; + } +};/* struct TupleSelectTypeRule */ + +struct TupleUpdateTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::TUPLE_UPDATE); + const TupleUpdate& tu = n.getOperator().getConst<TupleUpdate>(); + TypeNode tupleType = n[0].getType(check); + TypeNode newValue = n[1].getType(check); + if(check) { + if(!tupleType.isTuple()) { + if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) { + throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple"); + } + tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr()); + } + if(tu.getIndex() >= tupleType.getNumChildren()) { + std::stringstream ss; + ss << "Tuple-update expression index `" << tu.getIndex() + << "' is not a valid index; tuple type only has " + << tupleType.getNumChildren() << " fields"; + throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); + } + } + return tupleType; + } +};/* struct TupleUpdateTypeRule */ + +struct TupleProperties { + inline static Cardinality computeCardinality(TypeNode type) { + // Don't assert this; allow other theories to use this cardinality + // computation. + // + // Assert(type.getKind() == kind::TUPLE_TYPE); + + Cardinality card(1); + for(TypeNode::iterator i = type.begin(), + i_end = type.end(); + i != i_end; + ++i) { + card *= (*i).getCardinality(); + } + + return card; + } + + inline static bool isWellFounded(TypeNode type) { + // Don't assert this; allow other theories to use this + // wellfoundedness computation. + // + // Assert(type.getKind() == kind::TUPLE_TYPE); + + for(TypeNode::iterator i = type.begin(), + i_end = type.end(); + i != i_end; + ++i) { + if(! (*i).isWellFounded()) { + return false; + } + } + + return true; + } + + inline static Node mkGroundTerm(TypeNode type) { + Assert(type.getKind() == kind::TUPLE_TYPE); + + std::vector<Node> children; + for(TypeNode::iterator i = type.begin(), + i_end = type.end(); + i != i_end; + ++i) { + children.push_back((*i).mkGroundTerm()); + } + + return NodeManager::currentNM()->mkNode(kind::TUPLE, children); + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::TUPLE); + NodeManagerScope nms(nodeManager); + + for(TNode::iterator i = n.begin(), + i_end = n.end(); + i != i_end; + ++i) { + if(! (*i).isConst()) { + return false; + } + } + + return true; + } +};/* struct TupleProperties */ + +struct RecordTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::RECORD); + NodeManagerScope nms(nodeManager); + const Record& rec = n.getOperator().getConst<Record>(); + if(check) { + Record::iterator i = rec.begin(); + for(TNode::iterator child_it = n.begin(), child_it_end = n.end(); + child_it != child_it_end; + ++child_it, ++i) { + if(i == rec.end()) { + throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal"); + } + if(!(*child_it).getType(check).isComparableTo(TypeNode::fromType((*i).second))) { + throw TypeCheckingExceptionPrivate(n, "record description types differ from record literal types"); + } + } + if(i != rec.end()) { + throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal"); + } + } + return nodeManager->mkRecordType(rec); + } +};/* struct RecordTypeRule */ + +struct RecordSelectTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::RECORD_SELECT); + NodeManagerScope nms(nodeManager); + const RecordSelect& rs = n.getOperator().getConst<RecordSelect>(); + TypeNode recordType = n[0].getType(check); + if(!recordType.isRecord()) { + if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) { + throw TypeCheckingExceptionPrivate(n, "Record-select expression formed over non-record"); + } + recordType = recordType.getAttribute(expr::DatatypeRecordAttr()); + } + const Record& rec = recordType.getRecord(); + Record::const_iterator field = rec.find(rs.getField()); + if(field == rec.end()) { + std::stringstream ss; + ss << "Record-select field `" << rs.getField() + << "' is not a valid field name for the record type"; + throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); + } + return TypeNode::fromType((*field).second); + } +};/* struct RecordSelectTypeRule */ + +struct RecordUpdateTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + Assert(n.getKind() == kind::RECORD_UPDATE); + NodeManagerScope nms(nodeManager); + const RecordUpdate& ru = n.getOperator().getConst<RecordUpdate>(); + TypeNode recordType = n[0].getType(check); + TypeNode newValue = n[1].getType(check); + if(check) { + if(!recordType.isRecord()) { + if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) { + throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record"); + } + recordType = recordType.getAttribute(expr::DatatypeRecordAttr()); + } + const Record& rec = recordType.getRecord(); + Record::const_iterator field = rec.find(ru.getField()); + if(field == rec.end()) { + std::stringstream ss; + ss << "Record-update field `" << ru.getField() + << "' is not a valid field name for the record type"; + throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); + } + } + return recordType; + } +};/* struct RecordUpdateTypeRule */ + +struct RecordProperties { + inline static Node mkGroundTerm(TypeNode type) { + Unimplemented(); + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::RECORD); + NodeManagerScope nms(nodeManager); + + for(TNode::iterator i = n.begin(), + i_end = n.end(); + i != i_end; + ++i) { + if(! (*i).isConst()) { + return false; + } + } + + return true; + } +};/* struct RecordProperties */ + }/* CVC4::theory::datatypes namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 0f365bd71..ea68e8957 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -147,6 +147,146 @@ public: };/* DatatypesEnumerator */ +class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> { + TypeEnumerator** d_enumerators; + + void deleteEnumerators() throw() { + if(d_enumerators != NULL) { + for(size_t i = 0; i < getType().getNumChildren(); ++i) { + delete d_enumerators[i]; + } + delete [] d_enumerators; + d_enumerators = NULL; + } + } + +public: + + TupleEnumerator(TypeNode type) throw() : + TypeEnumeratorBase<TupleEnumerator>(type) { + Assert(type.isTuple()); + d_enumerators = new TypeEnumerator*[type.getNumChildren()]; + for(size_t i = 0; i < type.getNumChildren(); ++i) { + d_enumerators[i] = new TypeEnumerator(type[i]); + } + } + + ~TupleEnumerator() throw() { + deleteEnumerators(); + } + + Node operator*() throw(NoMoreValuesException) { + if(isFinished()) { + throw NoMoreValuesException(getType()); + } + + NodeBuilder<> nb(kind::TUPLE); + for(size_t i = 0; i < getType().getNumChildren(); ++i) { + nb << **d_enumerators[i]; + } + return Node(nb); + } + + TupleEnumerator& operator++() throw() { + if(isFinished()) { + return *this; + } + + size_t i; + for(i = 0; i < getType().getNumChildren(); ++i) { + if(d_enumerators[i]->isFinished()) { + *d_enumerators[i] = TypeEnumerator(getType()[i]); + } else { + ++*d_enumerators[i]; + return *this; + } + } + + deleteEnumerators(); + + return *this; + } + + bool isFinished() throw() { + return d_enumerators == NULL; + } + +};/* TupleEnumerator */ + +class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> { + TypeEnumerator** d_enumerators; + + void deleteEnumerators() throw() { + if(d_enumerators != NULL) { + for(size_t i = 0; i < getType().getNumChildren(); ++i) { + delete d_enumerators[i]; + } + delete [] d_enumerators; + d_enumerators = NULL; + } + } + +public: + + RecordEnumerator(TypeNode type) throw() : + TypeEnumeratorBase<RecordEnumerator>(type) { + Assert(type.isRecord()); + const Record& rec = getType().getConst<Record>(); + Debug("te") << "creating record enumerator for " << type << std::endl; + d_enumerators = new TypeEnumerator*[rec.getNumFields()]; + for(size_t i = 0; i < rec.getNumFields(); ++i) { + Debug("te") << " - sub-enumerator for " << rec[i].second << std::endl; + d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second)); + } + } + + ~RecordEnumerator() throw() { + deleteEnumerators(); + } + + Node operator*() throw(NoMoreValuesException) { + if(isFinished()) { + throw NoMoreValuesException(getType()); + } + + NodeBuilder<> nb(kind::RECORD); + Debug("te") << "record enumerator: creating record of type " << getType() << std::endl; + nb << getType(); + const Record& rec = getType().getConst<Record>(); + for(size_t i = 0; i < rec.getNumFields(); ++i) { + Debug("te") << " - " << i << " " << std::flush << "=> " << **d_enumerators[i] << std::endl; + nb << **d_enumerators[i]; + } + return Node(nb); + } + + RecordEnumerator& operator++() throw() { + if(isFinished()) { + return *this; + } + + size_t i; + const Record& rec = getType().getConst<Record>(); + for(i = 0; i < rec.getNumFields(); ++i) { + if(d_enumerators[i]->isFinished()) { + *d_enumerators[i] = TypeEnumerator(TypeNode::fromType(rec[i].second)); + } else { + ++*d_enumerators[i]; + return *this; + } + } + + deleteEnumerators(); + + return *this; + } + + bool isFinished() throw() { + return d_enumerators == NULL; + } + +};/* RecordEnumerator */ + }/* CVC4::theory::datatypes namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 8dacf86e9..66f0c8824 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -17,6 +17,7 @@ #include "theory/theory_engine.h" #include "theory/type_enumerator.h" #include "smt/options.h" +#include "smt/smt_engine.h" #include "theory/uf/theory_uf_model.h" using namespace std; @@ -56,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 ret.toExpr(); + return d_smt.postprocess(ret).toExpr(); } /** get cardinality for sort */ diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index 9add67441..42cb998be 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -97,8 +97,40 @@ public: ~TypeEnumerator() { delete d_te; } - bool isFinished() throw() { return d_te->isFinished(); } - Node operator*() throw(NoMoreValuesException) { return **d_te; } + bool isFinished() throw() { +#ifdef CVC4_ASSERTIONS + if(d_te->isFinished()) { + try { + **d_te; + Assert(false, "expected an NoMoreValuesException to be thrown"); + } catch(NoMoreValuesException&) { + // ignore the exception, we're just asserting that it would be thrown + } + } else { + try { + **d_te; + } catch(NoMoreValuesException&) { + Assert(false, "didn't expect a NoMoreValuesException to be thrown"); + } + } +#endif /* CVC4_ASSERTIONS */ + return d_te->isFinished(); + } + Node operator*() throw(NoMoreValuesException) { +#ifdef CVC4_ASSERTIONS + try { + Node n = **d_te; + Assert(n.isConst()); + Assert(! isFinished()); + return n; + } catch(NoMoreValuesException&) { + Assert(isFinished()); + throw; + } +#else /* CVC4_ASSERTIONS */ + return **d_te; +#endif /* CVC4_ASSERTIONS */ + } TypeEnumerator& operator++() throw() { ++*d_te; return *this; } TypeEnumerator operator++(int) throw() { TypeEnumerator te = *this; ++*d_te; return te; } |