From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Thu, 29 Apr 2010 19:45:24 +0000 (+0000)
Subject: (Not) Handling parameterized sorts in SMT v2
X-Git-Tag: cvc5-1.0.0~9097
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ac8b46fe3b5256e387da724b7c3abfb59d25531e;p=cvc5.git

(Not) Handling parameterized sorts in SMT v2
---

diff --git a/src/parser/input.h b/src/parser/input.h
index 21c5c4869..ecc2063db 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -167,7 +167,10 @@ public:
 
   /** Retrieve the text associated with a token. */
   inline static std::string tokenText(pANTLR3_COMMON_TOKEN token);
-
+  /** Retrieve an Integer from the text of a token */
+  inline static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token );
+  /** Retrieve a Rational from the text of a token */
+  inline static Rational tokenToRational(pANTLR3_COMMON_TOKEN token);
 
 protected:
   /** Create an input. This input takes ownership of the given input stream,
@@ -231,6 +234,16 @@ std::string Input::tokenText(pANTLR3_COMMON_TOKEN token) {
   return txt;
 }
 
+Integer Input::tokenToInteger(pANTLR3_COMMON_TOKEN token) {
+  Integer i( tokenText(token) );
+  return i;
+}
+
+Rational Input::tokenToRational(pANTLR3_COMMON_TOKEN token) {
+  Rational r( tokenText(token) );
+  return r;
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index ba5e8abf5..2dd680f09 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -236,14 +236,12 @@ annotatedFormula[CVC4::Expr& expr]
   | TRUE_TOK          { expr = MK_CONST(true); }
   | FALSE_TOK         { expr = MK_CONST(false); }
   | NUMERAL_TOK
-    { Integer num( Input::tokenText($NUMERAL_TOK) );
-      expr = MK_CONST(num); }
+    { expr = MK_CONST( Input::tokenToInteger($NUMERAL_TOK) ); }
   | RATIONAL_TOK
     { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
-      Rational rat( Input::tokenText($RATIONAL_TOK) );
-      expr = MK_CONST(rat); }
+      expr = MK_CONST( Input::tokenToRational($RATIONAL_TOK) ); }
     // NOTE: Theory constants go here
-    /* TODO: let, flet, quantifiers, arithmetic constants */
+    /* TODO: quantifiers, arithmetic constants */
   ;
 
 /**
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 44dd041c3..422e4b19e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -99,6 +99,7 @@ setLogic(Parser *parser, const std::string& name) {
     Unhandled(name);
   }
 }
+
 }
 
 
@@ -140,8 +141,10 @@ command returns [CVC4::Command* cmd]
     { cmd = new SetBenchmarkStatusCommand(b_status); }  
   | /* sort declaration */
     DECLARE_SORT_TOK identifier[name,CHECK_UNDECLARED,SYM_SORT] n=NUMERAL_TOK
-    // FIXME: What does the numeral argument mean?
-    { Debug("parser") << "declare sort: '" << name << "' " << n << std::endl;
+    { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl;
+      if( Input::tokenToInteger(n) > 0 ) {
+        Unimplemented("Parameterized user sorts.");
+      }
       PARSER_STATE->mkSort(name); 
       $cmd = new DeclarationCommand(name,EXPR_MANAGER->kindType()); }
   | /* function declaration */
@@ -223,12 +226,10 @@ term[CVC4::Expr& expr]
   | TRUE_TOK          { expr = MK_CONST(true); }
   | FALSE_TOK         { expr = MK_CONST(false); }
   | NUMERAL_TOK
-    { Integer num( Input::tokenText($NUMERAL_TOK) );
-      expr = MK_CONST(num); }
+    { expr = MK_CONST( Input::tokenToInteger($NUMERAL_TOK) ); }
   | RATIONAL_TOK
     { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
-      Rational rat( Input::tokenText($RATIONAL_TOK) );
-      expr = MK_CONST(rat); }
+      expr = MK_CONST( Input::tokenToRational($RATIONAL_TOK) ); }
     // NOTE: Theory constants go here
   ;