Fix native language parsing of chained-store expressions (resolves bug 585). Thanks to Eric Seidel for the report. Also fixed some operator precedence problems w.r.t. store expressions and arithmetic.

5 files changed, 116 insertions, 47 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 347759c9a..79db2b629 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1454,18 +1454,6 @@ comparisonBinop[unsigned& op]
   | MEMBER_TOK
   ;
 
-term[CVC4::Expr& f]
-@init {
-  std::vector<CVC4::Expr> expressions;
-  std::vector<unsigned> operators;
-  unsigned op;
-  Type t;
-}
-  : storeTerm[f] { expressions.push_back(f); }
-    ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
-    { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
-  ;
-
 arithmeticBinop[unsigned& op]
 @init {
   op = LT(1)->getType(LT(1));
@@ -1479,14 +1467,26 @@ arithmeticBinop[unsigned& op]
   | EXP_TOK
   ;
 
+moreArrayStores[CVC4::Expr& f]
+  : COMMA arrayStore[f]
+  ;
+
 /** Parses an array/tuple/record assignment term. */
-storeTerm[CVC4::Expr& f]
+term[CVC4::Expr& f]
+@init {
+  std::vector<CVC4::Expr> expressions;
+  std::vector<unsigned> operators;
+  unsigned op;
+  Type t;
+}
   : uminusTerm[f]
     ( WITH_TOK
       ( arrayStore[f] ( COMMA arrayStore[f] )*
       | DOT ( tupleStore[f] ( COMMA DOT tupleStore[f] )*
             | recordStore[f] ( COMMA DOT recordStore[f] )* ) )
-    | /* nothing */
+    | { expressions.push_back(f); }
+      ( arithmeticBinop[op] uminusTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
+      { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
     )
   ;
 
@@ -1496,28 +1496,15 @@ storeTerm[CVC4::Expr& f]
  */
 arrayStore[CVC4::Expr& f]
 @init {
-  Expr f2, f3;
-  std::vector<Expr> dims;
+  Expr f2, k;
 }
-  : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+
-    ASSIGN_TOK uminusTerm[f3]
-    { assert(dims.size() >= 1);
-      // these loops are a bit complicated; they're only used for the
-      // multidimensional ...WITH [a][b] :=... syntax
-      for(unsigned i = 0; i < dims.size() - 1; ++i) {
-        f = MK_EXPR(CVC4::kind::SELECT, f, dims[i]);
-      }
-      // a[i][j][k] := v  turns into
-      // store(a, i, store(a[i], j, store(a[i][j], k, v)))
-      for(unsigned i = dims.size() - 1; i > 0; --i) {
-        f3 = MK_EXPR(CVC4::kind::STORE, f, dims[i], f3);
-        // strip off one layer of the select
-        f = f[0];
-      }
-
-      // outermost wrapping
-      f = MK_EXPR(CVC4::kind::STORE, f, dims[0], f3);
-    }
+  : LBRACKET formula[k] RBRACKET
+    { f2 = MK_EXPR(CVC4::kind::SELECT, f, k); }
+    ( ( arrayStore[f2]
+      | DOT ( tupleStore[f2]
+            | recordStore[f2] ) )
+    | ASSIGN_TOK term[f2] )
+    { f = MK_EXPR(CVC4::kind::STORE, f, k, f2); }
   ;
 
 /**
@@ -1528,9 +1515,8 @@ tupleStore[CVC4::Expr& f]
 @init {
   Expr f2;
 }
-  : k=numeral ASSIGN_TOK uminusTerm[f2]
-    {
-      Type t = f.getType();
+  : k=numeral
+    { Type t = f.getType();
       if(! t.isTuple()) {
         PARSER_STATE->parseError("tuple-update applied to non-tuple");
       }
@@ -1540,8 +1526,13 @@ tupleStore[CVC4::Expr& f]
         ss << "tuple is of length " << length << "; cannot update index " << k;
         PARSER_STATE->parseError(ss.str());
       }
-      f = MK_EXPR(MK_CONST(TupleUpdate(k)), f, f2);
+      f2 = MK_EXPR(MK_CONST(TupleSelect(k)), f);
     }
+    ( ( arrayStore[f2]
+      | DOT ( tupleStore[f2]
+            | recordStore[f2] ) )
+    | ASSIGN_TOK term[f2] )
+    { f = MK_EXPR(MK_CONST(TupleUpdate(k)), f, f2); }
   ;
 
 /**
@@ -1553,19 +1544,27 @@ recordStore[CVC4::Expr& f]
   std::string id;
   Expr f2;
 }
-  : identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2]
-    {
-      Type t = f.getType();
+  : identifier[id,CHECK_NONE,SYM_VARIABLE]
+    { Type t = f.getType();
       if(! t.isRecord()) {
-        PARSER_STATE->parseError("record-update applied to non-record");
+        std::stringstream ss;
+        ss << "record-update applied to non-record term" << std::endl
+           << "the term: " << f << std::endl
+           << "its type: " << t;
+        PARSER_STATE->parseError(ss.str());
       }
       const Record& rec = RecordType(t).getRecord();
       Record::const_iterator fld = rec.find(id);
       if(fld == rec.end()) {
         PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
       }
-      f = MK_EXPR(MK_CONST(RecordUpdate(id)), f, f2);
+      f2 = MK_EXPR(MK_CONST(RecordSelect(id)), f);
     }
+    ( ( arrayStore[f2]
+      | DOT ( tupleStore[f2]
+            | recordStore[f2] ) )
+    | ASSIGN_TOK term[f2] )
+    { f = MK_EXPR(MK_CONST(RecordUpdate(id)), f, f2); }
   ;
 
 /** Parses a unary minus term. */
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 5e57e9b67..128783388 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -163,9 +163,10 @@ BUG_TESTS = \
 	bug567.smt2 \
 	bug576.smt2 \
 	bug576a.smt2 \
-	bug578.smt2
+	bug578.smt2 \
+	bug585.cvc
 
-TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
+TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
 # bug512 -- taking too long, --time-per not working perhaps? in any case,
 # we have a minimized version still getting tested
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index 345856d85..c11d68780 100644
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -39,7 +39,8 @@ TESTS =	\
 	incorrect11.smt \
 	swap_t1_np_nf_ai_00005_007.cvc.smt \
 	x2.smt \
-	x3.smt
+	x3.smt \
+	parsing_ringer.cvc
 
 EXTRA_DIST = $(TESTS) \
 	bug272.smt \
diff --git a/test/regress/regress0/arrays/parsing_ringer.cvc b/test/regress/regress0/arrays/parsing_ringer.cvc
new file mode 100644
index 000000000..c9f8c9e22
--- /dev/null
+++ b/test/regress/regress0/arrays/parsing_ringer.cvc
@@ -0,0 +1,59 @@
+% Test for presentiation language parsing, some edge cases with cascading
+% store terms.  Intended to put this part of the parser "through the ringer,"
+% hence the name.
+
+% COMMAND-LINE: --incremental
+% EXPECT: sat
+% EXPECT: sat
+% EXPECT: sat
+% EXPECT: sat
+% EXPECT: sat
+% EXPECT: sat
+
+PUSH;
+
+x, y : ARRAY INT OF ARRAY INT OF ARRAY INT OF INT;
+
+% multidimensional arrays
+ASSERT x[0][0][0] = 0; %% select
+ASSERT y = x WITH [0][0][1] := 1; %% partial store
+
+CHECKSAT;
+
+% mixed stores: records of arrays of tuples, oh my
+z : [# x:ARRAY INT OF [# x:INT #], y:[ARRAY INT OF INT, ARRAY INT OF INT] #];
+
+arr1 : ARRAY INT OF [# x:INT #];
+arr2 : [ ARRAY INT OF INT, ARRAY INT OF INT ];
+
+ASSERT arr1[0].x = 0;
+ASSERT arr2.0[0] = 1;
+ASSERT arr2.1[0] = 5;
+
+ASSERT z.y.1[1] /= 1;
+ASSERT (# x:=arr1, y:=arr2 #) = z;
+
+CHECKSAT;
+
+ASSERT z.x[0].x /= z.y.0[5];
+
+CHECKSAT;
+
+ASSERT z.y.0[1] = z.x[5].x;
+
+CHECKSAT;
+
+ASSERT z.y.0[5] = z.x[-2].x;
+
+CHECKSAT;
+
+POP;
+
+a : ARRAY INT OF ARRAY INT OF INT;
+b : ARRAY INT OF INT;
+
+% ambiguity in presentation language, comma needs to bind to innermost WITH
+% causes type error if the [2]:=2 at the end is attached to the wrong WITH
+ASSERT a = a WITH [0]:=b WITH [1]:=1,[2]:=2;
+
+CHECKSAT;
diff --git a/test/regress/regress0/bug585.cvc b/test/regress/regress0/bug585.cvc
new file mode 100644
index 000000000..825cb0003
--- /dev/null
+++ b/test/regress/regress0/bug585.cvc
@@ -0,0 +1,9 @@
+% EXPECT: sat
+
+Cache: TYPE = ARRAY [0..100] OF [# addr: INT, data: REAL #];
+State: TYPE = [# pc: INT, cache: Cache #];
+
+s0: State;
+s1: State = s0 WITH .cache[10].data := 2/3;
+
+CHECKSAT;