the array-store "construle" for isConst

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 4a8695ec4bd3555a74f01af2f6ec34fc1e1979fb..7386ec5c2857e099087e18936bc73aaac8d57f72 100644 (file)
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -44,4 +44,7 @@ typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
 typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule
 typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
 
+# store operations that are ordered (by index) over a store-all are constant
+construle STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
+
 endtheory

diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index ccbb379363982726dcb53888bb2808ac37565397..b130b78fd8b0b2ea61edeb7695d069b125e2e4af 100644 (file)
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -65,6 +65,24 @@ struct ArrayStoreTypeRule {
     }
     return arrayType;
   }
+
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
+    throw (AssertionException) {
+    Assert(n.getKind() == kind::STORE);
+    NodeManagerScope nms(nodeManager);
+
+    // TODO: test ordering of stores, and ultimate application to a store-all
+    // ALSO: ensure uniqueness of form (e.g. one constant of the array sort
+    // BOOL->INT can be represented as
+    //   [false->0, default=1]
+    // and also
+    //   [true->1, default=0]
+    // ..but by contract of isConst(), only one of these can be considered
+    // a "const" expression.
+
+    return false;
+  }
+
 };/* struct ArrayStoreTypeRule */
 
 struct ArrayTableFunTypeRule {
@@ -91,7 +109,7 @@ struct ArrayTableFunTypeRule {
     }
     return arrayType.getArrayIndexType();
   }
-};/* struct ArrayStoreTypeRule */
+};/* struct ArrayTableFunTypeRule */
 
 struct CardinalityComputer {
   inline static Cardinality computeCardinality(TypeNode type) {