diff options
29 files changed, 59 insertions, 771 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index be24dacdd..2757e3dbe 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -27,7 +27,6 @@ #include "base/output.h" #include "expr/expr_iomanip.h" #include "expr/kind.h" -#include "expr/predicate.h" #include "options/options.h" #include "options/set_language.h" #include "parser/parser.h" @@ -1257,6 +1256,7 @@ Type ValidityChecker::intType() { } Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { +/* bool noLowerBound = l.getType().isString() && l.getConst<CVC4::String>() == "_NEGINF"; bool noUpperBound = r.getType().isString() && r.getConst<CVC4::String>() == "_POSINF"; CompatCheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l); @@ -1264,10 +1264,12 @@ Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Rational>().getNumerator()); CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Rational>().getNumerator()); return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br)); + */ + Unimplemented("Subrange types not supported by CVC4 (sorry!)"); } Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) { - Unimplemented("Predicate subtyping not supported by CVC4 yet (sorry!)"); + Unimplemented("Predicate subtyping not supported by CVC4 (sorry!)"); /* if(witness.isNull()) { return d_em->mkPredicateSubtype(pred); diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index e45c765c0..859d5a312 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -61,8 +61,6 @@ libexpr_la_SOURCES = \ variable_type_map.h \ datatype.h \ datatype.cpp \ - predicate.h \ - predicate.cpp \ record.cpp \ record.h \ uninterpreted_constant.cpp \ @@ -103,7 +101,6 @@ EXTRA_DIST = \ kind.i \ expr.i \ record.i \ - predicate.i \ variable_type_map.i \ uninterpreted_constant.i diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 735d531e1..d6249d6fd 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -842,43 +842,6 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name, new TypeNode(d_nodeManager->mkSortConstructor(name, arity)))); } -/* - not in release 1.0 -Type ExprManager::mkPredicateSubtype(Expr lambda) - throw(TypeCheckingException) { - NodeManagerScope nms(d_nodeManager); - try { - return PredicateSubtype(Type(d_nodeManager, - new TypeNode(d_nodeManager->mkPredicateSubtype(lambda)))); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} -*/ - -/* - not in release 1.0 -Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness) - throw(TypeCheckingException) { - NodeManagerScope nms(d_nodeManager); - try { - return PredicateSubtype(Type(d_nodeManager, - new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness)))); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} -*/ - -Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds) - throw(TypeCheckingException) { - NodeManagerScope nms(d_nodeManager); - try { - return SubrangeType(Type(d_nodeManager, - new TypeNode(d_nodeManager->mkSubrangeType(bounds)))); - } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(this, &e); - } -} - /** * Get the type for the given Expr and optionally do type checking. * @@ -1062,8 +1025,6 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr return to->mkTypeConst(n.getConst<TypeConstant>()); } else if(n.getKind() == kind::BITVECTOR_TYPE) { return to->mkBitVectorType(n.getConst<BitVectorSize>()); - } else if(n.getKind() == kind::SUBRANGE_TYPE) { - return to->mkSubrangeType(n.getSubrangeBounds()); } Type from_t = from->toType(n); Type& to_t = vmap.d_typeMap[from_t]; diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 07dc88fd3..8719d8ef4 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -461,8 +461,8 @@ public: /** * Make an integer subrange type as defined by the argument. */ - Type mkSubrangeType(const SubrangeBounds& bounds) - throw(TypeCheckingException); + //Type mkSubrangeType(const SubrangeBounds& bounds) + // throw(TypeCheckingException); /** Get the type of an expression */ Type getType(Expr e, bool check = false) diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index b746e0de9..f7a1d98d6 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -506,51 +506,6 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor, return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); } -TypeNode NodeManager::mkPredicateSubtype(Expr lambda) - throw(TypeCheckingExceptionPrivate) { - - Node lambdan = Node::fromExpr(lambda); - - if(lambda.isNull()) { - throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression"); - } - - TypeNode tn = lambdan.getType(); - if(! tn.isPredicateLike() || - tn.getArgTypes().size() != 1) { - stringstream ss; - ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; - throw TypeCheckingExceptionPrivate(lambdan, ss.str()); - } - - return TypeNode(mkTypeConst(Predicate(lambda))); -} - -TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness) - throw(TypeCheckingExceptionPrivate) { - - Node lambdan = Node::fromExpr(lambda); - - if(lambda.isNull()) { - throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression"); - } - - TypeNode tn = lambdan.getType(); - if(! tn.isPredicateLike() || - tn.getArgTypes().size() != 1) { - stringstream ss; - ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; - throw TypeCheckingExceptionPrivate(lambdan, ss.str()); - } - - return TypeNode(mkTypeConst(Predicate(lambda, witness))); -} - -TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) - throw(TypeCheckingExceptionPrivate) { - return TypeNode(mkTypeConst(bounds)); -} - TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) { if( index==types.size() ){ if( d_data.isNull() ){ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1d1150842..44c116558 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -875,31 +875,6 @@ public: TypeNode mkSortConstructor(const std::string& name, size_t arity); /** - * Make a predicate subtype type defined by the given LAMBDA - * expression. A TypeCheckingExceptionPrivate can be thrown if - * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at - * proving that the resulting predicate subtype is inhabited. - */ - TypeNode mkPredicateSubtype(Expr lambda) - throw(TypeCheckingExceptionPrivate); - - /** - * Make a predicate subtype type defined by the given LAMBDA - * expression and whose non-emptiness is witnessed by the given - * witness. A TypeCheckingExceptionPrivate can be thrown if lambda - * is not a LAMBDA, or is ill-typed, or if the witness is not a - * witness or ill-typed. - */ - TypeNode mkPredicateSubtype(Expr lambda, Expr witness) - throw(TypeCheckingExceptionPrivate); - - /** - * Make an integer subrange type as defined by the argument. - */ - TypeNode mkSubrangeType(const SubrangeBounds& bounds) - throw(TypeCheckingExceptionPrivate); - - /** * Get the type for the given node and optionally do type checking. * * Initial type computation will be near-constant time if diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp deleted file mode 100644 index eaf587110..000000000 --- a/src/expr/predicate.cpp +++ /dev/null @@ -1,99 +0,0 @@ -/********************* */ -/*! \file predicate.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Representation of predicates for predicate subtyping - ** - ** Simple class to represent predicates for predicate subtyping. - ** Instances of this class are carried as the payload of - ** the CONSTANT-metakinded SUBTYPE_TYPE types. - **/ -#include "expr/predicate.h" - -#include "base/cvc4_assert.h" -#include "expr/expr.h" - - -using namespace std; - -namespace CVC4 { - -Predicate::Predicate(const Predicate& p) - : d_predicate(new Expr(p.getExpression())) - , d_witness(new Expr(p.getWitness())) -{} - -Predicate::Predicate(const Expr& e) throw(IllegalArgumentException) - : d_predicate(new Expr(e)) - , d_witness(new Expr()) -{ - PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null"); - PrettyCheckArgument(e.getType().isPredicate(), e, - "Expression given is not predicate"); - PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, - "Expression given is not predicate of a single argument"); -} - -Predicate::Predicate(const Expr& e, const Expr& w) - throw(IllegalArgumentException) - : d_predicate(new Expr(e)) - , d_witness(new Expr(w)) -{ - PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null"); - PrettyCheckArgument(e.getType().isPredicate(), e, - "Expression given is not predicate"); - PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, - "Expression given is not predicate of a single argument"); -} - -Predicate::~Predicate() { - delete d_predicate; - delete d_witness; -} - -Predicate& Predicate::operator=(const Predicate& p){ - (*d_predicate) = p.getExpression(); - (*d_witness) = p.getWitness(); - return *this; -} - - -// Predicate::operator Expr() const { -// return d_predicate; -// } - -const Expr& Predicate::getExpression() const { - return *d_predicate; -} - -const Expr& Predicate::getWitness() const { - return *d_witness; -} - -bool Predicate::operator==(const Predicate& p) const { - return getExpression() == p.getExpression() && - getWitness() == p.getWitness(); -} - -std::ostream& operator<<(std::ostream& out, const Predicate& p) { - out << p.getExpression(); - const Expr& witness = p.getWitness(); - if(! witness.isNull()) { - out << " : " << witness; - } - return out; -} - -size_t PredicateHashFunction::operator()(const Predicate& p) const { - ExprHashFunction h; - return h(p.getWitness()) * 5039 + h(p.getExpression()); -} - -}/* CVC4 namespace */ diff --git a/src/expr/predicate.h b/src/expr/predicate.h deleted file mode 100644 index 99e589fcd..000000000 --- a/src/expr/predicate.h +++ /dev/null @@ -1,72 +0,0 @@ -/********************* */ -/*! \file predicate.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Representation of predicates for predicate subtyping - ** - ** Simple class to represent predicates for predicate subtyping. - ** Instances of this class are carried as the payload of - ** the CONSTANT-metakinded SUBTYPE_TYPE types. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__PREDICATE_H -#define __CVC4__PREDICATE_H - -#include "base/exception.h" - -namespace CVC4 { - -class Predicate; - -std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC; - -struct CVC4_PUBLIC PredicateHashFunction { - size_t operator()(const Predicate& p) const; -};/* class PredicateHashFunction */ - -}/* CVC4 namespace */ - - -namespace CVC4 { -class CVC4_PUBLIC Expr; -}/* CVC4 namespace */ - - -namespace CVC4 { -class CVC4_PUBLIC Predicate { -public: - - Predicate(const Expr& e) throw(IllegalArgumentException); - Predicate(const Expr& e, const Expr& w) throw(IllegalArgumentException); - - Predicate(const Predicate& p); - ~Predicate(); - Predicate& operator=(const Predicate& p); - - //operator Expr() const; - - const Expr& getExpression() const; - const Expr& getWitness() const; - - bool operator==(const Predicate& p) const; - - friend std::ostream& CVC4::operator<<(std::ostream& out, const Predicate& p); - friend size_t PredicateHashFunction::operator()(const Predicate& p) const; - -private: - Expr* d_predicate; - Expr* d_witness; -};/* class Predicate */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__PREDICATE_H */ diff --git a/src/expr/predicate.i b/src/expr/predicate.i deleted file mode 100644 index aa80a98b5..000000000 --- a/src/expr/predicate.i +++ /dev/null @@ -1,12 +0,0 @@ -%{ -#include "expr/predicate.h" -%} - -%rename(equals) CVC4::Predicate::operator==(const Predicate&) const; -%rename(toExpr) CVC4::Predicate::operator Expr() const; - -%rename(apply) CVC4::PredicateHashFunction::operator()(const Predicate&) const; - -%ignore CVC4::operator<<(std::ostream&, const Predicate&); - -%include "expr/predicate.h" diff --git a/src/expr/type.cpp b/src/expr/type.cpp index bb3ce0f58..8bcb0f8d5 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -329,20 +329,6 @@ bool Type::isSortConstructor() const { return d_typeNode->isSortConstructor(); } -/** Is this a predicate subtype */ -/* - not in release 1.0 -bool Type::isPredicateSubtype() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isPredicateSubtype(); -} -*/ - -/** Is this an integer subrange */ -bool Type::isSubrange() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isSubrange(); -} - size_t FunctionType::getArity() const { return d_typeNode->getNumChildren() - 1; } @@ -505,20 +491,6 @@ SortConstructorType::SortConstructorType(const Type& t) PrettyCheckArgument(isNull() || isSortConstructor(), this); } -/* - not in release 1.0 -PredicateSubtype::PredicateSubtype(const Type& t) - throw(IllegalArgumentException) : - Type(t) { - PrettyCheckArgument(isNull() || isPredicateSubtype(), this); -} -*/ - -SubrangeType::SubrangeType(const Type& t) - throw(IllegalArgumentException) : - Type(t) { - PrettyCheckArgument(isNull() || isSubrange(), this); -} - unsigned BitVectorType::getSize() const { return d_typeNode->getBitVectorSize(); } @@ -666,11 +638,6 @@ Type PredicateSubtype::getParentType() const { } */ -SubrangeBounds SubrangeType::getSubrangeBounds() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->getSubrangeBounds(); -} - size_t TypeHashFunction::operator()(const Type& t) const { return TypeNodeHashFunction()(NodeManager::fromType(t)); } diff --git a/src/expr/type.h b/src/expr/type.h index 04b2907ff..25f0c5436 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -372,7 +372,7 @@ public: * Is this an integer subrange type? * @return true if this is an integer subrange type */ - bool isSubrange() const; + //bool isSubrange() const; /** * Outputs a string representation of this type to the stream. @@ -584,7 +584,6 @@ public: Type getParentType() const; };/* class PredicateSubtype */ -#endif /* 0 */ /** * Class encapsulating an integer subrange type. @@ -600,6 +599,7 @@ public: SubrangeBounds getSubrangeBounds() const; };/* class SubrangeType */ +#endif /* 0 */ /** * Class encapsulating the bit-vector type. diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 6e16ee9fa..383a31dd0 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -106,15 +106,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { return false; } } - if(isSubrange()) { - if(t.isSubrange()) { - return t.getSubrangeBounds() <= getSubrangeBounds(); - } else { - return t.getKind() == kind::TYPE_CONSTANT && - ( t.getConst<TypeConstant>() == INTEGER_TYPE || - t.getConst<TypeConstant>() == REAL_TYPE ); - } - } if(isTuple() && t.isTuple()) { const Datatype& dt1 = getDatatype(); const Datatype& dt2 = t.getDatatype(); @@ -151,9 +142,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { } return true; } - if(isPredicateSubtype()) { - return getSubtypeParentType().isSubtypeOf(t); - } if(isSet() && t.isSet()) { return getSetElementType().isSubtypeOf(t.getSetElementType()); } @@ -205,28 +193,13 @@ bool TypeNode::isComparableTo(TypeNode t) const { if(isArray() && t.isArray()) { return getArrayIndexType().isComparableTo(t.getArrayIndexType()) && getArrayConstituentType().isComparableTo(t.getArrayConstituentType()); } - //if(isPredicateSubtype()) { - // return t.isComparableTo(getSubtypeParentType()); - //} return false; } -Node TypeNode::getSubtypePredicate() const { - Assert(isPredicateSubtype()); - return Node::fromExpr(getConst<Predicate>().getExpression()); -} - -TypeNode TypeNode::getSubtypeParentType() const { - Assert(isPredicateSubtype()); - return getSubtypePredicate().getType().getArgTypes()[0]; -} - TypeNode TypeNode::getBaseType() const { TypeNode realt = NodeManager::currentNM()->realType(); if (isSubtypeOf(realt)) { return realt; - } else if (isPredicateSubtype()) { - return getSubtypeParentType().getBaseType(); } else if (isParametricDatatype()) { vector<Type> v; for(size_t i = 1; i < getNumChildren(); ++i) { @@ -264,14 +237,12 @@ std::vector<TypeNode> TypeNode::getParamTypes() const { /** Is this a tuple type? */ bool TypeNode::isTuple() const { - return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ) || - ( isPredicateSubtype() && getSubtypeParentType().isTuple() ); + return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ); } /** Is this a record type? */ bool TypeNode::isRecord() const { - return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() ) || - ( isPredicateSubtype() && getSubtypeParentType().isRecord() ); + return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() ); } size_t TypeNode::getTupleLength() const { @@ -375,11 +346,7 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { return TypeNode(); // null type } default: - //if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { - // return t0; // t0 is a constant type - //} else { - return TypeNode(); // null type - //} + return TypeNode(); // null type } } else if(t1.getKind() == kind::TYPE_CONSTANT) { return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases @@ -394,11 +361,7 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: case kind::TESTER_TYPE: - //if( t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) { - // return t0; - //} else { - return TypeNode(); - //} + return TypeNode(); case kind::FUNCTION_TYPE: return TypeNode(); // Not sure if this is right case kind::SET_TYPE: { @@ -423,47 +386,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { case kind::SEXPR_TYPE: Unimplemented("haven't implemented leastCommonType for symbolic expressions yet"); return TypeNode(); - case kind::SUBTYPE_TYPE: - //if(t1.isPredicateSubtype()){ - // // This is the case where both t0 and t1 are predicate subtypes. - // return leastCommonPredicateSubtype(t0, t1); - //}else{ // t0 is a predicate subtype and t1 is not - // return commonTypeNode(t1, t0, isLeast); //decrease the number of special cases - //} - return TypeNode(); - case kind::SUBRANGE_TYPE: - /* - if(t1.isSubrange()) { - const SubrangeBounds& t0SR = t0.getSubrangeBounds(); - const SubrangeBounds& t1SR = t1.getSubrangeBounds(); - if(SubrangeBounds::joinIsBounded(t0SR, t1SR)) { - SubrangeBounds j = SubrangeBounds::join(t0SR, t1SR); - return NodeManager::currentNM()->mkSubrangeType(j); - } else { - return NodeManager::currentNM()->integerType(); - } - } else if(t1.isPredicateSubtype()) { - // t0 is a subrange - // t1 is not a subrange - // t1 is a predicate subtype - if(t1.isInteger()) { - return NodeManager::currentNM()->integerType(); - } else if(t1.isReal()) { - return NodeManager::currentNM()->realType(); - } else { - return TypeNode(); - } - } else { - // t0 is a subrange - // t1 is not a subrange - // t1 is not a type constant && is not a predicate subtype - // t1 cannot be real subtype or integer. - Assert(t1.isReal()); - Assert(t1.isInteger()); - return TypeNode(); - } -*/ - return TypeNode(); case kind::DATATYPE_TYPE: if( t0.isTuple() && t1.isTuple() ){ const Datatype& dt1 = t0.getDatatype(); @@ -490,9 +412,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { if(!t1.isParametricDatatype()) { return TypeNode(); } - while(t1.getKind() != kind::PARAMETRIC_DATATYPE) { - t1 = t1.getSubtypeParentType(); - } if(t0[0] != t1[0] || t0.getNumChildren() != t1.getNumChildren()) { return TypeNode(); } @@ -508,38 +427,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { } } -TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){ - Assert(t0.isPredicateSubtype()); - Assert(t1.isPredicateSubtype()); - - std::vector<TypeNode> t0stack; - t0stack.push_back(t0); - while(t0stack.back().isPredicateSubtype()){ - t0stack.push_back(t0stack.back().getSubtypeParentType()); - } - std::vector<TypeNode> t1stack; - t1stack.push_back(t1); - while(t1stack.back().isPredicateSubtype()){ - t1stack.push_back(t1stack.back().getSubtypeParentType()); - } - - Assert(!t0stack.empty()); - Assert(!t1stack.empty()); - - if(t0stack.back() == t1stack.back()){ - TypeNode mostGeneral = t1stack.back(); - t0stack.pop_back(); t1stack.pop_back(); - while(!t0stack.empty() && t1stack.empty() && t0stack.back() == t1stack.back()){ - mostGeneral = t0stack.back(); - t0stack.pop_back(); t1stack.pop_back(); - } - return mostGeneral; - }else{ - return leastCommonTypeNode(t0stack.back(), t1stack.back()); - } -} - - Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) { TypeNode ntn = n.getType(); Assert( ntn.isComparableTo( tn ) ); @@ -581,8 +468,7 @@ Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) { /** Is this a sort kind */ bool TypeNode::isSort() const { - return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) || - ( isPredicateSubtype() && getSubtypeParentType().isSort() ); + return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ); } /** Is this a sort constructor kind */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 1a8bb14ed..8dd80bc37 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -620,27 +620,9 @@ public: /** Is this a sort constructor kind */ bool isSortConstructor() const; - /** Is this a subtype predicate */ - bool isPredicateSubtype() const; - - /** Get the predicate defining this subtype */ - Node getSubtypePredicate() const; - - /** - * Get the parent type of this subtype; note that it could be - * another subtype. - */ - TypeNode getSubtypeParentType() const; - /** Get the most general base type of the type */ TypeNode getBaseType() const; - /** Is this a subrange */ - bool isSubrange() const; - - /** Get the bounds defining this subrange */ - const SubrangeBounds& getSubrangeBounds() const; - /** * Returns the leastUpperBound in the extended type lattice of the two types. * If this is \top, i.e. there is no inhabited type that contains both, @@ -657,13 +639,7 @@ public: static Node getEnsureTypeCondition( Node n, TypeNode tn ); private: static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast); - - /** - * Returns the leastUpperBound in the extended type lattice of two - * predicate subtypes. - */ - static TypeNode leastCommonPredicateSubtype(TypeNode t0, TypeNode t1); - + /** * Indents the given stream a given amount of spaces. * @@ -852,22 +828,18 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const { inline bool TypeNode::isBoolean() const { return - ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) || - ( isPredicateSubtype() && getSubtypeParentType().isBoolean() ); + ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ); } inline bool TypeNode::isInteger() const { return - ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) || - isSubrange() || - ( isPredicateSubtype() && getSubtypeParentType().isInteger() ); + ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ); } inline bool TypeNode::isReal() const { return ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) || - isInteger() || - ( isPredicateSubtype() && getSubtypeParentType().isReal() ); + isInteger(); } inline bool TypeNode::isString() const { @@ -944,43 +916,27 @@ inline TypeNode TypeNode::getRangeType() const { /** Is this a symbolic expression type? */ inline bool TypeNode::isSExpr() const { - return getKind() == kind::SEXPR_TYPE || - ( isPredicateSubtype() && getSubtypeParentType().isSExpr() ); -} - -/** Is this a predicate subtype */ -inline bool TypeNode::isPredicateSubtype() const { - return getKind() == kind::SUBTYPE_TYPE; -} - -/** Is this a subrange type */ -inline bool TypeNode::isSubrange() const { - return getKind() == kind::SUBRANGE_TYPE || - ( isPredicateSubtype() && getSubtypeParentType().isSubrange() ); + return getKind() == kind::SEXPR_TYPE; } /** Is this a floating-point type */ inline bool TypeNode::isFloatingPoint() const { - return getKind() == kind::FLOATINGPOINT_TYPE || - ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint() ); + return getKind() == kind::FLOATINGPOINT_TYPE; } /** Is this a bit-vector type */ inline bool TypeNode::isBitVector() const { - return getKind() == kind::BITVECTOR_TYPE || - ( isPredicateSubtype() && getSubtypeParentType().isBitVector() ); + return getKind() == kind::BITVECTOR_TYPE; } /** Is this a datatype type */ inline bool TypeNode::isDatatype() const { - return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE || - ( isPredicateSubtype() && getSubtypeParentType().isDatatype() ); + return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE; } /** Is this a parametric datatype type */ inline bool TypeNode::isParametricDatatype() const { - return getKind() == kind::PARAMETRIC_DATATYPE || - ( isPredicateSubtype() && getSubtypeParentType().isParametricDatatype() ); + return getKind() == kind::PARAMETRIC_DATATYPE; } /** Is this a codatatype type */ @@ -1013,15 +969,13 @@ inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const { return ( getKind() == kind::FLOATINGPOINT_TYPE && getConst<FloatingPointSize>().exponent() == exp && - getConst<FloatingPointSize>().significand() == sig ) || - ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint(exp,sig) ); + getConst<FloatingPointSize>().significand() == sig ); } /** Is this a bit-vector type of size <code>size</code> */ inline bool TypeNode::isBitVector(unsigned size) const { return - ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size ) || - ( isPredicateSubtype() && getSubtypeParentType().isBitVector(size) ); + ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size ); } /** Get the datatype specification from a datatype type */ @@ -1054,16 +1008,6 @@ inline unsigned TypeNode::getBitVectorSize() const { return getConst<BitVectorSize>(); } -inline const SubrangeBounds& TypeNode::getSubrangeBounds() const { - Assert(isSubrange()); - if(getKind() == kind::SUBRANGE_TYPE){ - return getConst<SubrangeBounds>(); - }else{ - Assert(isPredicateSubtype()); - return getSubtypeParentType().getSubrangeBounds(); - } -} - #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index c865332e2..171c6cab0 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1293,7 +1293,8 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, << "] inappropriate: range must be nonempty!"; PARSER_STATE->parseError(ss.str()); } - t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2)); + PARSER_STATE->unimplementedFeature("subrange typing not supported in this release"); + //t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2)); } /* tuple types / old-style function types */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 69ba63a47..936a7261e 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -145,12 +145,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } break; } - case kind::SUBRANGE_TYPE: - out << '[' << n.getConst<SubrangeBounds>() << ']'; - break; - case kind::SUBTYPE_TYPE: - out << "SUBTYPE(" << n.getConst<Predicate>() << ")"; - break; case kind::TYPE_CONSTANT: switch(TypeConstant tc = n.getConst<TypeConstant>()) { case REAL_TYPE: @@ -398,12 +392,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo toStream(out, n[0], depth, types, true); const Datatype& dt = ((DatatypeType)t.toType()).getDatatype(); int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() ); + Assert( sindex>=0 ); out << '.' << sindex; }else if( t.isRecord() ){ toStream(out, n[0], depth, types, true); const Record& rec = t.getRecord(); const Datatype& dt = ((DatatypeType)t.toType()).getDatatype(); int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() ); + Assert( sindex>=0 ); std::pair<std::string, Type> fld = rec[sindex]; out << '.' << fld.first; }else{ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2ba593377..aa9c17e5a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -281,19 +281,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; } - case kind::SUBRANGE_TYPE: { - const SubrangeBounds& bounds = n.getConst<SubrangeBounds>(); - // No way to represent subranges in SMT-LIBv2; this is inspired - // by yices format (but isn't identical to it). - out << "(subrange " << bounds.lower << ' ' << bounds.upper << ')'; - break; - } - case kind::SUBTYPE_TYPE: - // No way to represent predicate subtypes in SMT-LIBv2; this is - // inspired by yices format (but isn't identical to it). - out << "(subtype " << n.getConst<Predicate>() << ')'; - break; - case kind::DATATYPE_TYPE: { const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() )); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f6b17e4cb..327f978e4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -545,8 +545,6 @@ class SmtEnginePrivate : public NodeManagerListener { /** TODO: whether certain preprocess steps are necessary */ //bool d_needsExpandDefs; - //bool d_needsRewriteBoolTerms; - //bool d_needsConstrainSubTypes; public: /** @@ -625,14 +623,6 @@ private: void compressBeforeRealAssertions(size_t before); /** - * Any variable in an assertion that is declared as a subtype type - * (predicate subtype or integer subrange type) must be constrained - * to be in that type. - */ - void constrainSubtypes(TNode n, AssertionPipeline& assertions) - throw(); - - /** * Trace nodes back to their assertions using CircuitPropagator's * BackEdgesMap. */ @@ -679,9 +669,7 @@ public: d_abstractValueMap(&d_fakeContext), d_abstractValues(), d_simplifyAssertionsDepth(0), - //d_needsExpandDefs(true), - //d_needsRewriteBoolTerms(true), - //d_needsConstrainSubTypes(true), //TODO + //d_needsExpandDefs(true), //TODO? d_iteSkolemMap(), d_iteRemover(smt.d_userContext), d_pbsProcessor(smt.d_userContext), @@ -3270,64 +3258,6 @@ void SmtEnginePrivate::unconstrainedSimp() { d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref()); } - -void SmtEnginePrivate::constrainSubtypes(TNode top, AssertionPipeline& assertions) - throw() { - - Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl; - - set<TNode> done; - stack<TNode> worklist; - worklist.push(top); - done.insert(top); - - do { - TNode n = worklist.top(); - worklist.pop(); - - TypeNode t = n.getType(); - if(t.isPredicateSubtype()) { - WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl; - Node pred = t.getSubtypePredicate(); - Kind k; - // pred can be a LAMBDA, a function constant, or a datatype tester - Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred.getType() << endl; - if(d_smt.d_definedFunctions->find(pred) != d_smt.d_definedFunctions->end()) { - k = kind::APPLY; - } else if(pred.getType().isTester()) { - k = kind::APPLY_TESTER; - } else { - k = kind::APPLY_UF; - } - Node app = NodeManager::currentNM()->mkNode(k, pred, n); - Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k << ") " << app << endl; - assertions.push_back(app); - } else if(t.isSubrange()) { - SubrangeBounds bounds = t.getSubrangeBounds(); - Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl; - if(bounds.lower.hasBound()) { - Node c = NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound())); - Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n); - Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl; - assertions.push_back(lb); - } - if(bounds.upper.hasBound()) { - Node c = NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound())); - Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c); - Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl; - assertions.push_back(ub); - } - } - - for(TNode::iterator i = n.begin(); i != n.end(); ++i) { - if(done.find(*i) == done.end()) { - worklist.push(*i); - done.insert(*i); - } - } - } while(! worklist.empty()); -} - void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions) { const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges(); for(vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) { @@ -4080,22 +4010,6 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - dumpAssertions("pre-constrain-subtypes", d_assertions); - { - // Any variables of subtype types need to be constrained properly. - // Careful, here: constrainSubtypes() adds to the back of - // d_assertions, but we don't need to reprocess those. - // We also can't use an iterator, because the vector may be moved in - // memory during this loop. - Chat() << "constraining subtypes..." << endl; - for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) { - constrainSubtypes(d_assertions[i], d_assertions); - } - } - dumpAssertions("post-constrain-subtypes", d_assertions); - - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - bool noConflict = true; // Unconstrained simplification diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 0884083c0..34ae30f4c 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -51,19 +51,6 @@ sort INTEGER_TYPE \ "expr/node_manager.h" \ "integer type" -constant SUBRANGE_TYPE \ - ::CVC4::SubrangeBounds \ - ::CVC4::SubrangeBoundsHashFunction \ - "util/subrange_bound.h" \ - "the type of an integer subrange" -cardinality SUBRANGE_TYPE \ - "::CVC4::theory::arith::SubrangeProperties::computeCardinality(%TYPE%)" \ - "theory/arith/theory_arith_type_rules.h" -well-founded SUBRANGE_TYPE \ - true \ - "::CVC4::theory::arith::SubrangeProperties::mkGroundTerm(%TYPE%)" \ - "theory/arith/theory_arith_type_rules.h" - constant CONST_RATIONAL \ ::CVC4::Rational \ ::CVC4::RationalHashFunction \ @@ -76,9 +63,6 @@ enumerator REAL_TYPE \ enumerator INTEGER_TYPE \ "::CVC4::theory::arith::IntegerEnumerator" \ "theory/arith/type_enumerator.h" -enumerator SUBRANGE_TYPE \ - "::CVC4::theory::arith::SubrangeEnumerator" \ - "theory/arith/type_enumerator.h" operator LT 2 "less than, x < y" operator LEQ 2 "less than or equal, x <= y" diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 59c2aaa8f..db3ae65f2 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -171,33 +171,6 @@ public: } };/* class RealNullaryOperatorTypeRule */ - -class SubrangeProperties { -public: - inline static Cardinality computeCardinality(TypeNode type) { - Assert(type.getKind() == kind::SUBRANGE_TYPE); - - const SubrangeBounds& bounds = type.getConst<SubrangeBounds>(); - if(!bounds.lower.hasBound() || !bounds.upper.hasBound()) { - return Cardinality::INTEGERS; - } - return Cardinality(bounds.upper.getBound() - bounds.lower.getBound()); - } - - inline static Node mkGroundTerm(TypeNode type) { - Assert(type.getKind() == kind::SUBRANGE_TYPE); - - const SubrangeBounds& bounds = type.getConst<SubrangeBounds>(); - if(bounds.lower.hasBound()) { - return NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound())); - } - if(bounds.upper.hasBound()) { - return NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound())); - } - return NodeManager::currentNM()->mkConst(Rational(0)); - } -};/* class SubrangeProperties */ - }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index 5d6b936a7..4cb34ed4a 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -108,55 +108,6 @@ public: };/* class IntegerEnumerator */ -class SubrangeEnumerator : public TypeEnumeratorBase<SubrangeEnumerator> { - Integer d_int; - SubrangeBounds d_bounds; - bool d_direction;// true == +, false == - - -public: - - SubrangeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : - TypeEnumeratorBase<SubrangeEnumerator>(type), - d_int(0), - d_bounds(type.getConst<SubrangeBounds>()), - d_direction(d_bounds.lower.hasBound()) { - - d_int = d_direction ? d_bounds.lower.getBound() : d_bounds.upper.getBound(); - - Assert(type.getKind() == kind::SUBRANGE_TYPE); - - // if we're counting down, there's no lower bound - Assert(d_direction || !d_bounds.lower.hasBound()); - } - - Node operator*() throw(NoMoreValuesException) { - if(isFinished()) { - throw NoMoreValuesException(getType()); - } - return NodeManager::currentNM()->mkConst(Rational(d_int)); - } - - SubrangeEnumerator& operator++() throw() { - if(d_direction) { - if(!d_bounds.upper.hasBound() || d_int <= d_bounds.upper.getBound()) { - d_int += 1; - } - } else { - // if we're counting down, there's no lower bound - d_int -= 1; - } - return *this; - } - - bool isFinished() throw() { - // if we're counting down, there's no lower bound - return d_direction && - d_bounds.upper.hasBound() && - d_int > d_bounds.upper.getBound(); - } - -};/* class SubrangeEnumerator */ - }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 4d3112129..2dbc5affd 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -36,8 +36,7 @@ struct ArraySelectTypeRule { throw TypeCheckingExceptionPrivate(n, "array select operating on non-array"); } TypeNode indexType = n[1].getType(check); - if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ - //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ //FIXME:typing + if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array"); } } @@ -56,12 +55,10 @@ struct ArrayStoreTypeRule { } TypeNode indexType = n[1].getType(check); TypeNode valueType = n[2].getType(check); - if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ - //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ //FIXME:typing + if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array"); } - if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){ - //if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){ //FIXME:typing + if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){ Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl; Debug("array-types") << "value types: " << valueType << std::endl; throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array"); diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 0ebebf1dd..12e897189 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -336,17 +336,4 @@ typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule -constant SUBTYPE_TYPE \ - ::CVC4::Predicate \ - ::CVC4::PredicateHashFunction \ - "expr/predicate.h" \ - "predicate subtype; payload is an instance of the CVC4::Predicate class" -cardinality SUBTYPE_TYPE \ - "::CVC4::theory::builtin::SubtypeProperties::computeCardinality(%TYPE%)" \ - "theory/builtin/theory_builtin_type_rules.h" -well-founded SUBTYPE_TYPE \ - "::CVC4::theory::builtin::SubtypeProperties::isWellFounded(%TYPE%)" \ - "::CVC4::theory::builtin::SubtypeProperties::mkGroundTerm(%TYPE%)" \ - "theory/builtin/theory_builtin_type_rules.h" - endtheory diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 7f86c7d0d..d8893d441 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -77,6 +77,9 @@ class EqualityTypeRule { TypeNode lhsType = n[0].getType(check); TypeNode rhsType = n[1].getType(check); + // TODO : we may want to limit cases where we have equalities between terms of different types + // equalities between (Set Int) and (Set Real) already cause strange issues in theory solver for sets + // one possibility is to only allow this for Int/Real if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) { std::stringstream ss; ss << "Subexpressions must have a common base type:" << std::endl; @@ -299,26 +302,6 @@ public: } };/* class SExprProperties */ -class SubtypeProperties { -public: - - inline static Cardinality computeCardinality(TypeNode type) { - Assert(type.getKind() == kind::SUBTYPE_TYPE); - Unimplemented("Computing the cardinality for predicate subtype not yet supported."); - } - - inline static bool isWellFounded(TypeNode type) { - Assert(type.getKind() == kind::SUBTYPE_TYPE); - Unimplemented("Computing the well-foundedness for predicate subtype not yet supported."); - } - - inline static Node mkGroundTerm(TypeNode type) { - Assert(type.getKind() == kind::SUBTYPE_TYPE); - Unimplemented("Constructing a ground term for predicate subtype not yet supported."); - } - -};/* class SubtypeProperties */ - }/* CVC4::theory::builtin namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 82d7274fa..e787ebc49 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -79,8 +79,7 @@ struct DatatypeConstructorTypeRule { Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl; TypeNode argumentType = *tchild_it; - if (!childType.isComparableTo(argumentType)) { - //if (!childType.isSubtypeOf(argumentType)) { //FIXME:typing + if (!childType.isSubtypeOf(argumentType)) { std::stringstream ss; ss << "bad type for constructor argument:\n" << "child type: " << childType << "\n" diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 1fd5f08be..23b185230 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -115,6 +115,21 @@ struct MemberTypeRule { throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set"); } TypeNode elementType = n[0].getType(check); + // TODO : still need to be flexible here due to situations like: + // + // T : (Set Int) + // S : (Set Real) + // (= (as T (Set Real)) S) + // (member 0.5 S) + // ...where (member 0.5 T) is inferred + // + // or + // + // S : (Set Real) + // (not (member 0.5 s)) + // (member 0.0 s) + // ...find model M where M( s ) = { 0 }, check model will generate (not (member 0.5 (singleton 0))) + // if(!elementType.isComparableTo(setType.getSetElementType())) { //if(!elementType.isSubtypeOf(setType.getSetElementType())) { //FIXME:typing std::stringstream ss; diff --git a/src/theory/theory.h b/src/theory/theory.h index 3ddb18754..82607a165 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -243,9 +243,6 @@ public: static inline TheoryId theoryOf(TypeNode typeNode) { Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl; TheoryId id; - while (typeNode.isPredicateSubtype()) { - typeNode = typeNode.getSubtypeParentType(); - } if (typeNode.getKind() == kind::TYPE_CONSTANT) { id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>()); } else { diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index a3c775a2a..c31de403c 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -45,8 +45,7 @@ class UfTypeRule { ++argument_it, ++argument_type_it) { TypeNode currentArgument = (*argument_it).getType(); TypeNode currentArgumentType = *argument_type_it; - if (!currentArgument.isComparableTo(currentArgumentType)) { - //if (!currentArgument.isSubtypeOf(currentArgumentType)) { //FIXME:typing + if (!currentArgument.isSubtypeOf(currentArgumentType)) { std::stringstream ss; ss << "argument type is not a subtype of the function's argument " << "type:\n" diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 9a16f68ca..17a2ea2ef 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -172,7 +172,6 @@ BUG_TESTS = \ bug576.smt2 \ bug576a.smt2 \ bug578.smt2 \ - bug585.cvc \ bug586.cvc \ bug593.smt2 \ bug595.cvc \ @@ -189,8 +188,10 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) # bug512 -- taking too long, --time-per not working perhaps? in any case, # we have a minimized version still getting tested # bug639 -- still fails, reopened bug +# bug585 -- contains subrange type (not supported) DISABLED_TESTS = \ - bug512.smt2 + bug512.smt2 \ + bug585.cvc EXTRA_DIST = $(TESTS) \ simplification_bug4.smt2.expect \ diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index b437f1878..572e2790d 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -27,11 +27,11 @@ TESTS = \ rec1.cvc \ rec2.cvc \ rec4.cvc \ - rec5.cvc \ datatype.cvc \ datatype0.cvc \ datatype1.cvc \ datatype2.cvc \ + datatype3.cvc \ datatype4.cvc \ datatype13.cvc \ empty_tuprec.cvc \ @@ -83,10 +83,10 @@ TESTS = \ tuple-no-clash.cvc \ jsat-2.6.smt2 +# rec5 -- no longer support subrange types FAILING_TESTS = \ - datatype-dump.cvc - -# takes a long time to build model on debug : datatype3.cvc + datatype-dump.cvc \ + rec5.cvc EXTRA_DIST = $(TESTS) |