summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node_manager.h3
-rw-r--r--src/expr/type_node.cpp136
-rw-r--r--src/expr/type_node.h27
-rw-r--r--src/theory/arith/theory_arith_type_rules.h9
-rw-r--r--src/theory/booleans/theory_bool_type_rules.h8
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h10
-rw-r--r--src/theory/datatypes/theory_datatypes_type_rules.h3
-rw-r--r--src/theory/uf/theory_uf_type_rules.h8
-rw-r--r--src/util/integer_cln_imp.h12
-rw-r--r--src/util/integer_gmp_imp.h10
-rw-r--r--src/util/subrange_bound.h38
-rw-r--r--test/regress/regress0/Makefile.am3
12 files changed, 241 insertions, 26 deletions
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<TypeConstant>()) {
+ 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<TypeNode> t0stack;
+ t0stack.push_back(t0);
+ while(t0stack.back().isPredicateSubtype()){
+ t0stack.push_back(t0stack.back().getSubtypeBaseType());
+ }
+ std::vector<TypeNode> 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,9 +593,25 @@ 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.
*
* @param out the stream to indent
@@ -940,7 +954,12 @@ inline unsigned TypeNode::getBitVectorSize() const {
inline const SubrangeBounds& TypeNode::getSubrangeBounds() const {
Assert(isSubrange());
- return getConst<SubrangeBounds>();
+ if(getKind() == kind::SUBRANGE_TYPE){
+ return getConst<SubrangeBounds>();
+ }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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback