diff options
| -rw-r--r-- | lib/SMT/LICENSE.CVC3 | 53 | ||||
| -rw-r--r-- | lib/SMT/Makefile | 59 | ||||
| -rw-r--r-- | lib/SMT/exception.h | 58 | ||||
| -rw-r--r-- | lib/SMT/lang.h | 66 | ||||
| -rw-r--r-- | lib/SMT/parser.cpp | 235 | ||||
| -rw-r--r-- | lib/SMT/parser.h | 79 | ||||
| -rw-r--r-- | lib/SMT/parser_exception.h | 46 | ||||
| -rw-r--r-- | lib/SMT/parser_temp.h | 85 | ||||
| -rw-r--r-- | lib/SMT/smtlib.lex | 224 | ||||
| -rw-r--r-- | lib/SMT/smtlib.y | 1222 |
10 files changed, 2127 insertions, 0 deletions
diff --git a/lib/SMT/LICENSE.CVC3 b/lib/SMT/LICENSE.CVC3 new file mode 100644 index 00000000..a70d12d5 --- /dev/null +++ b/lib/SMT/LICENSE.CVC3 @@ -0,0 +1,53 @@ +/*!\page LICENSE LICENSE + +Copyright (C) 2003-2009 by the Board of Trustees of Leland Stanford Junior +University, New York University, and the University of Iowa, hereafter +designated as the Copyright Owners. + +All rights reserved. + +Redistribution and use in source and binary forms, with or without modification, +are permitted provided that the following conditions are met: + +* Redistributions of source code must retain the above copyright notice, this +list of conditions and the following disclaimer. +* Redistributions in binary form must reproduce the above copyright notice, +this list of conditions and the following disclaimer in the documentation +and/or other materials provided with the distribution. +* Neither the names of the Copyright Owners nor the names of any contributors +may be used to endorse or promote products derived from this software +without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY +EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY +DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON +ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +Note: + +The following files contain code whose copyright does not belong to the +Copyright Owners. However, separate copyright notices in these files give +express permission to copy, use, modify, sell, or distribute the code. Please +see the copyright notices in the individual files for details. + +<pre> +src/include/fdstream.h +src/include/hash_map.h +src/include/hash_fun.h +src/include/hash_set.h +src/include/hash_table.h +src/sat/minisat_varorder.h +src/sat/minisat_solver.cpp +src/sat/minisat_heap.h +src/sat/minisat_types.h +src/sat/minisat_solver.h +src/sat/minisat_global.h +</pre> + +*/ diff --git a/lib/SMT/Makefile b/lib/SMT/Makefile new file mode 100644 index 00000000..ae9c2e18 --- /dev/null +++ b/lib/SMT/Makefile @@ -0,0 +1,59 @@ +MODULE = parser + +LIBRARY=libparser.a + +# Do not optimize the parser code - it compiles forever in some gcc versions +EXTRAFLAGS = -O0 + +TRANSIENT_CPP = \ + parsePL.cpp lexPL.cpp \ + parseLisp.cpp lexLisp.cpp \ + parsesmtlib.cpp lexsmtlib.cpp + +TRANSIENT = $(TRANSIENT_CPP) \ + parsePL_defs.h parsePL.output \ + parseLisp_defs.h parseLisp.output \ + parsesmtlib_defs.h parsesmtlib.output + +SRC = $(TRANSIENT_CPP) parser.cpp + +HEADERS = parser_temp.h + +# The actual source files for the parser that we want to include in a +# distribution +SRC_ORIG = PL.lex PL.y Lisp.lex Lisp.y smtlib.lex smtlib.y parser.cpp + +include ../../Makefile.local + +################################################## +# Rules for transient files +################################################## +lexPL.cpp: PL.lex parsePL_defs.h + $(LEX) $(LFLAGS) -I -PPL -olexPL.cpp PL.lex + +parsePL_defs.h: parsePL.cpp + +parsePL.cpp: PL.y + $(YACC) $(YFLAGS) -o parsePL.cpp -p PL --debug -v PL.y + @if [ -f parsePL.cpp.h ]; then mv parsePL.cpp.h parsePL.hpp; fi + @mv parsePL.hpp parsePL_defs.h + +lexLisp.cpp: Lisp.lex parseLisp_defs.h + $(LEX) $(LFLAGS) -I -PLisp -olexLisp.cpp Lisp.lex + +parseLisp_defs.h: parseLisp.cpp + +parseLisp.cpp: Lisp.y + $(YACC) $(YFLAGS) -o parseLisp.cpp -p Lisp --debug -v Lisp.y + @if [ -f parseLisp.cpp.h ]; then mv parseLisp.cpp.h parseLisp.hpp; fi + @mv parseLisp.hpp parseLisp_defs.h + +lexsmtlib.cpp: smtlib.lex parsesmtlib_defs.h + $(LEX) $(LFLAGS) -I -Psmtlib -olexsmtlib.cpp smtlib.lex + +parsesmtlib_defs.h: parsesmtlib.cpp + +parsesmtlib.cpp: smtlib.y + $(YACC) $(YFLAGS) -o parsesmtlib.cpp -p smtlib --debug -v smtlib.y + @if [ -f parsesmtlib.cpp.h ]; then mv parsesmtlib.cpp.h parsesmtlib.hpp; fi + @mv parsesmtlib.hpp parsesmtlib_defs.h diff --git a/lib/SMT/exception.h b/lib/SMT/exception.h new file mode 100644 index 00000000..97f79669 --- /dev/null +++ b/lib/SMT/exception.h @@ -0,0 +1,58 @@ +/*****************************************************************************/ +/*! + * \file exception.h + * + * Author: Sergey Berezin + * + * Created: Thu Feb 6 13:09:44 2003 + * + * <hr> + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + * <hr> + * + * A generic exception. Any thrown exception must inherit from this + * class and whenever possible, set the error message. + */ +/*****************************************************************************/ + +#ifndef _cvc3__exception_h_ +#define _cvc3__exception_h_ + +#include <string> +#include <iostream> + +namespace CVC3 { + + class Exception { + protected: + std::string d_msg; + public: + // Constructors + Exception(): d_msg("Unknown exception") { } + Exception(const std::string& msg): d_msg(msg) { } + Exception(const char* msg): d_msg(msg) { } + // Destructor + virtual ~Exception() { } + // NON-VIRTUAL METHODs for setting and printing the error message + void setMessage(const std::string& msg) { d_msg = msg; } + // Printing: feel free to redefine toString(). When inherited, + // it's recommended that this method print the type of exception + // before the actual message. + virtual std::string toString() const { return d_msg; } + // No need to overload operator<< for the inherited classes + friend std::ostream& operator<<(std::ostream& os, const Exception& e); + + }; // end of class Exception + + inline std::ostream& operator<<(std::ostream& os, const Exception& e) { + return os << e.toString(); + } + +} // end of namespace CVC3 + +#endif diff --git a/lib/SMT/lang.h b/lib/SMT/lang.h new file mode 100644 index 00000000..c021e63a --- /dev/null +++ b/lib/SMT/lang.h @@ -0,0 +1,66 @@ +/*****************************************************************************/ +/*! + * \file lang.h + * \brief Definition of input and output languages to CVC3 + * + * Author: Mehul Trivedi + * + * Created: Thu Jul 29 11:56:34 2004 + * + * <hr> + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + * <hr> + * + */ +/*****************************************************************************/ + +#ifndef _cvc3__lang_h_ +#define _cvc3__lang_h_ + +#include "debug.h" + +namespace CVC3 { + + //! Different input languages + typedef enum { + //! Nice SAL-like language for manually written specs + PRESENTATION_LANG, + //! SMT-LIB format + SMTLIB_LANG, + //! Lisp-like format for automatically generated specs + LISP_LANG, + AST_LANG, + + /* @brief AST is only for printing the Expr abstract syntax tree in lisp + format; there is no such input language <em>per se</em> */ + SIMPLIFY_LANG, + //! for output into Simplify format + TPTP_LANG + //! for output in TPTP format + } InputLanguage; + + inline InputLanguage getLanguage(const std::string& lang) { + if (lang.size() > 0) { + if(lang[0] == 'p') return PRESENTATION_LANG; + if(lang[0] == 'l') return LISP_LANG; + if(lang[0] == 'a') return AST_LANG; + if(lang[0] == 't') return TPTP_LANG; + if(lang[0] == 's') { + if (lang.size() > 1 && lang[1] == 'i') return SIMPLIFY_LANG; + else return SMTLIB_LANG; + } + + } + + throw Exception("Bad input language specified"); + return AST_LANG; + } + +} // end of namespace CVC3 + +#endif diff --git a/lib/SMT/parser.cpp b/lib/SMT/parser.cpp new file mode 100644 index 00000000..92693c35 --- /dev/null +++ b/lib/SMT/parser.cpp @@ -0,0 +1,235 @@ +/*****************************************************************************/ +/*! + * \file parser.cpp + * \brief The top-level API to the parser. See parser.h for details. + * + * Author: Sergey Berezin + * + * Created: Wed Feb 5 11:46:57 2003 + * + * <hr> + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + * <hr> + * + */ +/*****************************************************************************/ + +#include <fstream> +#include <iomanip> +#include "parser_temp.h" +#include "parser.h" +#include "parser_exception.h" + +using namespace std; + +// 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 Lisp language (Lisp.y and Lisp.lex) +extern int Lispparse(); +extern void *Lisp_createBuffer(int); +extern void Lisp_deleteBuffer(void *); +extern void Lisp_switchToBuffer(void *); +extern int Lisp_bufSize(); +extern void *LispBufState(); +void Lisp_setInteractive(bool); + +// for Lisp language (Lisp.y and Lisp.lex) +extern int Lispparse(); +extern void *Lisp_createBuffer(int); +extern void Lisp_deleteBuffer(void *); +extern void Lisp_switchToBuffer(void *); +extern int Lisp_bufSize(); +extern void *LispBufState(); +void Lisp_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); + +namespace CVC3 { + + // 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. + + // FIXME: This should probably go away eventually, when I figure out + // flex++ -- Sergey. + ParserTemp* parserTemp; + + int ParserTemp::error(const string& s) { + throw ParserException(s); + return 0; + } + + // Internal storage class; I'll use member names without 'd_'s here + class ParserData { + public: + // Which language to use + InputLanguage lang; + // Is the input given by the file name or as istream? + bool useName; + ParserTemp temp; + // Internal buffer used by the parser + void* buffer; + }; + + // Constructors + Parser::Parser(ValidityChecker* vc, InputLanguage lang, + bool interactive, + const std::string& fileName) + : d_data(new ParserData) { + d_data->temp.vc = vc; + d_data->lang = lang; + if(fileName == "") { + // Use std::cin + d_data->useName = false; + d_data->temp.is = &cin; + d_data->temp.fileName = "stdin"; + d_data->temp.interactive = interactive; + } else { + // Open the file by name + d_data->useName = true; + d_data->temp.fileName = fileName; + d_data->temp.is = new ifstream(fileName.c_str()); + if (!(*d_data->temp.is)) { + throw ParserException("File not found: "+fileName); + } + d_data->temp.interactive = false; + } + initParser(); + } + + Parser::Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is, + bool interactive) + : d_data(new ParserData) { + d_data->temp.vc = vc; + d_data->lang = lang; + d_data->useName = false; + d_data->temp.is = &is; + d_data->temp.fileName = "stdin"; + d_data->temp.interactive = interactive; + initParser(); + } + + // Destructor + Parser::~Parser() { + if(d_data->useName) // Stream is ours; delete it + delete d_data->temp.is; + deleteParser(); + delete d_data; + } + + // Initialize the actual parser + void Parser::initParser() { + switch(d_data->lang) { + case PRESENTATION_LANG: + d_data->buffer = PL_createBuffer(PL_bufSize()); + d_data->temp.lineNum = 1; + break; + case LISP_LANG: + d_data->buffer = Lisp_createBuffer(Lisp_bufSize()); + d_data->temp.lineNum = 1; + break; + case SMTLIB_LANG: + d_data->buffer = smtlib_createBuffer(smtlib_bufSize()); + d_data->temp.lineNum = 1; + break; + default: FatalAssert(false, "Bad input language specified"); exit(1); + } + } + + // Clean up the parser's internal data structures + void Parser::deleteParser() { + switch(d_data->lang) { + case PRESENTATION_LANG: + PL_deleteBuffer(d_data->buffer); + break; + case LISP_LANG: + Lisp_deleteBuffer(d_data->buffer); + break; + case SMTLIB_LANG: + smtlib_deleteBuffer(d_data->buffer); + break; + default: FatalAssert(false, "Bad input language specified"); + } + } + + + Expr Parser::next() { + // If no more commands are available, return a Null Expr + if(d_data->temp.done) return Expr(); + // Set the global var so the parser uses the right stream and EM + parserTemp = &(d_data->temp); + // Switch to our buffer, in case there are multiple instances of + // the parser running + try { + switch(d_data->lang) { + case PRESENTATION_LANG: + PL_switchToBuffer(d_data->buffer); + PL_setInteractive(d_data->temp.interactive); + PLparse(); + // Reset the prompt to the main one + d_data->temp.setPrompt1(); + break; + case LISP_LANG: + Lisp_switchToBuffer(d_data->buffer); + Lisp_setInteractive(d_data->temp.interactive); + Lispparse(); + // Reset the prompt to the main one + d_data->temp.setPrompt1(); + break; + case SMTLIB_LANG: + smtlib_switchToBuffer(d_data->buffer); + smtlib_setInteractive(d_data->temp.interactive); + smtlibparse(); + // Reset the prompt to the main one + d_data->temp.setPrompt1(); + break; + default: { + ostringstream ss; + ss << "Bad input language specified: " << d_data->lang; + DebugAssert(false, ss.str().c_str()); exit(1); + } + } + } catch(Exception* e) { + cerr << d_data->temp.fileName << ":" << d_data->temp.lineNum + << ": " << e << endl; + return Expr(); + } + return d_data->temp.expr; + } + + bool Parser::done() const { return d_data->temp.done; } + + void Parser::printLocation(ostream & out) const + { + out << d_data->temp.fileName << ":" << d_data->temp.lineNum; + } + + void Parser::reset() + { + d_data->temp.expr = Expr(); + } + + +} // end of namespace CVC3 diff --git a/lib/SMT/parser.h b/lib/SMT/parser.h new file mode 100644 index 00000000..2e580a31 --- /dev/null +++ b/lib/SMT/parser.h @@ -0,0 +1,79 @@ +/*****************************************************************************/ +/*! + * \file parser.h + * + * Author: Sergey Berezin + * + * Created: Wed Feb 5 11:46:57 2003 + * + * <hr> + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + * <hr> + * + * The top-level API to the parser. At this level, it is simply a + * stream of commands (Expr's) terminated by an infinite sequence of + * Null Expr. It has a support to parse several different input + * languages (as many as we care to implement), and may take a file + * name, or an istream to read from (default: std::cin, or stdin). + * Using iostream means no more worries about whether to close files + * or not. + */ +/*****************************************************************************/ + +#ifndef _cvc3__parser_h_ +#define _cvc3__parser_h_ + +#include "exception.h" +#include "lang.h" + +namespace CVC3 { + + class ValidityChecker; + class Expr; + + // Internal parser state and other data + class ParserData; + + class Parser { + private: + ParserData* d_data; + // Internal methods for constructing and destroying the actual parser + void initParser(); + void deleteParser(); + public: + // Constructors + Parser(ValidityChecker* vc, InputLanguage lang, + // The 'interactive' flag is ignored when fileName != "" + bool interactive = true, + const std::string& fileName = ""); + Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is, + bool interactive = false); + // Destructor + ~Parser(); + // Read the next command. + Expr next(); + // 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(); } + void printLocation(std::ostream & out) const; + // Reset any local data that depends on validity checker + 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. + class ParserTemp; + extern ParserTemp* parserTemp; + +} // end of namespace CVC3 + +#endif diff --git a/lib/SMT/parser_exception.h b/lib/SMT/parser_exception.h new file mode 100644 index 00000000..64a8f452 --- /dev/null +++ b/lib/SMT/parser_exception.h @@ -0,0 +1,46 @@ +/*****************************************************************************/ +/*! + * \file parser_exception.h + * \brief An exception thrown by the parser. + * + * Author: Sergey Berezin + * + * Created: Thu Feb 6 13:23:39 2003 + * + * <hr> + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + * <hr> + * + */ +/*****************************************************************************/ + +#ifndef _cvc3__parser_exception_h_ +#define _cvc3__parser_exception_h_ + +#include "exception.h" +#include <string> +#include <iostream> + +namespace CVC3 { + + class ParserException: public Exception { + public: + // Constructors + ParserException() { } + ParserException(const std::string& msg): Exception(msg) { } + ParserException(const char* msg): Exception(msg) { } + // Destructor + virtual ~ParserException() { } + virtual std::string toString() const { + return "Parse Error: " + d_msg; + } + }; // end of class ParserException + +} // end of namespace CVC3 + +#endif diff --git a/lib/SMT/parser_temp.h b/lib/SMT/parser_temp.h new file mode 100644 index 00000000..2c6f6b38 --- /dev/null +++ b/lib/SMT/parser_temp.h @@ -0,0 +1,85 @@ +/*****************************************************************************/ +/*! + * \file parser_temp.h + * + * Author: Sergey Berezin + * + * Created: Wed Feb 5 17:53:02 2003 + * + * <hr> + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + * <hr> + * + * A class used to communicate with the actual parser. No one else + * should use it. + */ +/*****************************************************************************/ + +#ifndef _cvc3__parser_temp_h_ +#define _cvc3__parser_temp_h_ + +#include "expr.h" +#include "exception.h" + +namespace CVC3 { + + class ValidityChecker; + + class ParserTemp { + 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: + ValidityChecker* vc; + std::istream* is; + // The current input line + int lineNum; + // File name + std::string fileName; + // The last parsed Expr + 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 + ParserTemp() : d_uid(0), prompt1("CVC> "), prompt2("- "), + prompt("CVC> "), lineNum(1), done(false), arrFlag(false), queryParsed(false) { } + // Parser error handling (implemented in parser.cpp) + int error(const std::string& s); + // Get the next uniqueID as a string + std::string uniqueID() { + std::ostringstream ss; + ss << d_uid++; + return ss.str(); + } + // Get the current prompt + std::string getPrompt() { return prompt; } + // Set the prompt to the main one + void setPrompt1() { prompt = prompt1; } + // Set the prompt to the secondary one + void setPrompt2() { prompt = prompt2; } + }; + +} // end of namespace CVC3 + +#endif diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex new file mode 100644 index 00000000..15c06fc5 --- /dev/null +++ b/lib/SMT/smtlib.lex @@ -0,0 +1,224 @@ +%{ +/*****************************************************************************/ +/*! + * \file smtlib.lex + * + * Author: Clark Barrett + * + * Created: 2005 + * + * <hr> + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + * <hr> + * + */ +/*****************************************************************************/ + +#include <iostream> +#include "parser_temp.h" +#include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */ +#include "parsesmtlib_defs.h" +#include "debug.h" + +namespace CVC3 { + extern ParserTemp* parserTemp; +} + +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(CVC3::parserTemp->interactive) { + // Print the current prompt + std::cout << CVC3::parserTemp->getPrompt() << std::flush; + // Set the prompt to "middle of the command" one + CVC3::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; res<size && buf[res] != 0; res++); + if(res == size) smtliberror("Lexer bug: overfilled the buffer"); + if(!partialStr) { // Insert \n into the buffer + buf[res++] = '\n'; + buf[res] = '\0'; + } + } else { + res = YY_NULL; + } + return res; +} + +// Redefine the input buffer function to read from an istream +#define YY_INPUT(buf,result,max_size) \ + result = smtlibinput(*CVC3::parserTemp->is, buf, max_size); + +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 CVC3::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; + + 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 (['!#?\_$&\|\\@])*/ + +%} + +%option noyywrap +%option nounput +%option noreject +%option noyymore +%option yylineno + +%x COMMENT +%x STRING_LITERAL +%x USER_VALUE +%s PAT_MODE + +LETTER ([a-zA-Z]) +DIGIT ([0-9]) +OPCHAR (['\.\_]) +IDCHAR ({LETTER}|{DIGIT}|{OPCHAR}) +%% + +[\n] { CVC3::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; } +<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */ + CVC3::parserTemp->lineNum++; } +<COMMENT>. { /* stay in comment mode */ } + +<INITIAL>"\"" { BEGIN STRING_LITERAL; + _string_lit.erase(_string_lit.begin(), + _string_lit.end()); } +<STRING_LITERAL>"\\". { /* escape characters (like \n or \") */ + _string_lit.insert(_string_lit.end(), + escapeChar(smtlibtext[1])); } +<STRING_LITERAL>"\"" { BEGIN INITIAL; /* return to normal mode */ + smtliblval.str = new std::string(_string_lit); + return STRING_TOK; } +<STRING_LITERAL>. { _string_lit.insert(_string_lit.end(),*smtlibtext); } + +<INITIAL>":pat" { BEGIN PAT_MODE; + return PAT_TOK;} +<PAT_MODE>"}" { BEGIN INITIAL; + return RCURBRACK_TOK; } +<INITIAL>"{" { BEGIN USER_VALUE; + _string_lit.erase(_string_lit.begin(), + _string_lit.end()); } +<USER_VALUE>"\\"[{}] { /* escape characters */ + _string_lit.insert(_string_lit.end(),smtlibtext[1]); } + +<USER_VALUE>"}" { BEGIN INITIAL; /* return to normal mode */ + smtliblval.str = new std::string(_string_lit); + return USER_VAL_TOK; } + +<USER_VALUE>"\n" { _string_lit.insert(_string_lit.end(),'\n'); + CVC3::parserTemp->lineNum++; } +<USER_VALUE>. { _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; } +"sorts" { return SORTS_TOK; } +"funs" { return FUNS_TOK; } +"preds" { return PREDS_TOK; } +"extensions" { return EXTENSIONS_TOK; } +"definition" { return DEFINITION_TOK; } +"axioms" { return AXIOMS_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; } +"language" { return LANGUAGE_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; } + +<<EOF>> { return EOF_TOK; } + +. { smtliberror("Illegal input character."); } +%% + diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y new file mode 100644 index 00000000..c9e7b990 --- /dev/null +++ b/lib/SMT/smtlib.y @@ -0,0 +1,1222 @@ +%{ +/*****************************************************************************/ +/*! + * \file smtlib.y + * + * Author: Clark Barrett + * + * Created: Apr 30 2005 + * + * <hr> + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + * <hr> + * + */ +/*****************************************************************************/ +/* + This file contains the bison code for the parser that reads in CVC + commands in SMT-LIB language. +*/ + +#include "vc.h" +#include "parser_exception.h" +#include "parser_temp.h" + +// Exported shared data +namespace CVC3 { + extern ParserTemp* parserTemp; +} +// Define shortcuts for various things +#define TMP CVC3::parserTemp +#define EXPR CVC3::parserTemp->expr +#define VC (CVC3::parserTemp->vc) +#define ARRAYSENABLED (CVC3::parserTemp->arrFlag) +#define BVENABLED (CVC3::parserTemp->bvFlag) +#define BVSIZE (CVC3::parserTemp->bvSize) +#define RAT(args) CVC3::newRational args +#define QUERYPARSED CVC3::parserTemp->queryParsed + +// Suppress the bogus warning suppression in bison (it generates +// compile error) +#undef __GNUC_MINOR__ + +/* stuff that lives in smtlib.lex */ +extern int smtliblex(void); + +int smtliberror(const char *s) +{ + std::ostringstream ss; + ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum + << ": " << s; + return CVC3::parserTemp->error(ss.str()); +} + + + +#define YYLTYPE_IS_TRIVIAL 1 +#define YYMAXDEPTH 10485760 + +%} + +%union { + std::string *str; + std::vector<std::string> *strvec; + CVC3::Expr *node; + std::vector<CVC3::Expr> *vec; + std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann; +}; + + +%start cmd + +/* strings are for better error messages. + "_TOK" is so macros don't conflict with kind names */ + +%type <vec> bench_attributes sort_symbs fun_symb_decls pred_symb_decls +%type <vec> an_formulas quant_vars an_terms fun_symb patterns +%type <node> pattern +%type <node> benchmark bench_name bench_attribute +%type <node> status fun_symb_decl fun_sig pred_symb_decl pred_sig +%type <node> an_formula quant_var an_atom prop_atom +%type <node> an_term basic_term sort_symb pred_symb +%type <node> var fvar +%type <str> logic_name quant_symb connective user_value attribute annotation +%type <strvec> annotations +%type <pat_ann> patterns_annotations + +%token <str> NUMERAL_TOK +%token <str> SYM_TOK +%token <str> STRING_TOK +%token <str> AR_SYMB +%token <str> USER_VAL_TOK +%token TRUE_TOK +%token FALSE_TOK +%token ITE_TOK +%token NOT_TOK +%token IMPLIES_TOK +%token IF_THEN_ELSE_TOK +%token AND_TOK +%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 SORTS_TOK +%token FUNS_TOK +%token PREDS_TOK +%token EXTENSIONS_TOK +%token DEFINITION_TOK +%token AXIOMS_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 +%token ASSUMPTION_TOK +%token FORMULA_TOK +%token STATUS_TOK +%token BENCHMARK_TOK +%token EXTRASORTS_TOK +%token EXTRAFUNS_TOK +%token EXTRAPREDS_TOK +%token LANGUAGE_TOK +%token DOLLAR_TOK +%token QUESTION_TOK +%token DISTINCT_TOK +%token SEMICOLON_TOK +%token EOF_TOK +%token PAT_TOK +%% + +cmd: + benchmark + { + EXPR = *$1; + delete $1; + YYACCEPT; + } +; + +benchmark: + LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK + { + if (!QUERYPARSED) + $4->push_back(CVC3::Expr(VC->listExpr("_CHECKSAT", CVC3::Expr(VC->idExpr("_TRUE_EXPR"))))); + $$ = new CVC3::Expr(VC->listExpr("_SEQ",*$4)); + delete $4; + } + | EOF_TOK + { + TMP->done = true; + $$ = new CVC3::Expr(); + } +; + +bench_name: + SYM_TOK + { + $$ = NULL; + delete $1; + } +; + +bench_attributes: + bench_attribute + { + $$ = new std::vector<CVC3::Expr>; + 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 CVC3::Expr(VC->listExpr("_ASSERT", *$3)); + delete $3; + } + | COLON_TOK FORMULA_TOK an_formula + { + $$ = new CVC3::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; + if (*$3 == "QF_UF") { + $$ = new CVC3::Expr(VC->listExpr("_TYPE", VC->idExpr("U"))); + } + else if (*$3 == "QF_A" || + *$3 == "QF_AX") { + ARRAYSENABLED = true; + std::vector<CVC3::Expr> 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")))); + $$ = new CVC3::Expr(VC->listExpr("_SEQ", tmp)); + } + else if (*$3 == "QF_AUFLIA" || + *$3 == "AUFLIA") { + ARRAYSENABLED = true; + std::vector<CVC3::Expr> tmp; + tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array"), + VC->listExpr("_ARRAY", + VC->idExpr("_INT"), + VC->idExpr("_INT")))); + $$ = new CVC3::Expr(VC->listExpr("_SEQ", tmp)); + } + else if (*$3 == "QF_AUFLIRA" || + *$3 == "AUFLIRA" || + *$3 == "QF_AUFNIRA" || + *$3 == "AUFNIRA") { + ARRAYSENABLED = true; + std::vector<CVC3::Expr> 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")))); + $$ = new CVC3::Expr(VC->listExpr("_SEQ", tmp)); + } + else if (*$3 == "QF_AUFBV" || + *$3 == "QF_ABV") { + ARRAYSENABLED = true; + BVENABLED = true; + $$ = NULL; +// $$ = new CVC3::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; + $$ = NULL; + } + // This enables the new arith for QF_LRA, but this results in assertion failures in DEBUG mode + else if (*$3 == "QF_LRA") { + $$ = new CVC3::Expr(VC->listExpr("_OPTION", VC->stringExpr("arith-new"), VC->ratExpr(1))); + } + else { + $$ = NULL; + } + delete $3; + } + | COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symbs RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_TYPE", *$4)); + delete $4; + } + | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK fun_symb_decls RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4)); + delete $4; + } + | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4)); + delete $4; + } + | COLON_TOK NOTES_TOK STRING_TOK + { + $$ = NULL; + delete $3; + } + | COLON_TOK CVC_COMMAND_TOK STRING_TOK + { + $$ = new CVC3::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<CVC3::Expr>; + $$->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<CVC3::Expr>; + $$->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; + } +; + +fun_sig: + fun_symb sort_symbs + { + if ($2->size() == 1) { + $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), (*$2)[0])); + } + else { + CVC3::Expr tmp(VC->listExpr("_ARROW", *$2)); + $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp)); + } + delete $1; + delete $2; + } +; + +pred_symb_decls: + pred_symb_decl + { + $$ = new std::vector<CVC3::Expr>; + $$->push_back(*$1); + delete $1; + } + | + pred_symb_decls pred_symb_decl + { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +; + +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<CVC3::Expr> tmp(*$2); + tmp.push_back(VC->idExpr("_BOOLEAN")); + CVC3::Expr tmp2(VC->listExpr("_ARROW", tmp)); + $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp2)); + delete $1; + delete $2; + } + | pred_symb + { + $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), + VC->idExpr("_BOOLEAN"))); + delete $1; + } +; + +an_formulas: + an_formula + { + $$ = new std::vector<CVC3::Expr>; + $$->push_back(*$1); + delete $1; + } + | + an_formulas an_formula + { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +; + +an_formula: + an_atom + { + $$ = $1; + } + | LPAREN_TOK connective an_formulas annotations RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$2, *$3)); + delete $2; + delete $3; + delete $4; + } + | LPAREN_TOK connective an_formulas RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$2, *$3)); + delete $2; + delete $3; + } + | LPAREN_TOK quant_symb quant_vars an_formula annotations RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4)); + delete $2; + delete $3; + delete $4; + delete $5; + } + | LPAREN_TOK quant_symb quant_vars an_formula RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4)); + delete $2; + delete $3; + delete $4; + } + | LPAREN_TOK quant_symb quant_vars an_formula patterns_annotations RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4, VC->listExpr((*$5).first))); + delete $2; + delete $3; + delete $4; + delete $5; + } + | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula annotations RPAREN_TOK + { + CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); + $$ = new CVC3::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 + { + CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); + $$ = new CVC3::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 + { + CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); + $$ = new CVC3::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 + { + CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); + $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7)); + delete $4; + delete $5; + delete $7; + } +; + +patterns_annotations: + patterns + { + $$ = new std::pair<std::vector<CVC3::Expr>, std::vector<std::string> >; + $$->first = *$1; + delete $1; + } + | annotation + { + $$ = new std::pair<std::vector<CVC3::Expr>, std::vector<std::string> >; + $$->second.push_back(*$1); + delete $1; + } + | patterns_annotations patterns + { + $1->first.insert($1->first.end(), $2->begin(), $2->end()); + $$ = $1; + delete $2; + } + | patterns_annotations annotation + { + $1->second.push_back(*$2); + $$ = $1; + delete $2; + } + +patterns: + pattern + { + $$ = new std::vector<CVC3::Expr >; + $$->push_back(*$1); + delete $1; + } + | patterns pattern + { + $1->push_back(*$2); + $$ = $1; + delete $2; + } + +pattern: + PAT_TOK LCURBRACK_TOK an_terms RCURBRACK_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$3)); + delete $3; + } + | PAT_TOK LCURBRACK_TOK an_formulas RCURBRACK_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$3)); + delete $3; + } + + + +quant_vars: + quant_var + { + $$ = new std::vector<CVC3::Expr>; + $$->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 CVC3::Expr(VC->listExpr(*$2, *$3)); + delete $2; + delete $3; + } +; + +quant_symb: + EXISTS_TOK + { + $$ = new std::string("_EXISTS"); + } + | FORALL_TOK + { + $$ = new std::string("_FORALL"); + } +; + +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"); + } +; + +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 CVC3::Expr(VC->listExpr("_TRANS_CLOSURE", + *$2, (*$3)[0], (*$3)[1])); + } + else { + std::vector<CVC3::Expr> tmp; + tmp.push_back(*$2); + tmp.insert(tmp.end(), $3->begin(), $3->end()); + $$ = new CVC3::Expr(VC->listExpr(tmp)); + } + delete $2; + delete $3; + delete $4; + } + | LPAREN_TOK pred_symb an_terms RPAREN_TOK + { + std::vector<CVC3::Expr> tmp; + tmp.push_back(*$2); + tmp.insert(tmp.end(), $3->begin(), $3->end()); + $$ = new CVC3::Expr(VC->listExpr(tmp)); + delete $2; + delete $3; + } + | LPAREN_TOK DISTINCT_TOK an_terms annotations RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3)); + +// std::vector<CVC3::Expr> tmp; +// tmp.push_back(*$2); +// tmp.insert(tmp.end(), $3->begin(), $3->end()); +// $$ = new CVC3::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 CVC3::Expr(VC->listExpr("_AND", tmp)); + delete $3; + delete $4; + } + | LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3)); +// std::vector<CVC3::Expr> 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 CVC3::Expr(VC->listExpr("_AND", tmp)); + delete $3; + } +; + +prop_atom: + TRUE_TOK + { + $$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR")); + } + | FALSE_TOK + { + $$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR")); + } + | fvar + { + $$ = $1; + } + | pred_symb + { + $$ = $1; + } +; + +an_terms: + an_term + { + $$ = new std::vector<CVC3::Expr>; + $$->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 CVC3::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 CVC3::Expr(VC->listExpr(*$2)); + delete $2; + delete $3; + } + | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations RPAREN_TOK + { + $$ = new CVC3::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 CVC3::Expr(VC->listExpr("_IF", *$3, *$4, *$5)); + delete $3; + delete $4; + delete $5; + } +; + +basic_term: + | TRUE_TOK + { + $$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR")); + } + | FALSE_TOK + { + $$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR")); + } + | fvar + { + $$ = $1; + } + | var + { + $$ = $1; + } + | fun_symb + { + if ($1->size() == 1) { + $$ = new CVC3::Expr(((*$1)[0])); + } + else { + $$ = new CVC3::Expr(VC->listExpr(*$1)); + } + delete $1; + } +; + +annotations: + annotation + { + $$ = new std::vector<std::string>; + $$->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 CVC3::Expr(VC->listExpr("_BITVECTOR", VC->ratExpr(*$3))); + } + else { + $$ = new CVC3::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 CVC3::Expr(VC->listExpr("_ARRAY", + VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)), + VC->listExpr("_BITVECTOR", VC->ratExpr(*$5)))); + } + else { + $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3), VC->ratExpr(*$5))); + } + delete $1; + delete $3; + delete $5; + } + | SYM_TOK + { + if (*$1 == "Real") { + $$ = new CVC3::Expr(VC->idExpr("_REAL")); + } else if (*$1 == "Int") { + $$ = new CVC3::Expr(VC->idExpr("_INT")); + } else { + $$ = new CVC3::Expr(VC->idExpr(*$1)); + } + delete $1; + } +; + +pred_symb: + SYM_TOK + { + if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) { + $$ = new CVC3::Expr(VC->idExpr("_BVLT")); + } + else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) { + $$ = new CVC3::Expr(VC->idExpr("_BVLE")); + } + else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) { + $$ = new CVC3::Expr(VC->idExpr("_BVGE")); + } + else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) { + $$ = new CVC3::Expr(VC->idExpr("_BVGT")); + } + else if (BVENABLED && *$1 == "bvslt") { + $$ = new CVC3::Expr(VC->idExpr("_BVSLT")); + } + else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) { + $$ = new CVC3::Expr(VC->idExpr("_BVSLE")); + } + else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) { + $$ = new CVC3::Expr(VC->idExpr("_BVSGE")); + } + else if (BVENABLED && *$1 == "bvsgt") { + $$ = new CVC3::Expr(VC->idExpr("_BVSGT")); + } + else { + $$ = new CVC3::Expr(VC->idExpr(*$1)); + } + delete $1; + } + | AR_SYMB + { + if ($1->length() == 1) { + switch ((*$1)[0]) { + case '=': $$ = new CVC3::Expr(VC->idExpr("_EQ")); break; + case '<': $$ = new CVC3::Expr(VC->idExpr("_LT")); break; + case '>': $$ = new CVC3::Expr(VC->idExpr("_GT")); break; + default: $$ = new CVC3::Expr(VC->idExpr(*$1)); break; + } + } + else { + if (*$1 == "<=") { + $$ = new CVC3::Expr(VC->idExpr("_LE")); + } else if (*$1 == ">=") { + $$ = new CVC3::Expr(VC->idExpr("_GE")); + } + else $$ = new CVC3::Expr(VC->idExpr(*$1)); + } + delete $1; + } +; + +fun_symb: + SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK + { + $$ = new std::vector<CVC3::Expr>; + 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<CVC3::Expr>; + 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<CVC3::Expr>; + 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")); + } + else 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 == "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<CVC3::Expr>; + 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<CVC3::Expr>; + $$->push_back(VC->ratExpr(*$1)); + delete $1; + } +; + +attribute: + COLON_TOK SYM_TOK + { + $$ = $2; + } +; + +var: + QUESTION_TOK SYM_TOK + { + $$ = new CVC3::Expr(VC->idExpr(*$2)); + delete $2; + } +; + +fvar: + DOLLAR_TOK SYM_TOK + { + $$ = new CVC3::Expr(VC->idExpr(*$2)); + delete $2; + } +; + +%% |