Improved compatibility layer, now supports quantifiers. Also incorporates

numerous bugfixes, and the cvc3 system test is enabled.

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 */