From: Christopher L. Conway 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 ;