From: Tim King Date: Fri, 18 May 2012 23:48:38 +0000 (+0000) Subject: This commit adds TypeNode::leastCommonTypeNode(). The special case for arithmetic... X-Git-Tag: cvc5-1.0.0~8152 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ea8139dc7b727bf48bd7b7c6b169d763618a1f2a;p=cvc5.git This commit adds TypeNode::leastCommonTypeNode(). The special case for arithmetic in TypeNode::operator==() has been removed. A number of faulty type checking checks were switched to use isSubtypeOf. The resolves bug #339 --- diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 2bcf5e18c..00fe6baa8 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -573,9 +573,6 @@ public: /** Get the (singleton) type for reals. */ inline TypeNode realType(); - /** Get the (singleton) type for pseudobooleans. */ - inline TypeNode pseudobooleanType(); - /** Get the (singleton) type for strings. */ inline TypeNode stringType(); diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 3f5c3a032..7b093d11a 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -181,4 +181,140 @@ bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const { return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1]; } +TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + + Assert(!t0.isNull()); + Assert(!t1.isNull()); + + if(EXPECT_TRUE(t0 == t1)){ + return t0; + }else{ // t0 != t1 + if(t0.getKind()== kind::TYPE_CONSTANT){ + switch(t0.getConst()) { + case INTEGER_TYPE: + if(t1.isInteger()){ + // t0 == IntegerType && t1.isInteger() + return t0; //IntegerType + }else if(t1.isReal()){ + // t0 == IntegerType && t1.isReal() && !t1.isInteger() + return NodeManager::currentNM()->realType(); // RealType + }else{ + return TypeNode(); //null type + } + case REAL_TYPE: + if(t1.isReal()){ + return t0; // RealType + }else{ + return TypeNode(); // null type + } + default: + if(t1.isPredicateSubtype() && t1.getSubtypeBaseType().isSubtypeOf(t0)){ + return t0; // t0 is a constant type + }else{ + return TypeNode(); // null type + } + } + }else if(t1.getKind() == kind::TYPE_CONSTANT){ + return leastCommonTypeNode(t1, t0); //decrease the number of special cases + }else{ + // t0 != t1 && + // t0.getKind() == kind::TYPE_CONSTANT && + // t1.getKind() == kind::TYPE_CONSTANT + switch(t0.getKind()){ + case kind::ARRAY_TYPE: + case kind::BITVECTOR_TYPE: + case kind::SORT_TYPE: + case kind::PARAMETRIC_DATATYPE: + case kind::CONSTRUCTOR_TYPE: + case kind::SELECTOR_TYPE: + case kind::TESTER_TYPE: + if(t1.isPredicateSubtype() && t1.getSubtypeBaseType().isSubtypeOf(t0)){ + return t0; + }else{ + return TypeNode(); + } + case kind::FUNCTION_TYPE: + return TypeNode(); // Not sure if this is right + case kind::TUPLE_TYPE: + Unimplemented(); + return TypeNode(); // Not sure if this is right + 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 leastCommonTypeNode(t1, t0); //decrease the number of special cases + } + 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(); + } + default: + Unimplemented(); + return TypeNode(); + } + } + } +} + +TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){ + Assert(t0.isPredicateSubtype()); + Assert(t1.isPredicateSubtype()); + + std::vector t0stack; + t0stack.push_back(t0); + while(t0stack.back().isPredicateSubtype()){ + t0stack.push_back(t0stack.back().getSubtypeBaseType()); + } + std::vector t1stack; + t1stack.push_back(t1); + while(t1stack.back().isPredicateSubtype()){ + t1stack.push_back(t1stack.back().getSubtypeBaseType()); + } + + 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()); + } +} + }/* CVC4 namespace */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 25b5e4bb3..482da2814 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -159,9 +159,7 @@ public: * @return true if expressions are equal, false otherwise */ bool operator==(const TypeNode& typeNode) const { - return - d_nv == typeNode.d_nv || - (typeNode.isReal() && this->isReal()); + return d_nv == typeNode.d_nv; } /** @@ -595,8 +593,24 @@ public: /** Is this a kind type (i.e., the type of a type)? */ bool isKind() 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, + * a TypeNode such that isNull() is true is returned. + * + * For more information see: http://church.cims.nyu.edu/wiki/Cvc4_Type_Lattice + */ + static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1); + private: + /** + * 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. * @@ -940,7 +954,12 @@ inline unsigned TypeNode::getBitVectorSize() const { inline const SubrangeBounds& TypeNode::getSubrangeBounds() const { Assert(isSubrange()); - return getConst(); + if(getKind() == kind::SUBRANGE_TYPE){ + return getConst(); + }else{ + Assert(isPredicateSubtype()); + return getSubtypeBaseType().getSubrangeBounds(); + } } #ifdef CVC4_DEBUG diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 69c98a255..af358b00d 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -59,7 +59,7 @@ public: } } if( check ) { - if(childType != integerType && childType != realType) { + if(!childType.isReal()) { throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm"); } } @@ -73,14 +73,13 @@ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { - TypeNode integerType = nodeManager->integerType(); - TypeNode realType = nodeManager->realType(); TypeNode lhsType = n[0].getType(check); - if (lhsType != integerType && lhsType != realType) { + if (!lhsType.isReal()) { + std::cout << lhsType << " : " << n[0] << std::endl; throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side"); } TypeNode rhsType = n[1].getType(check); - if (rhsType != integerType && rhsType != realType) { + if (!rhsType.isReal()) { throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side"); } } diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 3b30b9f59..ff6b99d77 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -50,14 +50,16 @@ class IteTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - TypeNode iteType = n[1].getType(check); + TypeNode thenType = n[1].getType(check); + TypeNode elseType = n[2].getType(check); + TypeNode iteType = TypeNode::leastCommonTypeNode(thenType, elseType); if( check ) { TypeNode booleanType = nodeManager->booleanType(); if (n[0].getType(check) != booleanType) { throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean"); } - if (iteType != n[2].getType(check)) { - throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be of the same type"); + if (iteType.isNull()) { + throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be a subtype of a common type."); } } return iteType; diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 706196f8b..52d0defd1 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -79,10 +79,10 @@ class EqualityTypeRule { TypeNode lhsType = n[0].getType(check); TypeNode rhsType = n[1].getType(check); - if ( lhsType != rhsType ) { + if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) { std::stringstream ss; ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)); - ss << "Types do not match in equation:" << std::endl; + ss << "Subtypes must have a common type:" << std::endl; ss << "Equation: " << n << std::endl; ss << "Type 1: " << lhsType << std::endl; ss << "Type 2: " << rhsType << std::endl; @@ -105,9 +105,11 @@ public: if( check ) { TNode::iterator child_it = n.begin(); TNode::iterator child_it_end = n.end(); - TypeNode firstType = (*child_it).getType(check); + TypeNode joinType = (*child_it).getType(check); for (++child_it; child_it != child_it_end; ++child_it) { - if ((*child_it).getType() != firstType) { + TypeNode currentType = (*child_it).getType(); + joinType = TypeNode::leastCommonTypeNode(joinType, currentType); + if (joinType.isNull()) { throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type"); } } diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 347bc16b3..d8d40154a 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -71,7 +71,8 @@ struct DatatypeConstructorTypeRule { for(; child_it != child_it_end; ++child_it, ++tchild_it) { TypeNode childType = (*child_it).getType(check); Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl; - if(childType != *tchild_it) { + TypeNode argumentType = *tchild_it; + if(!childType.isSubtypeOf(argumentType)) { throw TypeCheckingExceptionPrivate(n, "bad type for constructor argument"); } } diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 9b622bc15..3d7e51746 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -42,13 +42,15 @@ public: TNode::iterator argument_it_end = n.end(); TypeNode::iterator argument_type_it = fType.begin(); for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) { - if((*argument_it).getType() != *argument_type_it) { + TypeNode currentArgument = (*argument_it).getType(); + TypeNode currentArgumentType = *argument_type_it; + if(!currentArgument.isSubtypeOf(currentArgumentType)) { std::stringstream ss; ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)) - << "argument types do not match the function type:\n" + << "argument types is not a subtype of the function's argument type:\n" << "argument: " << *argument_it << "\n" << "has type: " << (*argument_it).getType() << "\n" - << "not equal: " << *argument_type_it; + << "not subtype: " << *argument_type_it; throw TypeCheckingExceptionPrivate(n, ss.str()); } } diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index d3e5c07ca..43b77df6a 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -443,10 +443,20 @@ public: /* cl_I xgcd (const cl_I& a, const cl_I& b, cl_I* u, cl_I* v) */ /* This function ("extended gcd") returns the greatest common divisor g of a and b and at the same time the representation of g as an integral linear combination of a and b: u and v with u*a+v*b = g, g >= 0. u and v will be normalized to be of smallest possible absolute value, in the following sense: If a and b are non-zero, and abs(a) != abs(b), u and v will satisfy the inequalities abs(u) <= abs(b)/(2*g), abs(v) <= abs(a)/(2*g). */ - static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){ + static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){ g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value); } + /** Returns a reference to the minimum of two integers. */ + static const Integer& min(const Integer& a, const Integer& b){ + return (a <=b ) ? a : b; + } + + /** Returns a reference to the maximum of two integers. */ + static const Integer& max(const Integer& a, const Integer& b){ + return (a >= b ) ? a : b; + } + friend class CVC4::Rational; };/* class Integer */ diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 74b4adad0..f5254a3d2 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -400,10 +400,20 @@ public: } static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){ + //see the documentation for: //mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b); mpz_gcdext (g.d_value.get_mpz_t(), s.d_value.get_mpz_t(), t.d_value.get_mpz_t(), a.d_value.get_mpz_t(), b.d_value.get_mpz_t()); } + /** Returns a reference to the minimum of two integers. */ + static const Integer& min(const Integer& a, const Integer& b){ + return (a <=b ) ? a : b; + } + + /** Returns a reference to the maximum of two integers. */ + static const Integer& max(const Integer& a, const Integer& b){ + return (a >= b ) ? a : b; + } friend class CVC4::Rational; };/* class Integer */ diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index 9d4d446bd..063e59a0f 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -57,7 +57,7 @@ public: } /** Get the finite SubrangeBound, failing an assertion if infinite. */ - Integer getBound() const throw(IllegalArgumentException) { + const Integer& getBound() const throw(IllegalArgumentException) { CheckArgument(!d_nobound, this, "SubrangeBound is infinite"); return d_bound; } @@ -130,6 +130,23 @@ public: ( hasBound() && b.hasBound() && getBound() <= b.getBound() ); } + + static SubrangeBound min(const SubrangeBound& a, const SubrangeBound& b){ + if(a.hasBound() && b.hasBound()){ + return SubrangeBound(Integer::min(a.getBound(), b.getBound())); + }else{ + return SubrangeBound(); + } + } + + static SubrangeBound max(const SubrangeBound& a, const SubrangeBound& b){ + if(a.hasBound() && b.hasBound()){ + return SubrangeBound(Integer::max(a.getBound(), b.getBound())); + }else{ + return SubrangeBound(); + } + } + };/* class SubrangeBound */ class CVC4_PUBLIC SubrangeBounds { @@ -192,6 +209,25 @@ public: return lower <= bounds.lower && upper >= bounds.upper; } + /** + * Returns true if the join of two subranges is not (- infinity, + infinity). + */ + static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){ + return (a.lower.hasBound() && b.lower.hasBound()) || + (a.upper.hasBound() && b.upper.hasBound()); + } + + /** + * Returns the join of two subranges, a and b. + * precondition: joinIsBounded(a,b) is true + */ + static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b){ + Assert(joinIsBounded(a,b)); + SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower); + SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper); + return SubrangeBounds(newLower, newUpper); + } + };/* class SubrangeBounds */ struct CVC4_PUBLIC SubrangeBoundsHashStrategy { diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index db3e1efeb..db9b4d07f 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -97,7 +97,8 @@ BUG_TESTS = \ bug239.smt \ buggy-ite.smt2 \ bug303.smt2 \ - bug310.cvc + bug310.cvc \ + bug339.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)