Adding Array types to SMT2 parser

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 91f2f205b0deceb78aaf59223d84adeefd28be27..c23ccca6b2046332c791c55dd476489eaa85c67a 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -359,9 +359,21 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check]
 sortSymbol[CVC4::Type& t]
 @declarations {
   std::string name;
+  std::vector<CVC4::Type> args;
 }
   : sortName[name,CHECK_NONE] 
        { t = PARSER_STATE->getSort(name); }
+  | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
+    { 
+      if( name == "Array" ) {
+        if( args.size() != 2 ) {
+          PARSER_STATE->parseError("Illegal array type.");
+        }
+        t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); 
+      } else {
+        PARSER_STATE->parseError("Unhandled parameterized type.");
+      }
+    }
   ;
 
 /**

diff --git a/test/regress/regress0/arr1.smt2 b/test/regress/regress0/arr1.smt2
new file mode 100644 (file)
index 0000000..844f7d8
--- /dev/null
+++ b/test/regress/regress0/arr1.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_AX)
+(set-info  :status unsat)
+(declare-sort Index 0)
+(declare-sort Element 0)
+(declare-fun a () (Array Index Element))
+(declare-fun i1 () Index)
+(declare-fun i2 () Index)
+(assert (not (=> (= i1 i2) (= (select a i1) (select a i2)))))
+(check-sat)
+