SMT2 parser: add 'as const'

This is an extension understood by Z3 and CVC4, which is the equivalent of
array_of_exprt.

Author: kroening

regression/smt2_solver/arrays/as_const1.desc

@@ -0,0 +1,7 @@
+CORE
+as_const1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

regression/smt2_solver/arrays/as_const1.smt2

@@ -0,0 +1,8 @@
+; an array consisting of all #x10
+(declare-const array (Array (_ BitVec 16) (_ BitVec 8)))
+(assert (= array ((as const (Array (_ BitVec 16) (_ BitVec 8))) #x10)))
+
+(declare-const index (_ BitVec 16))
+(assert (not (= #x10 (select array index))))
+
+(check-sat)

src/solvers/smt2/smt2_parser.cpp

@@ -690,6 +690,38 @@ exprt smt2_parsert::function_application()
                         << smt2_tokenizer.get_buffer() << '\'';
         }
       }
+      else if(smt2_tokenizer.get_buffer() == "as")
+      {
+        // This is an extension understood by Z3 and CVC4.
+        if(
+          smt2_tokenizer.peek() == smt2_tokenizert::SYMBOL &&
+          smt2_tokenizer.get_buffer() == "const")
+        {
+          next_token(); // eat the "const"
+          auto sort = this->sort();
+
+          if(sort.id() != ID_array)
+            throw error()
+              << "unexpected 'as const' expression expects array type";
+
+          const auto &array_sort = to_array_type(sort);
+
+          if(smt2_tokenizer.next_token() != smt2_tokenizert::CLOSE)
+            throw error() << "expecting ')' after sort in 'as const'";
+
+          auto value = expression();
+
+          if(value.type() != array_sort.subtype())
+            throw error() << "unexpected 'as const' with wrong element type";
+
+          if(smt2_tokenizer.next_token() != smt2_tokenizert::CLOSE)
+            throw error() << "expecting ')' at the end of 'as const'";
+
+          return array_of_exprt(value, to_array_type(sort));
+        }
+        else
+          throw error() << "unexpected 'as' expression";
+      }
       else
       {
         // just double parentheses