the array-store "construle" for isConst

2 files changed, 22 insertions, 1 deletions

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 4a8695ec4..7386ec5c2 100644
--- 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 ccbb37936..b130b78fd 100644
--- 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) {