Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre for the report.

2 files changed, 25 insertions, 0 deletions

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 0bc973de9..c18492a58 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -41,10 +41,18 @@ constant STORE_ALL \
 # used internally by array theory
 operator ARR_TABLE_FUN 4 "array table function (internal-only symbol)"
 
+# used internally for substitutions in models (e.g. the Boolean terms converter)
+# The (single) argument is a lambda(x:T):U.  Type of the array lambda is
+# Array T of U.  Thus ARRAY_LAMBDA LAMBDA(x:INT) . (read a x) is the same array
+# as a.  ARRAY_LAMBDA LAMBDA(x:INT) . (read a (- x 1)) is the same array as
+# as a shifted over one.
+operator ARRAY_LAMBDA 1 "array lambda (internal-only symbol)"
+
 typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule
 typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
 typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule
 typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
+typerule ARRAY_LAMBDA ::CVC4::theory::arrays::ArrayLambdaTypeRule
 
 # store operations that are ordered (by index) over a store-all are constant
 construle STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 6cb31e51a..70e1c1a5b 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -178,6 +178,23 @@ struct ArrayTableFunTypeRule {
   }
 };/* struct ArrayTableFunTypeRule */
 
+struct ArrayLambdaTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::ARRAY_LAMBDA);
+    TypeNode lamType = n[0].getType(check);
+    if( check ) {
+      if(n[0].getKind() != kind::LAMBDA) {
+        throw TypeCheckingExceptionPrivate(n, "array lambda arg is non-lambda");
+      }
+    }
+    if(lamType.getNumChildren() != 2) {
+      throw TypeCheckingExceptionPrivate(n, "array lambda arg is not unary lambda");
+    }
+    return nodeManager->mkArrayType(lamType[0], lamType[1]);
+  }
+};/* struct ArrayLambdaTypeRule */
+
 struct ArraysProperties {
   inline static Cardinality computeCardinality(TypeNode type) {
     Assert(type.getKind() == kind::ARRAY_TYPE);