diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-28 01:10:16 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-28 01:10:16 +0000 |
commit | cf287f593931a1c4fc141e18845b4c5d36879889 (patch) | |
tree | 4dad0f555b7db01fbeedcd9eace394cd8f7a0fb4 /src/theory/arrays | |
parent | b7b1c1d99ffa333704af2c8ecd60b1af8833a28b (diff) |
Improved compatibility layer, now supports quantifiers. Also incorporates
numerous bugfixes, and the cvc3 system test is enabled.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/kinds | 7 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 23 |
2 files changed, 21 insertions, 9 deletions
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 986654cd3..3850fab98 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -15,9 +15,12 @@ rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arra operator ARRAY_TYPE 2 "array type" cardinality ARRAY_TYPE \ - "::CVC4::theory::arrays::CardinalityComputer::computeCardinality(%TYPE%)" \ + "::CVC4::theory::arrays::ArraysProperties::computeCardinality(%TYPE%)" \ + "theory/arrays/theory_arrays_type_rules.h" +well-founded ARRAY_TYPE \ + "::CVC4::theory::arrays::ArraysProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::arrays::ArraysProperties::mkGroundTerm(%TYPE%)" \ "theory/arrays/theory_arrays_type_rules.h" -well-founded ARRAY_TYPE false enumerator ARRAY_TYPE \ "::CVC4::theory::arrays::ArrayEnumerator" \ diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 8b31a31f9..854b5449f 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -22,6 +22,7 @@ #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H #include "theory/arrays/theory_arrays_rewriter.h" // for array-constant attributes +#include "theory/type_enumerator.h" namespace CVC4 { namespace theory { @@ -37,7 +38,7 @@ struct ArraySelectTypeRule { throw TypeCheckingExceptionPrivate(n, "array select operating on non-array"); } TypeNode indexType = n[1].getType(check); - if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ + if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array"); } } @@ -56,10 +57,10 @@ struct ArrayStoreTypeRule { } TypeNode indexType = n[1].getType(check); TypeNode valueType = n[2].getType(check); - if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ + if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array"); } - if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){ + if(!valueType.isComparableTo(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"); @@ -167,11 +168,11 @@ struct ArrayTableFunTypeRule { throw TypeCheckingExceptionPrivate(n, "array table fun arg 1 is non-array"); } TypeNode indexType = n[2].getType(check); - if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ + if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array table fun arg 2 does not match type of array"); } indexType = n[3].getType(check); - if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ + if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array table fun arg 3 does not match type of array"); } } @@ -179,7 +180,7 @@ struct ArrayTableFunTypeRule { } };/* struct ArrayTableFunTypeRule */ -struct CardinalityComputer { +struct ArraysProperties { inline static Cardinality computeCardinality(TypeNode type) { Assert(type.getKind() == kind::ARRAY_TYPE); @@ -188,7 +189,15 @@ struct CardinalityComputer { return valueCard ^ indexCard; } -};/* struct CardinalityComputer */ + + inline static bool isWellFounded(TypeNode type) { + return type[0].isWellFounded() && type[1].isWellFounded(); + } + + inline static Node mkGroundTerm(TypeNode type) { + return *TypeEnumerator(type); + } +};/* struct ArraysProperties */ }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ |