From eb63fdb37b2784d6d4340402cd0ee00ceb8f5041 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 3 Oct 2014 13:12:11 -0400
Subject: [PATCH] More array constants and parsing: better error messages,
 extend to CVC presentation language.

---
 NEWS                            |  1 +
 src/parser/cvc/Cvc.g            | 39 +++++++++++++++++++++++----------
 src/parser/smt2/Smt2.g          | 19 ++++++++++++++--
 src/printer/cvc/cvc_printer.cpp |  7 ++++++
 4 files changed, 53 insertions(+), 13 deletions(-)

diff --git a/NEWS b/NEWS
index fc8a38864..84debe315 100644
--- a/NEWS
+++ b/NEWS
@@ -6,6 +6,7 @@ Changes since 1.4
 * Support for unsat cores.
 * Simplification mode "incremental" no longer supported.
 * Support for array constants in constraints.
+* Syntax for array models have changed in some language front-ends.
 
 Changes since 1.3
 =================
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 0a440f299..74c236dd1 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1368,14 +1368,6 @@ prefixFormula[CVC4::Expr& f]
       PARSER_STATE->preemptCommand(cmd);
       f = func;
     }
-
-    /* array literals */
-  | ARRAY_TOK { PARSER_STATE->pushScope(); } LPAREN
-    boundVarDecl[ids,t] RPAREN COLON formula[f]
-    { PARSER_STATE->popScope();
-      UNSUPPORTED("array literals not supported yet");
-      f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()), ExprManager::VAR_FLAG_GLOBAL);
-    }
   ;
 
 instantiationPatterns[ CVC4::Expr& expr ]
@@ -1898,7 +1890,7 @@ simpleTerm[CVC4::Expr& f]
   std::vector<std::string> names;
   Expr e;
   Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
-  Type t;
+  Type t, t2;
 }
     /* if-then-else */
   : iteTerm[f]
@@ -1928,7 +1920,6 @@ simpleTerm[CVC4::Expr& f]
       f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), std::vector<Expr>());
     }
 
-
     /* empty set literal */
   | LBRACE RBRACE
     { f = MK_CONST(EmptySet(Type())); }
@@ -1942,6 +1933,32 @@ simpleTerm[CVC4::Expr& f]
       }
     }
 
+    /* array literals */
+  | ARRAY_TOK /* { PARSER_STATE->pushScope(); } */ LPAREN
+    restrictedType[t, CHECK_DECLARED] OF_TOK restrictedType[t2, CHECK_DECLARED]
+    RPAREN COLON simpleTerm[f]
+    { /* Eventually if we support a bound var (like a lambda) for array
+       * literals, we can use the push/pop scope. */
+      /* PARSER_STATE->popScope(); */
+      t = EXPR_MANAGER->mkArrayType(t, t2);
+      if(!f.isConst()) {
+        std::stringstream ss;
+        ss << "expected constant term inside array constant, but found "
+           << "nonconstant term" << std::endl
+           << "the term: " << f;
+        PARSER_STATE->parseError(ss.str());
+      }
+      if(!t2.isComparableTo(f.getType())) {
+        std::stringstream ss;
+        ss << "type mismatch inside array constant term:" << std::endl
+           << "array type:          " << t << std::endl
+           << "expected const type: " << t2 << std::endl
+           << "computed const type: " << f.getType();
+        PARSER_STATE->parseError(ss.str());
+      }
+      f = MK_CONST( ArrayStoreAll(t, f) );
+    }
+
     /* boolean literals */
   | TRUE_TOK  { f = MK_CONST(bool(true)); }
   | FALSE_TOK { f = MK_CONST(bool(false)); }
@@ -1986,7 +2003,7 @@ simpleTerm[CVC4::Expr& f]
   ;
 
 /**
- * Matches (and performs) a type ascription.
+ * Matches a type ascription.
  * The f arg is the term to check (it is an input-only argument).
  */
 typeAscription[const CVC4::Expr& f, CVC4::Type& t]
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4491e5643..6a98755f2 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1010,10 +1010,25 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       RPAREN_TOK term[f, f2] RPAREN_TOK
       {
         if(!type.isArray()) {
-          PARSER_STATE->parseError("(as const...) type ascription can only be used for array sorts.");
+          std::stringstream ss;
+          ss << "expected array constant term, but cast is not of array type" << std::endl
+             << "cast type: " << type;
+          PARSER_STATE->parseError(ss.str());
+        }
+        if(!f.isConst()) {
+          std::stringstream ss;
+          ss << "expected constant term inside array constant, but found "
+             << "nonconstant term:" << std::endl
+             << "the term: " << f;
+          PARSER_STATE->parseError(ss.str());
         }
         if(!ArrayType(type).getConstituentType().isComparableTo(f.getType())) {
-          PARSER_STATE->parseError("type of the array cast is not compatible with term.");
+          std::stringstream ss;
+          ss << "type mismatch inside array constant term:" << std::endl
+             << "array type:          " << type << std::endl
+             << "expected const type: " << ArrayType(type).getConstituentType() << std::endl
+             << "computed const type: " << f.getType();
+          PARSER_STATE->parseError(ss.str());
         }
         expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) );
       }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 9b3e83578..2d89d3aff 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -168,6 +168,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     }
 
+    case kind::STORE_ALL: {
+      const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
+      out << "ARRAY(" << asa.getType().getIndexType() << " OF "
+          << asa.getType().getConstituentType() << ") : " << asa.getExpr();
+      break;
+    }
+
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and print something reasonable
-- 
2.30.2