From fad7938f682c0cb07ecf6cb71e2efb878eecad1f Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 26 Nov 2009 03:22:53 +0000 Subject: [PATCH] Enough parsing for tonight. Added: * Everything goes through the ParserState instead of coding in lex/yacc files * Bare Boolean SMT lexer/parser * Basic commands To be completed: ParserState method implementations, parser.h/parser.cpp, make it compile and run... --- src/parser/Makefile.am | 6 +- src/parser/parser.cpp | 80 +- src/parser/parser.h | 112 ++- src/parser/parser_state.cpp | 105 ++- src/parser/parser_state.h | 254 ++++-- src/parser/pl.ypp | 2 +- src/parser/pl_scanner.lpp | 4 +- src/parser/smtlib.ypp | 1509 ++------------------------------- src/parser/smtlib_scanner.lpp | 245 ++---- 9 files changed, 509 insertions(+), 1808 deletions(-) diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 8d8730d68..256ebef0e 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -8,10 +8,8 @@ libparser_la_SOURCES = \ parser.cpp \ parser_state.cpp \ symbol_table.cpp \ - pl_scanner.lpp \ - pl.ypp -# smtlib_scanner.lpp \ -# smtlib.ypp + smtlib_scanner.lpp \ + smtlib.ypp BUILT_SOURCES = \ pl_scanner.cpp \ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 42ff506fa..1bf0341f2 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -10,85 +10,17 @@ ** Parser implementation. **/ -#include "parser/parser.h" -#include "parser/parser_state.h" -#include "parser/parser_exception.h" -#include "parser/pl.hpp" -//#include "parser/smtlib.hpp" - -// The communication entry points of the actual parsers - -// for presentation language (PL.y and PL.lex) -extern int PLparse(); -extern void *PL_createBuffer(int); -extern void PL_deleteBuffer(void *); -extern void PL_switchToBuffer(void *); -extern int PL_bufSize(); -extern void *PL_bufState(); -void PL_setInteractive(bool); - -// for smtlib language (smtlib.y and smtlib.lex) -extern int smtlibparse(); -extern void *smtlib_createBuffer(int); -extern void smtlib_deleteBuffer(void *); -extern void smtlib_switchToBuffer(void *); -extern int smtlib_bufSize(); -extern void *smtlibBufState(); -void smtlib_setInteractive(bool); +#include "parser.h" +#include "parser_state.h" +#include "parser_exception.h" namespace CVC4 { -namespace parser { - -ParserState *parserState; -Parser::Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive) throw() - : d_smt(smt), - d_is(is), - d_opts(opts), - d_lang(lang), - d_interactive(interactive), - d_buffer(0) { - - parserState->lineNum = 1; - switch(d_lang) { - case PL: - d_buffer = ::PL_createBuffer(::PL_bufSize()); - break; - case SMTLIB: - //d_buffer = ::smtlib_createBuffer(::smtlib_bufSize()); - break; - default: - Unhandled(); - } -} - -Parser::~Parser() throw() { - switch(d_lang) { - case PL: - ::PL_deleteBuffer(d_buffer); - break; - case SMTLIB: - //::smtlib_deleteBuffer(d_buffer); - break; - default: - Unhandled(); - } -} - -CVC4::Command* Parser::next() throw() { - return 0; -} - -bool Parser::done() const throw() { - return false; -} +namespace parser { -void Parser::printLocation(std::ostream & out) const throw() { -} +ParserState *_global_parser_state; -void Parser::reset() throw() { } - -}/* CVC4::parser namespace */ }/* CVC4 namespace */ + diff --git a/src/parser/parser.h b/src/parser/parser.h index 8103238b3..765fb0553 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -13,46 +13,86 @@ #ifndef __CVC4__PARSER__PARSER_H #define __CVC4__PARSER__PARSER_H +#include #include -#include "util/exception.h" -#include "parser/language.h" -#include "parser/parser_state.h" -#include "util/command.h" -#include "util/options.h" -#include "expr/expr.h" -#include "smt/smt_engine.h" -#include "util/assert.h" - -namespace CVC4 { -namespace parser { - -class Parser { - - CVC4::SmtEngine *d_smt; - std::istream &d_is; - CVC4::Options *d_opts; - Language d_lang; - bool d_interactive; - void *d_buffer; - -public: - // Constructors - Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive = false) throw(); - // Destructor - ~Parser() throw(); - // Read the next command. - CVC4::Command* next() throw(); - // Check if we are done (end of input has been reached) - bool done() const throw(); - // The same check can be done by using the class Parser's value as - // a Boolean - operator bool() const throw() { return done(); } - void printLocation(std::ostream & out) const throw(); - // Reset any local data that depends on SmtEngine - void reset() throw(); +namespace CVC4 +{ +namespace parser +{ + +// Forward declarations +class Expr; +class Command; +class ExprManager; +class ParserState; + +/** + * The parser. + */ +class Parser +{ + private: + + /** Internal parser state we are keeping */ + ParserState* d_data; + + /** Initialize the parser */ + void initParser(); + + /** Remove the parser components */ + void deleteParser(); + + public: + + /** The supported input languages */ + enum InputLanguage { + /** SMT-LIB language */ + INPUT_SMTLIB, + /** CVC language */ + INPUT_CVC + }; + + /** + * Constructor for parsing out of a file. + * @param em the expression manager to use + * @param lang the language syntax to use + * @param file_name the file to parse + */ + Parser(ExprManager* em, InputLanguage lang, const std::string& file_name); + + /** + * Destructor. + */ + ~Parser(); + + /** Parse a command */ + Command parseNextCommand(); + + /** Parse an expression of the stream */ + Expr parseNextExpression(); + + // Check if we are done (end of input has been reached) + bool done() const; + + // The same check can be done by using the class Parser's value as a Boolean + operator bool() const { return done(); } + + /** Prints the location to the output stream */ + void printLocation(std::ostream& out) const; + + /** Reset any local data */ + void reset(); + }; // end of class Parser +/** + * The global pointer to ParserTemp. Each instance of class Parser sets this pointer + * before any calls to the lexer. We do it this way because flex and bison use global + * vars, and we want each Parser object to appear independent. + */ +extern ParserState* _global_parser_state; + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp index 654fbfe32..74def84cb 100644 --- a/src/parser/parser_state.cpp +++ b/src/parser/parser_state.cpp @@ -1,25 +1,86 @@ -/********************* -*- C++ -*- */ -/** parser_state.cpp - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Parser state implementation. - **/ - -#include -#include "parser/parser_state.h" -#include "parser/parser_exception.h" - -namespace CVC4 { -namespace parser { - -void ParserState::error(const std::string& s) throw(ParserException*) { +/* + * parser_state.cpp + * + * Created on: Nov 20, 2009 + * Author: dejan + */ + +#include "parser_state.h" +#include "parser_exception.h" +#include + +using namespace std; + +namespace CVC4 +{ + +namespace parser +{ + +int ParserState::read(char* buffer, int size) +{ + if (d_input_stream) { + // Read the characters and count them in result + d_input_stream->read(buffer, size); + return d_input_stream->gcount(); + } else return 0; +} + +ParserState::ParserState() : + d_uid(0), d_prompt_main("CVC>"), d_prompt_continue("- "), d_prompt("CVC"), d_input_line(0), d_done(false) +{ + +} + +int ParserState::parseError(const std::string& s) +{ throw new ParserException(s); } -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ +string ParserState::getNextUniqueID() +{ + ostringstream ss; + ss << d_uid++; + return ss.str(); +} + +string ParserState::getCurrentPrompt() const +{ + return d_prompt; +} + +void ParserState::setPromptMain() +{ + d_prompt = d_prompt_main; +} + +void ParserState::setPromptNextLine() +{ + d_prompt = d_prompt_continue; +} + +void ParserState::increaseLineNumber() +{ + ++d_input_line; +} + +int ParserState::getLineNumber() const +{ + return d_input_line; +} + +std::string ParserState::getFileName() const +{ + return d_file_name; +} + +void ParserState::getParsedCommands(vector& commands_vector) +{ + d_commands.swap(commands_vector); + d_commands.clear(); +} + +} // End namespace parser + +} // End namespace CVC3 + diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 2bcc08bef..fbb0afe70 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -17,86 +17,182 @@ #ifndef __CVC4__PARSER__PARSER_STATE_H #define __CVC4__PARSER__PARSER_STATE_H +#include #include -#include -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "parser/symbol_table.h" -#include "parser/parser_exception.h" -#include "util/exception.h" - -namespace CVC4 { - -class SmtEngine; - -namespace parser { - -class ParserState { -private: - // Counter for uniqueID of bound variables - int d_uid; - // The main prompt when running interactive - std::string prompt1; - // The interactive prompt in the middle of a multi-line command - std::string prompt2; - // The currently used prompt - std::string prompt; -public: - CVC4::SmtEngine* smtEngine; - CVC4::ExprManager* exprManager; - SymbolTable* symbolTable; - std::istream* is; - // The current input line - int lineNum; - // File name - std::string fileName; - // The last parsed Expr - CVC4::Expr expr; - // Whether we are done or not - bool done; - // Whether we are running interactive - bool interactive; - // Whether arrays are enabled for smt-lib format - bool arrFlag; - // Whether bit-vectors are enabled for smt-lib format - bool bvFlag; - // Size of bit-vectors for smt-lib format - int bvSize; - // Did we encounter a formula query (smtlib) - bool queryParsed; - // Default constructor - ParserState() throw() - : d_uid(0), - prompt1("CVC> "), - prompt2("- "), - prompt("CVC> "), - smtEngine(0), - exprManager(0), - symbolTable(0), - is(0), - lineNum(1), - fileName(), - expr(CVC4::Expr::null()), - done(false), - interactive(false), - arrFlag(false), - bvFlag(false), - bvSize(0), - queryParsed(false) { } - // Parser error handling (implemented in parser.cpp) - void error(const std::string& s) throw(ParserException*) __attribute__((noreturn)); - // Get the next uniqueID as a string - std::string uniqueID() throw() { - std::ostringstream ss; - ss << d_uid++; - return ss.str(); - } - // Get the current prompt - std::string getPrompt() throw() { return prompt; } - // Set the prompt to the main one - void setPrompt1() throw() { prompt = prompt1; } - // Set the prompt to the secondary one - void setPrompt2() throw() { prompt = prompt2; } +#include + +namespace CVC4 +{ + +class Expr; +class ExprManager; + +namespace parser +{ + +/** + * The state of the parser. + */ +class ParserState +{ + public: + + /** Possible status values of a benchmark */ + enum BenchmarkStatus { + SATISFIABLE, + UNSATISFIABLE, + UNKNOWN + }; + + /** The default constructor. */ + ParserState(); + + /** Parser error handling */ + int parseError(const std::string& s); + + /** Get the next uniqueID as a string */ + std::string getNextUniqueID(); + + /** Get the current prompt */ + std::string getCurrentPrompt() const; + + /** Set the prompt to the main one */ + void setPromptMain(); + + /** Set the prompt to the secondary one */ + void setPromptNextLine(); + + /** Increases the current line number */ + void increaseLineNumber(); + + /** Gets the line number */ + int getLineNumber() const; + + /** Gets the file we are parsing, if any */ + std::string getFileName() const; + + /** + * Parses the next chunk of input from the stream. Reads at most size characters + * from the input stream and copies them into the buffer. + * @param the buffer to put the read characters into + * @param size the max numer of character + */ + int read(char* buffer, int size); + + /** + * Returns the vector of parsed commands in the given vector (and forgets + * about them in the local state. + */ + void getParsedCommands(std::vector& commands_vector); + + /** + * Adds the commands in the given vector. + */ + void addCommands(std::vector& commands_vector); + + /** + * Makes room for a new string literal (empties the buffer). + */ + void newStringLiteral(); + + /** + * Returns the current string literal. + */ + std::string getStringLiteral() const; + + /** + * Appends the first character of str to the string literal buffer. If + * is_escape is true, the first character should be '\' and second character + * is examined to determine the escaped character. + */ + void appendCharToStringLiteral(const char* str, bool is_escape = false); + + /** + * Sets the name of the benchmark. + */ + void setBenchmarkName(const std::string bench_name); + + /** + * Returns the benchmark name. + */ + std::string getBenchmarkName() const; + + /** + * Add the command to the list of commands. + */ + void addCommand(const Command* cmd); + + /** + * Set the status of the parsed benchmark. + */ + void setBenchmarkStatus(BenchmarkStatus status); + + /** + * Get the status of the parsed benchmark. + */ + BenchmarkStatus getBenchmarkStatus() const; + + /** + * Set the logic of the benchmark. + */ + void setBenchmarkLogic(const std::string logic); + + /** + * Declare a unary predicate (Boolean variable). + */ + void declareNewPredicate(const std::string pred_name); + + /** + * Creates a new expression, given the kind and the children + */ + CVC4::Expr* newExpression(CVC4::Kind kind, std::vector& children); + + /** + * Returns a new TRUE Boolean constant. + */ + CVC4::Expr* getNewTrue() const; + + /** + * Returns a new TRUE Boolean constant. + */ + CVC4::Expr* getNewFalse() const; + + /** + * Retruns a variable, given the name. + */ + CVC4::Expr* getNewVariableByName(const std::string var_name) const; + + private: + + /** Counter for uniqueID of bound variables */ + int d_uid; + /** The main prompt when running interactive */ + std::string d_prompt_main; + /** The interactive prompt in the middle of a multiline command */ + std::string d_prompt_continue; + /** The currently used prompt */ + std::string d_prompt; + /** The expression manager we will be using */ + ExprManager* d_expression_manager; + /** The stream we are reading off */ + std::istream* d_input_stream; + /** The current input line */ + unsigned d_input_line; + /** File we are parsing */ + std::string d_file_name; + /** Whether we are done or not */ + bool d_done; + /** Whether we are running in interactive mode */ + bool d_interactive; + + /** String to buffer the string literals */ + std::string d_string_buffer; + + /** The name of the benchmark if any */ + std::string d_benchmark_name; + + /** The vector of parsed commands if parsed as a whole */ + std::vector d_commands; }; }/* CVC4::parser namespace */ diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index a4aa7ef70..2668eabb8 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -14,8 +14,8 @@ %{ -#include #include +#include #include #include "smt/smt_engine.h" diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp index f3b866f2d..3b0f79a42 100644 --- a/src/parser/pl_scanner.lpp +++ b/src/parser/pl_scanner.lpp @@ -20,9 +20,9 @@ %{ -#include -#include #include +#include +#include #include "expr/expr_manager.h" /* for the benefit of parsePL_defs.h */ #include "util/command.h" diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index e616b3a65..8e6d99f6e 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -11,42 +11,29 @@ ** commands in SMT-LIB language. **/ -#include "smt/smt_engine.h" -#include "parser/parser_exception.h" +#include "cvc4_expr.h" #include "parser/parser_state.h" - -#include +#include "util/command.h" // Exported shared data namespace CVC4 { - extern ParserState* parserState; +namespace parser { + extern ParserState* _global_parser_state; +} } -// Define shortcuts for various things -#define TMP CVC4::parserState -#define EXPR CVC4::parserState->expr -#define VC (CVC4::parserState->vc) -#define ARRAYSENABLED (CVC4::parserState->arrFlag) -#define BVENABLED (CVC4::parserState->bvFlag) -#define BVSIZE (CVC4::parserState->bvSize) -#define RAT(args) CVC4::newRational args -#define QUERYPARSED CVC4::parserState->queryParsed -// Suppress the bogus warning suppression in bison (it generates -// compile error) +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; + +// Suppress the bogus warning suppression in bison (it generates compile error) #undef __GNUC_MINOR__ -/* stuff that lives in smtlib.lex */ +/** stuff that lives in smtlib_scanner.lpp */ extern int smtliblex(void); -int smtliberror(const char *s) -{ - std::ostringstream ss; - ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum - << ": " << s; - return CVC4::parserState->error(ss.str()); -} - - +/** Error call */ +int smtliberror(const char *s) { return _global_parser_state->parseError(s); } #define YYLTYPE_IS_TRIVIAL 1 #define YYMAXDEPTH 10485760 @@ -54,36 +41,29 @@ int smtliberror(const char *s) %} %union { - std::string *str; - std::vector *strvec; - CVC4::Expr *node; - std::vector *vec; - std::pair, std::vector > *pat_ann; -}; + std::string *p_string; + std::vector *p_string_vector; + + CVC4::Expr *p_expression; + std::vector *p_expression_vector; + + CVC4::Command *p_command; + std::vector *p_command_vector; -%start cmd + CVC4::parser::ParserState::BenchmarkStatus d_bench_status; + + CVC4::Kind d_kind; + +}; -/* strings are for better error messages. - "_TOK" is so macros don't conflict with kind names */ +%start benchmark -%type bench_attributes sort_symbs fun_symb_decls pred_symb_decls -%type an_exprs an_formulas quant_vars an_terms fun_symb fun_pred_symb -%type pattern -%type benchmark bench_name bench_attribute -%type status fun_symb_decl fun_sig pred_symb_decl pred_sig -%type an_expr an_formula quant_var an_atom prop_atom -%type an_term basic_term sort_symb pred_symb -%type var fvar -%type logic_name quant_symb connective user_value attribute annotation -%type annotations -%type patterns_annotations +%token NUMERAL_TOK +%token SYM_TOK +%token STRING_TOK +%token USER_VAL_TOK -%token NUMERAL_TOK -%token SYM_TOK -%token STRING_TOK -%token AR_SYMB -%token USER_VAL_TOK %token TRUE_TOK %token FALSE_TOK %token ITE_TOK @@ -94,20 +74,10 @@ int smtliberror(const char *s) %token OR_TOK %token XOR_TOK %token IFF_TOK -%token EXISTS_TOK -%token FORALL_TOK %token LET_TOK %token FLET_TOK %token NOTES_TOK -%token CVC_COMMAND_TOK %token LOGIC_TOK -%token COLON_TOK -%token LBRACKET_TOK -%token RBRACKET_TOK -%token LCURBRACK_TOK -%token RCURBRACK_TOK -%token LPAREN_TOK -%token RPAREN_TOK %token SAT_TOK %token UNSAT_TOK %token UNKNOWN_TOK @@ -118,1424 +88,113 @@ int smtliberror(const char *s) %token EXTRASORTS_TOK %token EXTRAFUNS_TOK %token EXTRAPREDS_TOK +%token DISTINCT_TOK +%token COLON_TOK +%token LBRACKET_TOK +%token RBRACKET_TOK +%token LPAREN_TOK +%token RPAREN_TOK %token DOLLAR_TOK %token QUESTION_TOK -%token DISTINCT_TOK + %token EOF_TOK -%token PAT_TOK -%% -cmd: - benchmark - { - EXPR = *$1; - delete $1; - YYACCEPT; - } -; +%type bench_name logic_name pred_symb attribute user_value +%type status +%type an_formula an_atom prop_atom +%type an_formulas; +%type connective; + +%% benchmark: - LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK - { - if (!QUERYPARSED) - $4->push_back(CVC4::Expr(VC->listExpr("_CHECKSAT", CVC4::Expr(VC->idExpr("_TRUE_EXPR"))))); - $$ = new CVC4::Expr(VC->listExpr("_SEQ",*$4)); - delete $4; - } + LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK { + _global_parser_state->setBenchmarkName(*$3); + } | EOF_TOK - { - TMP->done = true; - $$ = new CVC4::Expr(); - } -; +; -bench_name: - SYM_TOK - { - $$ = NULL; - delete $1; - } -; +bench_name: SYM_TOK; bench_attributes: bench_attribute - { - $$ = new std::vector; - if ($1) { - $$->push_back(*$1); - delete $1; - } - } | bench_attributes bench_attribute - { - $$ = $1; - if ($2) { - $$->push_back(*$2); - delete $2; - } - } ; bench_attribute: - COLON_TOK ASSUMPTION_TOK an_formula - { - $$ = new CVC4::Expr(VC->listExpr("_ASSERT", *$3)); - delete $3; - } - | COLON_TOK FORMULA_TOK an_formula - { - $$ = new CVC4::Expr(VC->listExpr("_CHECKSAT", *$3)); - QUERYPARSED = true; - delete $3; - } - | COLON_TOK STATUS_TOK status - { - $$ = NULL; - } - | COLON_TOK LOGIC_TOK logic_name - { - ARRAYSENABLED = false; - BVENABLED = false; - CVC4::Expr cmd; - if (*$3 == "QF_UF") { - cmd = CVC4::Expr(VC->listExpr("_TYPE", VC->idExpr("U"))); - } - else if (*$3 == "QF_A" || - *$3 == "QF_AX") { - ARRAYSENABLED = true; - std::vector tmp; - tmp.push_back(VC->listExpr("_TYPE", VC->idExpr("Index"))); - tmp.push_back(VC->listExpr("_TYPE", VC->idExpr("Element"))); - tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array"), - VC->listExpr("_ARRAY", - VC->idExpr("Index"), - VC->idExpr("Element")))); - cmd = CVC4::Expr(VC->listExpr("_SEQ", tmp)); - } - else if (*$3 == "QF_AUFLIA" || - *$3 == "AUFLIA") { - ARRAYSENABLED = true; - std::vector tmp; - tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array"), - VC->listExpr("_ARRAY", - VC->idExpr("_INT"), - VC->idExpr("_INT")))); - cmd = CVC4::Expr(VC->listExpr("_SEQ", tmp)); - } - else if (*$3 == "QF_AUFLIRA" || - *$3 == "AUFLIRA" || - *$3 == "QF_AUFNIRA" || - *$3 == "AUFNIRA") { - ARRAYSENABLED = true; - std::vector tmp; - tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array1"), - VC->listExpr("_ARRAY", - VC->idExpr("_INT"), - VC->idExpr("_REAL")))); - tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array2"), - VC->listExpr("_ARRAY", - VC->idExpr("_INT"), - VC->idExpr("Array1")))); - cmd = CVC4::Expr(VC->listExpr("_SEQ", tmp)); - } - else if (*$3 == "QF_AUFBV" || - *$3 == "QF_ABV") { - ARRAYSENABLED = true; - BVENABLED = true; -// $$ = new CVC4::Expr(VC->listExpr("_TYPEDEF", VC->idExpr("Array"), -// VC->listExpr("_ARRAY", -// VC->listExpr("_BITVECTOR", VC->ratExpr(32)), -// VC->listExpr("_BITVECTOR", VC->ratExpr(8))))); - } - else if (*$3 == "QF_BV" || - *$3 == "QF_UFBV") { - BVENABLED = true; - } - // This enables the new arith for QF_LRA, but this results in assertion failures in DEBUG mode -// else if (*$3 == "QF_LRA") { -// cmd = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("arith-new"), VC->ratExpr(1))); -// } - - CVC4::Expr cmd2; - if (*$3 == "AUFLIA" || - *$3 == "AUFLIRA" || - *$3 == "AUFNIRA" || - *$3 == "LRA" || - *$3 == "UFNIA") { - cmd2 = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("quant-complete-inst"), VC->ratExpr(1))); - } -// else if (*$3 == "QF_NIA" || -// *$3 == "QF_UFNRA") { -// cmd2 = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("unknown-check-model"), VC->ratExpr(1))); -// } -// else if (*$3 == "QF_LIA" || -// *$3 == "QF_AUFLIA" || -// *$3 == "QF_AX") { -// cmd2 = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("pp-budget"), VC->ratExpr(5000))); -// } - - if (cmd.isNull()) { - if (cmd2.isNull()) { - $$ = NULL; - } - else $$ = new CVC4::Expr(cmd2); - } - else { - if (!cmd2.isNull()) { - cmd = CVC4::Expr(VC->listExpr("_SEQ", cmd, cmd2)); - } - $$ = new CVC4::Expr(cmd); - } - delete $3; - } - | COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symbs RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_TYPE", *$4)); - delete $4; - } - | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK fun_symb_decls RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_SEQ", *$4)); - delete $4; - } + | COLON_TOK FORMULA_TOK an_formula { _global_parser_state->addCommand(new CheckSatCommand(*$3)); delete $3; } + | COLON_TOK STATUS_TOK status { _global_parser_state->setBenchmarkStatus($3); } + | COLON_TOK LOGIC_TOK logic_name { _global_parser_state->setBenchmarkLogic(*$3); delete $3; } | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_SEQ", *$4)); - delete $4; - } - | COLON_TOK NOTES_TOK STRING_TOK - { - $$ = NULL; - delete $3; - } - | COLON_TOK CVC_COMMAND_TOK STRING_TOK - { - $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_"+*$3))); - delete $3; - } | annotation - { - $$ = NULL; - delete $1; - } -; - -logic_name: - SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - BVSIZE = atoi($3->c_str()); - delete $3; - $$ = $1; - } - | SYM_TOK - { - $$ = $1; - } -; - -status: - SAT_TOK { $$ = NULL; } - | UNSAT_TOK { $$ = NULL; } - | UNKNOWN_TOK { $$ = NULL; } -; - -sort_symbs: - sort_symb - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } - | sort_symbs sort_symb - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } -; - -fun_symb_decls: - fun_symb_decl - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } - | - fun_symb_decls fun_symb_decl - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } -; - -fun_symb_decl: - LPAREN_TOK fun_sig annotations RPAREN_TOK - { - $$ = $2; - delete $3; - } - | LPAREN_TOK fun_sig RPAREN_TOK - { - $$ = $2; - } -; +; + +logic_name: SYM_TOK; -fun_sig: - fun_symb sort_symbs - { - if ($2->size() == 1) { - $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), (*$2)[0])); - } - else { - CVC4::Expr tmp(VC->listExpr("_ARROW", *$2)); - $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp)); - } - delete $1; - delete $2; - } +status: + SAT_TOK { $$ = ParserState::SATISFIABLE; } + | UNSAT_TOK { $$ = ParserState::UNSATISFIABLE; } + | UNKNOWN_TOK { $$ = ParserState::UNKNOWN; } ; pred_symb_decls: pred_symb_decl - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } - | - pred_symb_decls pred_symb_decl - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } + | pred_symb_decls pred_symb_decl ; pred_symb_decl: LPAREN_TOK pred_sig annotations RPAREN_TOK - { - $$ = $2; - delete $3; - } | LPAREN_TOK pred_sig RPAREN_TOK - { - $$ = $2; - } ; pred_sig: - pred_symb sort_symbs - { - std::vector tmp(*$2); - tmp.push_back(VC->idExpr("_BOOLEAN")); - CVC4::Expr tmp2(VC->listExpr("_ARROW", tmp)); - $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp2)); - delete $1; - delete $2; - } - | pred_symb - { - $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), - VC->idExpr("_BOOLEAN"))); - delete $1; - } + pred_symb { _global_parser_state->declareNewPredicate(*$1); delete $1; } ; an_formulas: - an_formula - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } - | - an_formulas an_formula - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } + an_formula { $$ = new vector; $$->push_back($1); delete $1; } + | an_formulas an_formula { $$ = $1; $$->push_back($2); delete $2; } ; an_formula: an_atom - { - $$ = $1; - } - | LPAREN_TOK connective an_formulas annotations RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$2, *$3)); - delete $2; - delete $3; - delete $4; - } - | LPAREN_TOK connective an_formulas RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$2, *$3)); - delete $2; - delete $3; - } - | LPAREN_TOK quant_symb quant_vars an_formula patterns_annotations RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4, VC->listExpr((*$5).first))); - delete $2; - delete $3; - delete $4; - delete $5; - } - | LPAREN_TOK quant_symb quant_vars an_formula RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4)); - delete $2; - delete $3; - delete $4; - } - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula annotations RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - delete $8; - } - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } - | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula annotations RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - delete $8; - } - | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } -; - -patterns_annotations: - pattern - { - $$ = new std::pair, std::vector >; - $$->first.push_back(*$1); - delete $1; - } - | annotation - { - $$ = new std::pair, std::vector >; - $$->second.push_back(*$1); - delete $1; - } - | patterns_annotations pattern - { - $1->first.push_back(*$2); - $$ = $1; - delete $2; - } - | patterns_annotations annotation - { - $1->second.push_back(*$2); - $$ = $1; - delete $2; - } - -pattern: - PAT_TOK LCURBRACK_TOK an_exprs RCURBRACK_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$3)); - delete $3; - } - -quant_vars: - quant_var - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } - | quant_vars quant_var - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } -; - -quant_var: - LPAREN_TOK var sort_symb RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$2, *$3)); - delete $2; - delete $3; - } -; - -quant_symb: - EXISTS_TOK - { - $$ = new std::string("_EXISTS"); - } - | FORALL_TOK - { - $$ = new std::string("_FORALL"); - } + | LPAREN_TOK connective an_formulas RPAREN_TOK { $$ = _global_parser_state->newExpression($2, *$3); delete $3; } ; connective: - NOT_TOK - { - $$ = new std::string("_NOT"); - } - | IMPLIES_TOK - { - $$ = new std::string("_IMPLIES"); - } - | IF_THEN_ELSE_TOK - { - $$ = new std::string("_IF"); - } - | AND_TOK - { - $$ = new std::string("_AND"); - } - | OR_TOK - { - $$ = new std::string("_OR"); - } - | XOR_TOK - { - $$ = new std::string("_XOR"); - } - | IFF_TOK - { - $$ = new std::string("_IFF"); - } + NOT_TOK { $$ = NOT; } + | IMPLIES_TOK { $$ = IMPLIES; } + | IF_THEN_ELSE_TOK { $$ = ITE; } + | AND_TOK { $$ = AND; } + | OR_TOK { $$ = OR; } + | XOR_TOK { $$ = XOR; } + | IFF_TOK { $$ = IFF; } ; -an_atom: - prop_atom - { - $$ = $1; - } - | LPAREN_TOK prop_atom annotations RPAREN_TOK - { - $$ = $2; - delete $3; - } - | LPAREN_TOK pred_symb an_terms annotations RPAREN_TOK - { - if ($4->size() == 1 && (*$4)[0] == "transclose" && - $3->size() == 2) { - $$ = new CVC4::Expr(VC->listExpr("_TRANS_CLOSURE", - *$2, (*$3)[0], (*$3)[1])); - } - else { - std::vector tmp; - tmp.push_back(*$2); - tmp.insert(tmp.end(), $3->begin(), $3->end()); - $$ = new CVC4::Expr(VC->listExpr(tmp)); - } - delete $2; - delete $3; - delete $4; - } - | LPAREN_TOK pred_symb an_terms RPAREN_TOK - { - std::vector tmp; - tmp.push_back(*$2); - tmp.insert(tmp.end(), $3->begin(), $3->end()); - $$ = new CVC4::Expr(VC->listExpr(tmp)); - delete $2; - delete $3; - } - | LPAREN_TOK DISTINCT_TOK an_terms annotations RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_DISTINCT", *$3)); - -// std::vector tmp; -// tmp.push_back(*$2); -// tmp.insert(tmp.end(), $3->begin(), $3->end()); -// $$ = new CVC4::Expr(VC->listExpr(tmp)); -// for (unsigned i = 0; i < (*$3).size(); ++i) { -// tmp.push_back(($3)[i]) -// for (unsigned j = i+1; j < (*$3).size(); ++j) { -// tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j])); -// } -// } -// $$ = new CVC4::Expr(VC->listExpr("_AND", tmp)); - delete $3; - delete $4; - } - | LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_DISTINCT", *$3)); -// std::vector tmp; -// for (unsigned i = 0; i < (*$3).size(); ++i) { -// for (unsigned j = i+1; j < (*$3).size(); ++j) { -// tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j])); -// } -// } -// $$ = new CVC4::Expr(VC->listExpr("_AND", tmp)); - delete $3; - } -; +an_atom: prop_atom; prop_atom: - TRUE_TOK - { - $$ = new CVC4::Expr(VC->idExpr("_TRUE_EXPR")); - } - | FALSE_TOK - { - $$ = new CVC4::Expr(VC->idExpr("_FALSE_EXPR")); - } - | fvar - { - $$ = $1; - } - | pred_symb - { - $$ = $1; - } + TRUE_TOK { $$ = _global_parser_state->getNewTrue(); } + | FALSE_TOK { $$ = _global_parser_state->getNewFalse(); } + | pred_symb { $$ = _global_parser_state->getNewVariableByName(*$1); delete $1; } ; -an_terms: - an_term - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } - | an_terms an_term - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } -; - -an_term: - basic_term - { - $$ = $1; - } - | LPAREN_TOK basic_term annotations RPAREN_TOK - { - $$ = $2; - delete $3; - } - | LPAREN_TOK fun_symb an_terms annotations RPAREN_TOK - { - $2->insert($2->end(), $3->begin(), $3->end()); - $$ = new CVC4::Expr(VC->listExpr(*$2)); - delete $2; - delete $3; - delete $4; - } - | LPAREN_TOK fun_symb an_terms RPAREN_TOK - { - $2->insert($2->end(), $3->begin(), $3->end()); - $$ = new CVC4::Expr(VC->listExpr(*$2)); - delete $2; - delete $3; - } - | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_IF", *$3, *$4, *$5)); - delete $3; - delete $4; - delete $5; - delete $6; - } - | LPAREN_TOK ITE_TOK an_formula an_term an_term RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_IF", *$3, *$4, *$5)); - delete $3; - delete $4; - delete $5; - } - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_term annotations RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - delete $8; - } - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_term RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } - | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_term annotations RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - delete $8; - } - | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_term RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } -; - -basic_term: - var - { - $$ = $1; - } - | fun_symb - { - if ($1->size() == 1) { - $$ = new CVC4::Expr(((*$1)[0])); - } - else { - $$ = new CVC4::Expr(VC->listExpr(*$1)); - } - delete $1; - } -; - annotations: annotation - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } | annotations annotation - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } ; - annotation: - attribute - { $$ = $1; } - | attribute user_value - { $$ = $1; } -; - -user_value: - USER_VAL_TOK - { - $$ = NULL; - delete $1; - } -; - - -sort_symb: - SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - if (BVENABLED && *$1 == "BitVec") { - $$ = new CVC4::Expr(VC->listExpr("_BITVECTOR", VC->ratExpr(*$3))); - } - else { - $$ = new CVC4::Expr(VC->listExpr(*$1, VC->ratExpr(*$3))); - } - delete $1; - delete $3; - } - | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK - { - if (BVENABLED && ARRAYSENABLED && *$1 == "Array") { - $$ = new CVC4::Expr(VC->listExpr("_ARRAY", - VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)), - VC->listExpr("_BITVECTOR", VC->ratExpr(*$5)))); - } - else { - $$ = new CVC4::Expr(VC->listExpr(*$1, VC->ratExpr(*$3), VC->ratExpr(*$5))); - } - delete $1; - delete $3; - delete $5; - } - | SYM_TOK - { - if (*$1 == "Real") { - $$ = new CVC4::Expr(VC->idExpr("_REAL")); - } else if (*$1 == "Int") { - $$ = new CVC4::Expr(VC->idExpr("_INT")); - } else { - $$ = new CVC4::Expr(VC->idExpr(*$1)); - } - delete $1; - } -; - -pred_symb: - SYM_TOK - { - if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) { - $$ = new CVC4::Expr(VC->idExpr("_BVLT")); - } - else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) { - $$ = new CVC4::Expr(VC->idExpr("_BVLE")); - } - else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) { - $$ = new CVC4::Expr(VC->idExpr("_BVGE")); - } - else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) { - $$ = new CVC4::Expr(VC->idExpr("_BVGT")); - } - else if (BVENABLED && *$1 == "bvslt") { - $$ = new CVC4::Expr(VC->idExpr("_BVSLT")); - } - else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) { - $$ = new CVC4::Expr(VC->idExpr("_BVSLE")); - } - else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) { - $$ = new CVC4::Expr(VC->idExpr("_BVSGE")); - } - else if (BVENABLED && *$1 == "bvsgt") { - $$ = new CVC4::Expr(VC->idExpr("_BVSGT")); - } - else { - $$ = new CVC4::Expr(VC->idExpr(*$1)); - } - delete $1; - } - | AR_SYMB - { - if ($1->length() == 1) { - switch ((*$1)[0]) { - case '=': $$ = new CVC4::Expr(VC->idExpr("_EQ")); break; - case '<': $$ = new CVC4::Expr(VC->idExpr("_LT")); break; - case '>': $$ = new CVC4::Expr(VC->idExpr("_GT")); break; - default: $$ = new CVC4::Expr(VC->idExpr(*$1)); break; - } - } - else { - if (*$1 == "<=") { - $$ = new CVC4::Expr(VC->idExpr("_LE")); - } else if (*$1 == ">=") { - $$ = new CVC4::Expr(VC->idExpr("_GE")); - } - else $$ = new CVC4::Expr(VC->idExpr(*$1)); - } - delete $1; - } -; - -fun_symb: - SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - $$ = new std::vector; - if (BVENABLED && *$1 == "repeat") { - $$->push_back(VC->idExpr("_BVREPEAT")); - } - else if (BVENABLED && *$1 == "zero_extend") { - $$->push_back(VC->idExpr("_BVZEROEXTEND")); - } - else if (BVENABLED && *$1 == "sign_extend") { - $$->push_back(VC->idExpr("_SX")); - $$->push_back(VC->idExpr("_smtlib")); - } - else if (BVENABLED && *$1 == "rotate_left") { - $$->push_back(VC->idExpr("_BVROTL")); - } - else if (BVENABLED && *$1 == "rotate_right") { - $$->push_back(VC->idExpr("_BVROTR")); - } - else if (BVENABLED && - $1->size() > 2 && - (*$1)[0] == 'b' && - (*$1)[1] == 'v') { - int i = 2; - while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i; - if ((*$1)[i] == '\0') { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr($1->substr(2), 10)); - } - else $$->push_back(VC->idExpr(*$1)); - } - else $$->push_back(VC->idExpr(*$1)); - $$->push_back(VC->ratExpr(*$3)); - delete $1; - delete $3; - } - | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK - { - $$ = new std::vector; - if (BVENABLED && *$1 == "extract") { - $$->push_back(VC->idExpr("_EXTRACT")); - } - else $$->push_back(VC->idExpr(*$1)); - $$->push_back(VC->ratExpr(*$3)); - $$->push_back(VC->ratExpr(*$5)); - delete $1; - delete $3; - delete $5; - } - | SYM_TOK - { - $$ = new std::vector; - if (ARRAYSENABLED && *$1 == "select") { - $$->push_back(VC->idExpr("_READ")); - } - else if (ARRAYSENABLED && *$1 == "store") { - $$->push_back(VC->idExpr("_WRITE")); - } - else if (BVENABLED && *$1 == "bit0") { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr(0)); - $$->push_back(VC->ratExpr(1)); - } - else if (BVENABLED && *$1 == "bit1") { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr(1)); - $$->push_back(VC->ratExpr(1)); - } - else if (BVENABLED && *$1 == "concat") { - $$->push_back(VC->idExpr("_CONCAT")); - } - else if (BVENABLED && *$1 == "bvnot") { - $$->push_back(VC->idExpr("_BVNEG")); - } - else if (BVENABLED && *$1 == "bvand") { - $$->push_back(VC->idExpr("_BVAND")); - } - else if (BVENABLED && *$1 == "bvor") { - $$->push_back(VC->idExpr("_BVOR")); - } - else if (BVENABLED && *$1 == "bvneg") { - $$->push_back(VC->idExpr("_BVUMINUS")); - } - else if (BVENABLED && *$1 == "bvadd") { - $$->push_back(VC->idExpr("_BVPLUS")); - } - else if (BVENABLED && *$1 == "bvmul") { - $$->push_back(VC->idExpr("_BVMULT")); - } - else if (BVENABLED && *$1 == "bvudiv") { - $$->push_back(VC->idExpr("_BVUDIV")); - } - else if (BVENABLED && *$1 == "bvurem") { - $$->push_back(VC->idExpr("_BVUREM")); - } - else if (BVENABLED && *$1 == "bvshl") { - $$->push_back(VC->idExpr("_BVSHL")); - } - else if (BVENABLED && *$1 == "bvlshr") { - $$->push_back(VC->idExpr("_BVLSHR")); - } - - else if (BVENABLED && *$1 == "bvnand") { - $$->push_back(VC->idExpr("_BVNAND")); - } - else if (BVENABLED && *$1 == "bvnor") { - $$->push_back(VC->idExpr("_BVNOR")); - } - else if (BVENABLED && *$1 == "bvxor") { - $$->push_back(VC->idExpr("_BVXOR")); - } - else if (BVENABLED && *$1 == "bvxnor") { - $$->push_back(VC->idExpr("_BVXNOR")); - } - else if (BVENABLED && *$1 == "bvcomp") { - $$->push_back(VC->idExpr("_BVCOMP")); - } - - else if (BVENABLED && *$1 == "bvsub") { - $$->push_back(VC->idExpr("_BVSUB")); - } - else if (BVENABLED && *$1 == "bvsdiv") { - $$->push_back(VC->idExpr("_BVSDIV")); - } - else if (BVENABLED && *$1 == "bvsrem") { - $$->push_back(VC->idExpr("_BVSREM")); - } - else if (BVENABLED && *$1 == "bvsmod") { - $$->push_back(VC->idExpr("_BVSMOD")); - } - else if (BVENABLED && *$1 == "bvashr") { - $$->push_back(VC->idExpr("_BVASHR")); - } - - // For backwards compatibility: - else if (BVENABLED && *$1 == "shift_left0") { - $$->push_back(VC->idExpr("_CONST_WIDTH_LEFTSHIFT")); - } - else if (BVENABLED && *$1 == "shift_right0") { - $$->push_back(VC->idExpr("_RIGHTSHIFT")); - } - else if (BVENABLED && *$1 == "sign_extend") { - $$->push_back(VC->idExpr("_SX")); - $$->push_back(VC->idExpr("_smtlib")); - } - - // Bitvector constants - else if (BVENABLED && - $1->size() > 2 && - (*$1)[0] == 'b' && - (*$1)[1] == 'v') { - bool done = false; - if ((*$1)[2] >= '0' && (*$1)[2] <= '9') { - int i = 3; - while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i; - if ((*$1)[i] == '\0') { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr($1->substr(2), 10)); - $$->push_back(VC->ratExpr(32)); - done = true; - } - } - else if ($1->size() > 5) { - std::string s = $1->substr(0,5); - if (s == "bvbin") { - int i = 5; - while ((*$1)[i] >= '0' && (*$1)[i] <= '1') ++i; - if ((*$1)[i] == '\0') { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr($1->substr(5), 2)); - $$->push_back(VC->ratExpr(i-5)); - done = true; - } - } - else if (s == "bvhex") { - int i = 5; - char c = (*$1)[i]; - while ((c >= '0' && c <= '9') || - (c >= 'a' && c <= 'f') || - (c >= 'A' && c <= 'F')) { - ++i; - c =(*$1)[i]; - } - if ((*$1)[i] == '\0') { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr($1->substr(5), 16)); - $$->push_back(VC->ratExpr(i-5)); - done = true; - } - } - } - if (!done) $$->push_back(VC->idExpr(*$1)); - } - else { - $$->push_back(VC->idExpr(*$1)); - } - delete $1; - } - | AR_SYMB - { - $$ = new std::vector; - if ($1->length() == 1) { - switch ((*$1)[0]) { - case '+': $$->push_back(VC->idExpr("_PLUS")); break; - case '-': $$->push_back(VC->idExpr("_MINUS")); break; - case '*': $$->push_back(VC->idExpr("_MULT")); break; - case '~': $$->push_back(VC->idExpr("_UMINUS")); break; - case '/': $$->push_back(VC->idExpr("_DIVIDE")); break; - // case '=': $$->push_back(VC->idExpr("_EQ")); break; - // case '<': $$->push_back(VC->idExpr("_LT")); break; - // case '>': $$->push_back(VC->idExpr("_GT")); break; - default: $$->push_back(VC->idExpr(*$1)); - } - } - // else { - // if (*$1 == "<=") { - // $$->push_back(VC->idExpr("_LE")); - // } else if (*$1 == ">=") { - // $$->push_back(VC->idExpr("_GE")); - // } - else $$->push_back(VC->idExpr(*$1)); - // } - delete $1; - } - | NUMERAL_TOK - { - $$ = new std::vector; - $$->push_back(VC->ratExpr(*$1)); - delete $1; - } -; - -attribute: - COLON_TOK SYM_TOK - { - $$ = $2; - } -; - -var: - QUESTION_TOK SYM_TOK - { - $$ = new CVC4::Expr(VC->idExpr("_"+*$2)); - delete $2; - } -; - -fvar: - DOLLAR_TOK SYM_TOK - { - $$ = new CVC4::Expr(VC->idExpr("_"+*$2)); - delete $2; - } -; - -an_exprs: - an_expr - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } - | - an_exprs an_expr - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } -; - -an_expr: - var - { - $$ = $1; - } - | fvar - { - $$ = $1; - } - | LPAREN_TOK fun_pred_symb an_terms annotations RPAREN_TOK - { - $2->insert($2->end(), $3->begin(), $3->end()); - $$ = new CVC4::Expr(VC->listExpr(*$2)); - delete $2; - delete $3; - delete $4; - } - | LPAREN_TOK fun_pred_symb an_terms RPAREN_TOK - { - $2->insert($2->end(), $3->begin(), $3->end()); - $$ = new CVC4::Expr(VC->listExpr(*$2)); - delete $2; - delete $3; - } - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_expr annotations RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - delete $8; - } - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_expr RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } - | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_expr annotations RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - delete $8; - } - | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_expr RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } -; - -fun_pred_symb: - SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - $$ = new std::vector; - if (BVENABLED && *$1 == "repeat") { - $$->push_back(VC->idExpr("_BVREPEAT")); - } - else if (BVENABLED && *$1 == "zero_extend") { - $$->push_back(VC->idExpr("_BVZEROEXTEND")); - } - else if (BVENABLED && *$1 == "sign_extend") { - $$->push_back(VC->idExpr("_SX")); - $$->push_back(VC->idExpr("_smtlib")); - } - else if (BVENABLED && *$1 == "rotate_left") { - $$->push_back(VC->idExpr("_BVROTL")); - } - else if (BVENABLED && *$1 == "rotate_right") { - $$->push_back(VC->idExpr("_BVROTR")); - } - else if (BVENABLED && - $1->size() > 2 && - (*$1)[0] == 'b' && - (*$1)[1] == 'v') { - int i = 2; - while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i; - if ((*$1)[i] == '\0') { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr($1->substr(2), 10)); - } - else $$->push_back(VC->idExpr(*$1)); - } - else $$->push_back(VC->idExpr(*$1)); - $$->push_back(VC->ratExpr(*$3)); - delete $1; - delete $3; - } - | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK - { - $$ = new std::vector; - if (BVENABLED && *$1 == "extract") { - $$->push_back(VC->idExpr("_EXTRACT")); - } - else $$->push_back(VC->idExpr(*$1)); - $$->push_back(VC->ratExpr(*$3)); - $$->push_back(VC->ratExpr(*$5)); - delete $1; - delete $3; - delete $5; - } - | SYM_TOK - { - $$ = new std::vector; - if (ARRAYSENABLED && *$1 == "select") { - $$->push_back(VC->idExpr("_READ")); - } - else if (ARRAYSENABLED && *$1 == "store") { - $$->push_back(VC->idExpr("_WRITE")); - } - else if (BVENABLED && *$1 == "bit0") { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr(0)); - $$->push_back(VC->ratExpr(1)); - } - else if (BVENABLED && *$1 == "bit1") { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr(1)); - $$->push_back(VC->ratExpr(1)); - } - else if (BVENABLED && *$1 == "concat") { - $$->push_back(VC->idExpr("_CONCAT")); - } - else if (BVENABLED && *$1 == "bvnot") { - $$->push_back(VC->idExpr("_BVNEG")); - } - else if (BVENABLED && *$1 == "bvand") { - $$->push_back(VC->idExpr("_BVAND")); - } - else if (BVENABLED && *$1 == "bvor") { - $$->push_back(VC->idExpr("_BVOR")); - } - else if (BVENABLED && *$1 == "bvneg") { - $$->push_back(VC->idExpr("_BVUMINUS")); - } - else if (BVENABLED && *$1 == "bvadd") { - $$->push_back(VC->idExpr("_BVPLUS")); - } - else if (BVENABLED && *$1 == "bvmul") { - $$->push_back(VC->idExpr("_BVMULT")); - } - else if (BVENABLED && *$1 == "bvudiv") { - $$->push_back(VC->idExpr("_BVUDIV")); - } - else if (BVENABLED && *$1 == "bvurem") { - $$->push_back(VC->idExpr("_BVUREM")); - } - else if (BVENABLED && *$1 == "bvshl") { - $$->push_back(VC->idExpr("_BVSHL")); - } - else if (BVENABLED && *$1 == "bvlshr") { - $$->push_back(VC->idExpr("_BVLSHR")); - } - - else if (BVENABLED && *$1 == "bvnand") { - $$->push_back(VC->idExpr("_BVNAND")); - } - else if (BVENABLED && *$1 == "bvnor") { - $$->push_back(VC->idExpr("_BVNOR")); - } - else if (BVENABLED && *$1 == "bvxor") { - $$->push_back(VC->idExpr("_BVXOR")); - } - else if (BVENABLED && *$1 == "bvxnor") { - $$->push_back(VC->idExpr("_BVXNOR")); - } - else if (BVENABLED && *$1 == "bvcomp") { - $$->push_back(VC->idExpr("_BVCOMP")); - } - - else if (BVENABLED && *$1 == "bvsub") { - $$->push_back(VC->idExpr("_BVSUB")); - } - else if (BVENABLED && *$1 == "bvsdiv") { - $$->push_back(VC->idExpr("_BVSDIV")); - } - else if (BVENABLED && *$1 == "bvsrem") { - $$->push_back(VC->idExpr("_BVSREM")); - } - else if (BVENABLED && *$1 == "bvsmod") { - $$->push_back(VC->idExpr("_BVSMOD")); - } - else if (BVENABLED && *$1 == "bvashr") { - $$->push_back(VC->idExpr("_BVASHR")); - } + attribute { delete $1; } + | attribute user_value { delete $1; delete $2; } + ; - // predicates - else if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) { - $$->push_back(VC->idExpr("_BVLT")); - } - else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) { - $$->push_back(VC->idExpr("_BVLE")); - } - else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) { - $$->push_back(VC->idExpr("_BVGE")); - } - else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) { - $$->push_back(VC->idExpr("_BVGT")); - } - else if (BVENABLED && *$1 == "bvslt") { - $$->push_back(VC->idExpr("_BVSLT")); - } - else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) { - $$->push_back(VC->idExpr("_BVSLE")); - } - else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) { - $$->push_back(VC->idExpr("_BVSGE")); - } - else if (BVENABLED && *$1 == "bvsgt") { - $$->push_back(VC->idExpr("_BVSGT")); - } +user_value: USER_VAL_TOK; - // For backwards compatibility: - else if (BVENABLED && *$1 == "shift_left0") { - $$->push_back(VC->idExpr("_CONST_WIDTH_LEFTSHIFT")); - } - else if (BVENABLED && *$1 == "shift_right0") { - $$->push_back(VC->idExpr("_RIGHTSHIFT")); - } - else if (BVENABLED && *$1 == "sign_extend") { - $$->push_back(VC->idExpr("_SX")); - $$->push_back(VC->idExpr("_smtlib")); - } +pred_symb: SYM_TOK; - // Bitvector constants - else if (BVENABLED && - $1->size() > 2 && - (*$1)[0] == 'b' && - (*$1)[1] == 'v') { - bool done = false; - if ((*$1)[2] >= '0' && (*$1)[2] <= '9') { - int i = 3; - while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i; - if ((*$1)[i] == '\0') { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr($1->substr(2), 10)); - $$->push_back(VC->ratExpr(32)); - done = true; - } - } - else if ($1->size() > 5) { - std::string s = $1->substr(0,5); - if (s == "bvbin") { - int i = 5; - while ((*$1)[i] >= '0' && (*$1)[i] <= '1') ++i; - if ((*$1)[i] == '\0') { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr($1->substr(5), 2)); - $$->push_back(VC->ratExpr(i-5)); - done = true; - } - } - else if (s == "bvhex") { - int i = 5; - char c = (*$1)[i]; - while ((c >= '0' && c <= '9') || - (c >= 'a' && c <= 'f') || - (c >= 'A' && c <= 'F')) { - ++i; - c =(*$1)[i]; - } - if ((*$1)[i] == '\0') { - $$->push_back(VC->idExpr("_BVCONST")); - $$->push_back(VC->ratExpr($1->substr(5), 16)); - $$->push_back(VC->ratExpr(i-5)); - done = true; - } - } - } - if (!done) $$->push_back(VC->idExpr(*$1)); - } - else { - $$->push_back(VC->idExpr(*$1)); - } - delete $1; - } - | AR_SYMB - { - $$ = new std::vector; - if ($1->length() == 1) { - switch ((*$1)[0]) { - case '+': $$->push_back(VC->idExpr("_PLUS")); break; - case '-': $$->push_back(VC->idExpr("_MINUS")); break; - case '*': $$->push_back(VC->idExpr("_MULT")); break; - case '~': $$->push_back(VC->idExpr("_UMINUS")); break; - case '/': $$->push_back(VC->idExpr("_DIVIDE")); break; - case '=': $$->push_back(VC->idExpr("_EQ")); break; - case '<': $$->push_back(VC->idExpr("_LT")); break; - case '>': $$->push_back(VC->idExpr("_GT")); break; - default: $$->push_back(VC->idExpr(*$1)); - } - } - else { - if (*$1 == "<=") { - $$->push_back(VC->idExpr("_LE")); - } else if (*$1 == ">=") { - $$->push_back(VC->idExpr("_GE")); - } - else $$->push_back(VC->idExpr(*$1)); - } - delete $1; - } - | NUMERAL_TOK - { - $$ = new std::vector; - $$->push_back(VC->ratExpr(*$1)); - delete $1; - } -; +attribute: + COLON_TOK SYM_TOK { $$ = $2; } + ; %% diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp index b367b0d93..4d9cb8213 100644 --- a/src/parser/smtlib_scanner.lpp +++ b/src/parser/smtlib_scanner.lpp @@ -19,190 +19,105 @@ %option prefix="smtlib" %{ + #include -#include "parser/smtlib.hpp" -#include "util/debug.h" +#include "parser_state.h" +#include "smtlib.hpp" namespace CVC4 { - extern ParserTemp* parserTemp; +namespace parser { + extern ParserState* _global_parser_state; } - -extern int smtlib_inputLine; -extern char *smtlibtext; - -extern int smtliberror (const char *msg); - -static int smtlibinput(std::istream& is, char* buf, int size) { - int res; - if(is) { - // If interactive, read line by line; otherwise read as much as we - // can gobble - if(CVC4::parserTemp->interactive) { - // Print the current prompt - std::cout << CVC4::parserTemp->getPrompt() << std::flush; - // Set the prompt to "middle of the command" one - CVC4::parserTemp->setPrompt2(); - // Read the line - is.getline(buf, size-1); - } else // Set the terminator char to 0 - is.getline(buf, size-1, 0); - // If failbit is set, but eof is not, it means the line simply - // didn't fit; so we clear the state and keep on reading. - bool partialStr = is.fail() && !is.eof(); - if(partialStr) - is.clear(); - - for(res = 0; resis, buf, max_size); +using CVC4::parser::_global_parser_state; -int smtlib_bufSize() { return YY_BUF_SIZE; } -YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; } - -/* some wrappers for methods that need to refer to a struct. - These are used by CVC4::Parser. */ -void *smtlib_createBuffer(int sz) { - return (void *)smtlib_create_buffer(NULL, sz); -} -void smtlib_deleteBuffer(void *buf_state) { - smtlib_delete_buffer((struct yy_buffer_state *)buf_state); -} -void smtlib_switchToBuffer(void *buf_state) { - smtlib_switch_to_buffer((struct yy_buffer_state *)buf_state); -} -void *smtlib_bufState() { - return (void *)smtlib_buf_state(); -} - -void smtlib_setInteractive(bool is_interactive) { - yy_set_interactive(is_interactive); -} - -// File-static (local to this file) variables and functions -static std::string _string_lit; +extern char *smtlibtext; - static char escapeChar(char c) { - switch(c) { - case 'n': return '\n'; - case 't': return '\t'; - default: return c; - } - } -// for now, we don't have subranges. -// -// ".." { return DOTDOT_TOK; } -/*OPCHAR (['!#?\_$&\|\\@])*/ +// Redefine the input buffer function to read from an istream +#define YY_INPUT(buffer,result,max_size) result = _global_parser_state->read(buffer, max_size); %} -%x COMMENT -%x STRING_LITERAL -%x USER_VALUE -%s PAT_MODE +%x COMMENT +%x STRING_LITERAL +%x SYM_TOK +%x USER_VALUE LETTER ([a-zA-Z]) -DIGIT ([0-9]) +DIGIT ([0-9]) OPCHAR (['\.\_]) IDCHAR ({LETTER}|{DIGIT}|{OPCHAR}) + %% -[\n] { CVC4::parserTemp->lineNum++; } -[ \t\r\f] { /* skip whitespace */ } - -{DIGIT}+"\."{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; } -{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; - } - -";" { BEGIN COMMENT; } -"\n" { BEGIN INITIAL; /* return to normal mode */ - CVC4::parserTemp->lineNum++; } -. { /* stay in comment mode */ } - -"\"" { BEGIN STRING_LITERAL; - _string_lit.erase(_string_lit.begin(), - _string_lit.end()); } -"\\". { /* escape characters (like \n or \") */ - _string_lit.insert(_string_lit.end(), - escapeChar(smtlibtext[1])); } -"\"" { BEGIN INITIAL; /* return to normal mode */ - smtliblval.str = new std::string(_string_lit); - return STRING_TOK; } -. { _string_lit.insert(_string_lit.end(),*smtlibtext); } - -":pat" { BEGIN PAT_MODE; - return PAT_TOK;} -"}" { BEGIN INITIAL; - return RCURBRACK_TOK; } -"{" { BEGIN USER_VALUE; - _string_lit.erase(_string_lit.begin(), - _string_lit.end()); } -"\\"[{}] { /* escape characters */ - _string_lit.insert(_string_lit.end(),smtlibtext[1]); } - -"}" { BEGIN INITIAL; /* return to normal mode */ - smtliblval.str = new std::string(_string_lit); - return USER_VAL_TOK; } - -"\n" { _string_lit.insert(_string_lit.end(),'\n'); - CVC4::parserTemp->lineNum++; } -. { _string_lit.insert(_string_lit.end(),*smtlibtext); } - -"true" { return TRUE_TOK; } -"false" { return FALSE_TOK; } -"ite" { return ITE_TOK; } -"not" { return NOT_TOK; } -"implies" { return IMPLIES_TOK; } -"if_then_else" { return IF_THEN_ELSE_TOK; } -"and" { return AND_TOK; } -"or" { return OR_TOK; } -"xor" { return XOR_TOK; } -"iff" { return IFF_TOK; } -"exists" { return EXISTS_TOK; } -"forall" { return FORALL_TOK; } -"let" { return LET_TOK; } -"flet" { return FLET_TOK; } -"notes" { return NOTES_TOK; } -"cvc_command" { return CVC_COMMAND_TOK; } -"logic" { return LOGIC_TOK; } -"sat" { return SAT_TOK; } -"unsat" { return UNSAT_TOK; } -"unknown" { return UNKNOWN_TOK; } -"assumption" { return ASSUMPTION_TOK; } -"formula" { return FORMULA_TOK; } -"status" { return STATUS_TOK; } -"benchmark" { return BENCHMARK_TOK; } -"extrasorts" { return EXTRASORTS_TOK; } -"extrafuns" { return EXTRAFUNS_TOK; } -"extrapreds" { return EXTRAPREDS_TOK; } -"distinct" { return DISTINCT_TOK; } -":pattern" { return PAT_TOK; } -":" { return COLON_TOK; } -"\[" { return LBRACKET_TOK; } -"\]" { return RBRACKET_TOK; } -"{" { return LCURBRACK_TOK;} -"}" { return RCURBRACK_TOK;} -"(" { return LPAREN_TOK; } -")" { return RPAREN_TOK; } -"$" { return DOLLAR_TOK; } -"?" { return QUESTION_TOK; } - -[=<>&@#+\-*/%|~]+ { smtliblval.str = new std::string(smtlibtext); return AR_SYMB; } -({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; } +[\n] { _global_parser_state->increaseLineNumber(); } +[ \t\r\f] { /* skip whitespace */ } + +{DIGIT}+"\."{DIGIT}+ { smtliblval.p_string = new std::string(smtlibtext); return NUMERAL_TOK; } +{DIGIT}+ { smtliblval.p_string = new std::string(smtlibtext); return NUMERAL_TOK; } + +";" { BEGIN COMMENT; } +"\n" { BEGIN INITIAL; _global_parser_state->increaseLineNumber(); } +. { /* stay in comment mode */ } + +"\"" { BEGIN STRING_LITERAL; _global_parser_state->newStringLiteral(); } +"\\". { _global_parser_state->appendCharToStringLiteral(smtlibtext, true); } +"\"" { BEGIN INITIAL; + /* return to normal mode */ + smtliblval.p_string = new std::string(_global_parser_state->getStringLiteral()); + return STRING_TOK; + } +. { _global_parser_state->appendCharToStringLiteral(smtlibtext, false); } + +"{" { BEGIN USER_VALUE; _global_parser_state->newStringLiteral(); } +"\\"[{}] { _global_parser_state->appendCharToStringLiteral(smtlibtext, true); } +"}" { BEGIN INITIAL; + /* return to normal mode */ + smtliblval.p_string = new std::string(_global_parser_state->getStringLiteral()); + return USER_VAL_TOK; + } +. { _global_parser_state->appendCharToStringLiteral(smtlibtext, false); } + + +"true" { return TRUE_TOK; } +"false" { return FALSE_TOK; } +"ite" { return ITE_TOK; } +"not" { return NOT_TOK; } +"implies" { return IMPLIES_TOK; } +"if_then_else" { return IF_THEN_ELSE_TOK; } +"and" { return AND_TOK; } +"or" { return OR_TOK; } +"xor" { return XOR_TOK; } +"iff" { return IFF_TOK; } +"let" { return LET_TOK; } +"flet" { return FLET_TOK; } +"notes" { return NOTES_TOK; } +"logic" { return LOGIC_TOK; } +"sat" { return SAT_TOK; } +"unsat" { return UNSAT_TOK; } +"unknown" { return UNKNOWN_TOK; } +"assumption" { return ASSUMPTION_TOK; } +"formula" { return FORMULA_TOK; } +"status" { return STATUS_TOK; } +"benchmark" { return BENCHMARK_TOK; } +"extrasorts" { return EXTRASORTS_TOK; } +"extrafuns" { return EXTRAFUNS_TOK; } +"extrapreds" { return EXTRAPREDS_TOK; } +"distinct" { return DISTINCT_TOK; } +":" { return COLON_TOK; } +"\[" { return LBRACKET_TOK; } +"\]" { return RBRACKET_TOK; } +"(" { return LPAREN_TOK; } +")" { return RPAREN_TOK; } +"$" { return DOLLAR_TOK; } +"?" { return QUESTION_TOK; } + +({LETTER})({IDCHAR})* { smtliblval.p_string = new std::string(smtlibtext); return SYM_TOK; } <> { return EOF_TOK; } -. { smtliberror("Illegal input character."); } +. { _global_parser_state->parseError("Illegal input character."); } + %% -- 2.30.2