diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:35:03 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:50:58 -0500 |
commit | 360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 (patch) | |
tree | 9e1fb4d128a62ca3e9152530dbfadb448ed49a45 /src/theory | |
parent | d6d34604fa6d4c260edfc10a5b7f543540be75f4 (diff) |
Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/kinds | 16 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 27 | ||||
-rw-r--r-- | src/theory/arith/type_enumerator.h | 49 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 9 | ||||
-rw-r--r-- | src/theory/builtin/kinds | 13 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 23 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 3 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 15 | ||||
-rw-r--r-- | src/theory/theory.h | 3 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 3 |
10 files changed, 23 insertions, 138 deletions
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" |