From 86eb2490a00466d5b014976fc89b813011b663eb Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Tue, 6 Jul 2010 17:10:53 +0000
Subject: Adding Array types to SMT2 parser

---
 src/parser/smt2/Smt2.g | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'src/parser/smt2/Smt2.g')

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 91f2f205b..c23ccca6b 100644
--- 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.");
+      }
+    }
   ;
 
 /**
-- 
cgit v1.2.3