diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-29 19:45:24 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-29 19:45:24 +0000 |
| commit | ac8b46fe3b5256e387da724b7c3abfb59d25531e (patch) | |
| tree | f2ecd4914fe011cabbc77f8a76ffc199e6398012 /src/parser/smt2/Smt2.g | |
| parent | 3cb49313dbefe6111414dafa521e006d45eb72d8 (diff) | |
(Not) Handling parameterized sorts in SMT v2
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 13 |
1 files changed, 7 insertions, 6 deletions
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 ; |