aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/SMT/LICENSE.CVC353
-rw-r--r--lib/SMT/Makefile59
-rw-r--r--lib/SMT/exception.h58
-rw-r--r--lib/SMT/lang.h66
-rw-r--r--lib/SMT/parser.cpp235
-rw-r--r--lib/SMT/parser.h79
-rw-r--r--lib/SMT/parser_exception.h46
-rw-r--r--lib/SMT/parser_temp.h85
-rw-r--r--lib/SMT/smtlib.lex224
-rw-r--r--lib/SMT/smtlib.y1222
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;
+ }
+;
+
+%%
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-19 19:58:23 +0000