From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Tue, 6 Jul 2010 17:10:53 +0000 (+0000)
Subject: Adding Array types to SMT2 parser
X-Git-Tag: cvc5-1.0.0~8939
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=86eb2490a00466d5b014976fc89b813011b663eb;p=cvc5.git

Adding Array types to SMT2 parser
---

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.");
+      }
+    }
   ;
 
 /**
diff --git a/test/regress/regress0/arr1.smt2 b/test/regress/regress0/arr1.smt2
new file mode 100644
index 000000000..844f7d8e5
--- /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)
+