From acd68152ff9600bdff208376f2cd43f09d45cdc8 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 17 Nov 2009 07:19:39 +0000 Subject: [PATCH] fixes and additions --- configure.ac | 4 +- contrib/update-copyright.pl | 61 ++++++++++++++++++++ src/Makefile.am | 3 +- src/core/Makefile.am | 7 +++ src/core/expr.cpp | 103 +++++++++++++++++++++++++++++++++ src/core/expr_manager.cpp | 49 ++++++++++++++++ src/core/expr_value.cpp | 61 ++++++++++++++++++++ src/include/debug.h | 24 ++++++++ src/include/exception.h | 2 +- src/include/expr.h | 27 ++++++++- src/include/expr_builder.h | 4 ++ src/include/expr_manager.h | 56 ++++++------------ src/include/expr_value.h | 9 ++- src/include/kind.h | 6 +- src/include/parser_temp.h | 76 ------------------------ src/parser/Makefile.am | 25 ++++++-- src/parser/parser_state.h | 89 ++++++++++++++++++++++++++++ src/parser/pl.ypp | 55 +++++++----------- src/parser/pl_scanner.lpp | 105 +++++++++------------------------- src/parser/smtlib.ypp | 69 +++++++++------------- src/parser/smtlib_scanner.lpp | 93 +++++++----------------------- 21 files changed, 575 insertions(+), 353 deletions(-) create mode 100755 contrib/update-copyright.pl create mode 100644 src/core/Makefile.am create mode 100644 src/core/expr.cpp create mode 100644 src/core/expr_manager.cpp create mode 100644 src/core/expr_value.cpp create mode 100644 src/include/debug.h delete mode 100644 src/include/parser_temp.h create mode 100644 src/parser/parser_state.h diff --git a/configure.ac b/configure.ac index 53fecffb1..87f1458b6 100644 --- a/configure.ac +++ b/configure.ac @@ -8,7 +8,6 @@ AC_CONFIG_AUX_DIR([config]) AC_CONFIG_MACRO_DIR([config]) AM_INIT_AUTOMAKE(cvc4, prerelease) AC_CONFIG_HEADERS([config.h]) -AM_MAINTAINER_MODE LT_INIT AC_LIBTOOL_WIN32_DLL @@ -22,7 +21,7 @@ AM_PROG_LEX AC_PROG_YACC AC_CHECK_PROG(DOXYGEN, doxygen, doxygen,) -if [ "$DOXYGEN" = '' ]; then +if test "$DOXYGEN" = ''; then echo 'WARNING: documentation targets require doxygen. Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.' fi @@ -45,6 +44,7 @@ AC_CONFIG_FILES([ contrib/Makefile doc/Makefile src/Makefile + src/core/Makefile src/parser/Makefile src/sat/Makefile src/sat/minisat/Makefile diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl new file mode 100755 index 000000000..73adba7e8 --- /dev/null +++ b/contrib/update-copyright.pl @@ -0,0 +1,61 @@ +#!/bin/bash + +cd `dirname "$0"`/../src + +cat <) { + next if !m,^ \*\* ,; + } +} +while(<>) { + print; +}' "$FILE" + +done + diff --git a/src/Makefile.am b/src/Makefile.am index 90efb9cab..3f0d0b381 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -1,10 +1,11 @@ INCLUDES = -I@srcdir@/include -SUBDIRS = parser sat +SUBDIRS = core parser sat lib_LTLIBRARIES = libcvc4.la libcvc4_la_LIBADD = \ + core/libcore.a parser/libparser.a sat/minisat/libminisat.a diff --git a/src/core/Makefile.am b/src/core/Makefile.am new file mode 100644 index 000000000..043882f36 --- /dev/null +++ b/src/core/Makefile.am @@ -0,0 +1,7 @@ +INCLUDES = -I@srcdir@/../include + +noinst_LIBRARIES = libcore.a + +libcore_a_SOURCES = \ + expr.cpp \ + expr_value.cpp diff --git a/src/core/expr.cpp b/src/core/expr.cpp new file mode 100644 index 000000000..1af197f27 --- /dev/null +++ b/src/core/expr.cpp @@ -0,0 +1,103 @@ +/********************* -*- C++ -*- */ +/** expr.cpp + ** This file is part of the CVC4 prototype. + ** + ** Reference-counted encapsulation of a pointer to an expression. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#include "expr.h" +#include "expr_value.h" +#include "expr_builder.h" + +namespace CVC4 { + +Expr Expr::s_null(0); + +Expr::Expr(ExprValue* ev) + : d_ev(ev) { + // FIXME: thread-safety + ++d_ev->d_rc; +} + +Expr::Expr(const Expr& e) { + // FIXME: thread-safety + if((d_ev = e.d_ev)) + ++d_ev->d_rc; +} + +Expr::~Expr() { + // FIXME: thread-safety + --d_ev->d_rc; +} + +Expr& Expr::operator=(const Expr& e) { + // FIXME: thread-safety + if(d_ev) + --d_ev->d_rc; + if((d_ev = e.d_ev)) + ++d_ev->d_rc; + return *this; +} + +ExprValue* Expr::operator->() { + return d_ev; +} + +const ExprValue* Expr::operator->() const { + return d_ev; +} + +uint64_t Expr::hash() const { + return d_ev->hash(); +} + +Expr Expr::eqExpr(const Expr& right) const { + return ExprBuilder(*this).eqExpr(right); +} + +Expr Expr::notExpr() const { + return ExprBuilder(*this).notExpr(); +} + +Expr Expr::negate() const { // avoid double-negatives + return ExprBuilder(*this).negate(); +} + +Expr Expr::andExpr(const Expr& right) const { + return ExprBuilder(*this).andExpr(right); +} + +Expr Expr::orExpr(const Expr& right) const { + return ExprBuilder(*this).orExpr(right); +} + +Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const { + return ExprBuilder(*this).iteExpr(thenpart, elsepart); +} + +Expr Expr::iffExpr(const Expr& right) const { + return ExprBuilder(*this).iffExpr(right); +} + +Expr Expr::impExpr(const Expr& right) const { + return ExprBuilder(*this).impExpr(right); +} + +Expr Expr::xorExpr(const Expr& right) const { + return ExprBuilder(*this).xorExpr(right); +} + +Expr Expr::skolemExpr(int i) const { + return ExprBuilder(*this).skolemExpr(i); +} + +Expr Expr::substExpr(const std::vector& oldTerms, + const std::vector& newTerms) const { + return ExprBuilder(*this).substExpr(oldTerms, newTerms); +} + +} /* CVC4 namespace */ diff --git a/src/core/expr_manager.cpp b/src/core/expr_manager.cpp new file mode 100644 index 000000000..93903c3aa --- /dev/null +++ b/src/core/expr_manager.cpp @@ -0,0 +1,49 @@ +/********************* -*- C++ -*- */ +/** expr_manager.cpp + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#include +#include "expr.h" +#include "kind.h" + +namespace CVC4 { + +class ExprManager { + static __thread ExprManager* s_current; + +public: + static ExprManager* currentEM() { return s_current; } + + // general expression-builders + Expr mkExpr(Kind kind); + Expr mkExpr(Kind kind, Expr child1); + Expr mkExpr(Kind kind, Expr child1, Expr child2); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); + // N-ary version + Expr mkExpr(Kind kind, std::vector children); + + // TODO: these use the current EM (but must be renamed) + /* + static Expr mkExpr(Kind kind) + { currentEM()->mkExpr(kind); } + static Expr mkExpr(Kind kind, Expr child1); + { currentEM()->mkExpr(kind, child1); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2); + { currentEM()->mkExpr(kind, child1, child2); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); + { currentEM()->mkExpr(kind, child1, child2, child3); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + { currentEM()->mkExpr(kind, child1, child2, child3, child4); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); + { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); } + */ +}; + +} /* CVC4 namespace */ diff --git a/src/core/expr_value.cpp b/src/core/expr_value.cpp new file mode 100644 index 000000000..b7c65023e --- /dev/null +++ b/src/core/expr_value.cpp @@ -0,0 +1,61 @@ +/********************* +/** expr_value.cpp + ** This file is part of the CVC4 prototype. + ** + ** An expression node. + ** + ** Instances of this class are generally referenced through + ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the + ** reference count on ExprValue instances and + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#include "expr_value.h" + +namespace CVC4 { + +uint64_t ExprValue::hash() const { + uint64_t hash = d_kind; + + for(const_iterator i = begin(); i != end(); ++i) + hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ i->hash(); + + return hash; +} + +ExprValue::iterator ExprValue::begin() { + return d_children; +} + +ExprValue::iterator ExprValue::end() { + return d_children + d_nchildren; +} + +ExprValue::iterator ExprValue::rbegin() { + return d_children + d_nchildren - 1; +} + +ExprValue::iterator ExprValue::rend() { + return d_children - 1; +} + +ExprValue::const_iterator ExprValue::begin() const { + return d_children; +} + +ExprValue::const_iterator ExprValue::end() const { + return d_children + d_nchildren; +} + +ExprValue::const_iterator ExprValue::rbegin() const { + return d_children + d_nchildren - 1; +} + +ExprValue::const_iterator ExprValue::rend() const { + return d_children - 1; +} + +} /* CVC4 namespace */ diff --git a/src/include/debug.h b/src/include/debug.h new file mode 100644 index 000000000..95e705bcb --- /dev/null +++ b/src/include/debug.h @@ -0,0 +1,24 @@ +/********************* -*- C++ -*- */ +/** debug.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_DEBUG_H +#define __CVC4_DEBUG_H + +#include + +#ifdef DEBUG +// the __builtin_expect() helps us if assert is built-in or a macro +# define cvc4assert(x) assert(__builtin_expect((x), 1)) +#else +// TODO: use a compiler annotation when assertions are off ? +// (to improve optimization) +# define cvc4assert(x) +#endif /* DEBUG */ + +#endif /* __CVC4_DEBUG_H */ diff --git a/src/include/exception.h b/src/include/exception.h index 3502fdf0c..ce19b0d68 100644 --- a/src/include/exception.h +++ b/src/include/exception.h @@ -10,7 +10,7 @@ **/ #ifndef __CVC4_EXCEPTION_H -#ifndef __CVC4_EXCEPTION_H +#define __CVC4_EXCEPTION_H #include #include diff --git a/src/include/expr.h b/src/include/expr.h index 5e3559fd7..9ca449ce7 100644 --- a/src/include/expr.h +++ b/src/include/expr.h @@ -12,6 +12,9 @@ #ifndef __CVC4_EXPR_H #define __CVC4_EXPR_H +#include +#include + namespace CVC4 { class ExprValue; @@ -34,19 +37,39 @@ class Expr { * Increments the reference count. */ explicit Expr(ExprValue*); +public: + Expr(const Expr&); + /** Destructor. Decrements the reference count and, if zero, * collects the ExprValue. */ ~Expr(); -public: + Expr& operator=(const Expr&); + /** Access to the encapsulated expression. * @return the encapsulated expression. */ ExprValue* operator->(); - /** Const access to the encapsulated expressoin. + /** Const access to the encapsulated expression. * @return the encapsulated expression [const]. */ const ExprValue* operator->() const; + uint64_t hash() const; + + Expr eqExpr(const Expr& right) const; + Expr notExpr() const; + Expr negate() const; // avoid double-negatives + Expr andExpr(const Expr& right) const; + Expr orExpr(const Expr& right) const; + Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const; + Expr iffExpr(const Expr& right) const; + Expr impExpr(const Expr& right) const; + Expr xorExpr(const Expr& right) const; + Expr skolemExpr(int i) const; + Expr substExpr(const std::vector& oldTerms, + const std::vector& newTerms) const; + + static Expr null() { return s_null; } };/* class Expr */ } /* CVC4 namespace */ diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h index 59503aa4f..342834e37 100644 --- a/src/include/expr_builder.h +++ b/src/include/expr_builder.h @@ -43,6 +43,10 @@ class ExprBuilder { public: + ExprBuilder(); + ExprBuilder(const Expr&); + ExprBuilder(const ExprBuilder&); + // Compound expression constructors ExprBuilder& eqExpr(const Expr& right); ExprBuilder& notExpr(); diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h index 0c265f57f..5dae5b854 100644 --- a/src/include/expr_manager.h +++ b/src/include/expr_manager.h @@ -23,47 +23,29 @@ public: static ExprManager* currentEM() { return s_current; } // general expression-builders - Expr build(Kind kind); - Expr build(Kind kind, Expr child1); - Expr build(Kind kind, Expr child1, Expr child2); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9); - Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10); + Expr mkExpr(Kind kind); + Expr mkExpr(Kind kind, Expr child1); + Expr mkExpr(Kind kind, Expr child1, Expr child2); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); // N-ary version - Expr build(Kind kind, std::vector children); + Expr mkExpr(Kind kind, std::vector children); // TODO: these use the current EM (but must be renamed) /* - static Expr build(Kind kind) - { currentEM()->build(kind); } - static Expr build(Kind kind, Expr child1); - { currentEM()->build(kind, child1); } - static Expr build(Kind kind, Expr child1, Expr child2); - { currentEM()->build(kind, child1, child2); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3); - { currentEM()->build(kind, child1, child2, child3); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); - { currentEM()->build(kind, child1, child2, child3, child4); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); - { currentEM()->build(kind, child1, child2, child3, child4, child5); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6); - { currentEM()->build(kind, child1, child2, child3, child4, child5, child6); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7); - { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8); - { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9); - { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9); } - static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10); - { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9, child10); } - // N-ary version - static Expr build(Kind kind, vector children) - { currentEM()->build(kind, children); } + static Expr mkExpr(Kind kind) + { currentEM()->mkExpr(kind); } + static Expr mkExpr(Kind kind, Expr child1); + { currentEM()->mkExpr(kind, child1); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2); + { currentEM()->mkExpr(kind, child1, child2); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); + { currentEM()->mkExpr(kind, child1, child2, child3); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + { currentEM()->mkExpr(kind, child1, child2, child3, child4); } + static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); + { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); } */ // do we want a varargs one? perhaps not.. diff --git a/src/include/expr_value.h b/src/include/expr_value.h index ca12b8e03..c15241ebf 100644 --- a/src/include/expr_value.h +++ b/src/include/expr_value.h @@ -16,6 +16,7 @@ #ifndef __CVC4_EXPR_VALUE_H #define __CVC4_EXPR_VALUE_H +#include #include "expr.h" namespace CVC4 { @@ -41,14 +42,12 @@ class ExprValue { /** Variable number of child nodes */ Expr d_children[0]; + friend class Expr; + public: /** Hash this expression. * @return the hash value of this expression. */ - unsigned hash() const; - - /** Convert to (wrap in) an Expr. - * @return an Expr pointing to this expression. */ - operator Expr(); + uint64_t hash() const; // Iterator support diff --git a/src/include/kind.h b/src/include/kind.h index 9307cc677..a015a6b71 100644 --- a/src/include/kind.h +++ b/src/include/kind.h @@ -22,7 +22,11 @@ enum Kind { XOR, NOT, PLUS, - MINUS + MINUS, + ITE, + IFF, + SKOLEM, + SUBST };/* enum Kind */ }/* CVC4 namespace */ diff --git a/src/include/parser_temp.h b/src/include/parser_temp.h deleted file mode 100644 index d64a770e4..000000000 --- a/src/include/parser_temp.h +++ /dev/null @@ -1,76 +0,0 @@ -/********************* -*- C++ -*- */ -/** parser_temp.h - ** This file is part of the CVC4 prototype. - ** - ** A temporary holder for data used with the parser. - ** - ** The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - **/ - -#ifndef __CVC4_PARSER_TEMP_H -#define __CVC4_PARSER_TEMP_H - -#include - -#include "expr.h" -#include "exception.h" - -namespace CVC4 { - - 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; } - }; - -}/* CVC4 namespace */ - -#endif /* __CVC4_PARSER_TEMP_H */ diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 0ebcad8c7..8cf9f4a6d 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -10,9 +10,26 @@ libparser_a_SOURCES = \ parser.cpp BUILT_SOURCES = \ - pl_scanner.lpp \ - pl.ypp \ - smtlib_scanner.lpp \ - smtlib.ypp + pl_scanner.cpp \ + pl.cpp \ + pl.h \ + smtlib_scanner.cpp \ + smtlib.cpp \ + smtlib.h + +# produce headers too +AM_YFLAGS = -d + +pl_scanner.cpp: pl_scanner.lpp + $(LEX) $(AM_LFLAGS) $(LFLAGS) -P PL -o $@ $< +smtlib_scanner.cpp: smtlib_scanner.lpp + $(LEX) $(AM_LFLAGS) $(LFLAGS) -P smtlib -o $@ $< + +pl_scanner.o: pl.h +pl.cpp: pl.ypp + $(YACC) $(AM_YFLAGS) $(YFLAGS) -p PL -o $@ $< +smtlib_scanner.o: smtlib.h +smtlib.cpp: smtlib.ypp + $(YACC) $(AM_YFLAGS) $(YFLAGS) -p smtlib -o $@ $< diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h new file mode 100644 index 000000000..4444925e2 --- /dev/null +++ b/src/parser/parser_state.h @@ -0,0 +1,89 @@ +/********************* -*- C++ -*- */ +/** parser_state.h + ** This file is part of the CVC4 prototype. + ** + ** Extra state of the parser shared by the lexer and parser. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_PARSER_STATE_H +#define __CVC4_PARSER_STATE_H + +#include +#include +#include "expr.h" +#include "exception.h" + +namespace CVC4 { + +class ValidityChecker; + +class ParserState { +private: + // Counter for uniqueID of bound variables + int d_uid; + // The main prompt when running interactive + std::string prompt1; + // The interactive prompt in the middle of a multi-line command + std::string prompt2; + // The currently used prompt + std::string prompt; +public: + 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 + ParserState() : d_uid(0), + prompt1("CVC> "), + prompt2("- "), + prompt("CVC> "), + vc(0), + is(0), + lineNum(1), + fileName(), + expr(Expr::null()), + done(false), + interactive(false), + arrFlag(false), + bvFlag(false), + bvSize(0), + 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; } +}; + +} /* CVC4 namespace */ + +#endif /* __CVC4_PARSER_STATE_H */ diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index dfed55dbb..e9aeab78e 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -1,43 +1,32 @@ +/********************* -*- C++ -*- */ +/** smtlib.ypp + ** This file is part of the CVC4 prototype. + ** + ** Reference-counted encapsulation of a pointer to an expression. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** + ** This file contains the bison code for the parser that reads in CVC + ** commands in the presentation language (hence "PL"). + **/ + %{ -/*****************************************************************************/ -/*! - * \file PL.y - * - * Author: Sergey Berezin - * - * Created: Feb 06 03:00:43 GMT 2003 - * - *
- * - * 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. - * - *
- * - */ -/*****************************************************************************/ -/* PL.y - Aaron Stump, 4/14/01 - - This file contains the bison code for the parser that reads in CVC - commands in the presentation language (hence "PL"). -*/ #include "vc.h" #include "parser_exception.h" -#include "parser_temp.h" -#include "rational.h" +#include "parser_state.h" +//#include "rational.h" // Exported shared data namespace CVC4 { - extern ParserTemp* parserTemp; + extern ParserState* parserState; } // Define shortcuts for various things -#define TMP CVC4::parserTemp -#define EXPR CVC4::parserTemp->expr -#define VC (CVC4::parserTemp->vc) +#define TMP CVC4::parserState +#define EXPR CVC4::parserState->expr +#define VC (CVC4::parserState->vc) #define RAT(args) CVC4::newRational args // Suppress the bogus warning suppression in bison (it generates @@ -50,9 +39,9 @@ extern int PLlex(void); int PLerror(const char *s) { std::ostringstream ss; - ss << CVC4::parserTemp->fileName << ":" << CVC4::parserTemp->lineNum + ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum << ": " << s; - return CVC4::parserTemp->error(ss.str()); + return CVC4::parserState->error(ss.str()); } diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp index d203a1e9a..d70937e34 100644 --- a/src/parser/pl_scanner.lpp +++ b/src/parser/pl_scanner.lpp @@ -1,76 +1,34 @@ +/********************* -*- C++ -*- */ +/** pl_scanner.lpp + ** This file is part of the CVC4 prototype. + ** + ** Reference-counted encapsulation of a pointer to an expression. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +%option interactive +%option noyywrap +%option nounput +%option noreject +%option noyymore +%option yylineno +%option prefix="PL" + %{ -/*****************************************************************************/ -/*! - * \file PL.lex - * - * Author: Sergey Berezin - * - * Created: Feb 06 03:00:43 GMT 2003 - * - *
- * - * 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. - * - *
- * - */ -/*****************************************************************************/ #include -#include "parser_temp.h" #include "expr_manager.h" /* for the benefit of parsePL_defs.h */ -#include "parsePL_defs.h" +#include "parser_state.h" +#include "pl.h" #include "debug.h" namespace CVC4 { - extern ParserTemp* parserTemp; + extern ParserState* parserState; } -/* prefixing hack from gdb (via automake docs) */ -#define yymaxdepth PL_maxdepth -#define yyparse PL_parse -#define yylex PL_lex -#define yyerror PL_error -#define yylval PL_lval -#define yychar PL_char -#define yydebug PL_debug -#define yypact PL_pact -#define yyr1 PL_r1 -#define yyr2 PL_r2 -#define yydef PL_def -#define yychk PL_chk -#define yypgo PL_pgo -#define yyact PL_act -#define yyexca PL_exca -#define yyerrflag PL_errflag -#define yynerrs PL_nerrs -#define yyps PL_ps -#define yypv PL_pv -#define yys PL_s -#define yy_yys PL_yys -#define yystate PL_state -#define yytmp PL_tmp -#define yyv PL_v -#define yy_yyv PL_yyv -#define yyval PL_val -#define yylloc PL_lloc -#define yyreds PL_reds -#define yytoks PL_toks -#define yylhs PL_yylhs -#define yylen PL_yylen -#define yydefred PL_yydefred -#define yydgoto PL_yydgoto -#define yysindex PL_yysindex -#define yyrindex PL_yyrindex -#define yygindex PL_yygindex -#define yytable PL_yytable -#define yycheck PL_yycheck -#define yyname PL_yyname -#define yyrule PL_yyrule - extern int PL_inputLine; extern char *PLtext; @@ -81,11 +39,11 @@ static int PLinput(std::istream& is, char* buf, int size) { if(is) { // If interactive, read line by line; otherwise read as much as we // can gobble - if(CVC4::parserTemp->interactive) { + if(CVC4::parserState->interactive) { // Print the current prompt - std::cout << CVC4::parserTemp->getPrompt() << std::flush; + std::cout << CVC4::parserState->getPrompt() << std::flush; // Set the prompt to "middle of the command" one - CVC4::parserTemp->setPrompt2(); + CVC4::parserState->setPrompt2(); // Read the line is.getline(buf, size-1); } else // Set the terminator char to 0 @@ -110,7 +68,7 @@ static int PLinput(std::istream& is, char* buf, int size) { // Redefine the input buffer function to read from an istream #define YY_INPUT(buf,result,max_size) \ - result = PLinput(*CVC4::parserTemp->is, buf, max_size); + result = PLinput(*CVC4::parserState->is, buf, max_size); int PL_bufSize() { return YY_BUF_SIZE; } YY_BUFFER_STATE PL_buf_state() { return YY_CURRENT_BUFFER; } @@ -152,13 +110,6 @@ static std::string _string_lit; %} -%option interactive -%option noyywrap -%option nounput -%option noreject -%option noyymore -%option yylineno - %x COMMENT %x STRING_LITERAL @@ -171,7 +122,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) %% -[\n] { CVC4::parserTemp->lineNum++; } +[\n] { CVC4::parserState->lineNum++; } [ \t\r\f] { /* skip whitespace */ } @@ -184,7 +135,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) "%" { BEGIN COMMENT; } "\n" { BEGIN INITIAL; /* return to normal mode */ - CVC4::parserTemp->lineNum++; } + CVC4::parserState->lineNum++; } . { /* stay in comment mode */ } "\"" { BEGIN STRING_LITERAL; diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index 1bc22675a..97f61e715 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -1,45 +1,34 @@ -%{ -/*****************************************************************************/ -/*! - * \file smtlib.y - * - * Author: Clark Barrett - * - * Created: Apr 30 2005 - * - *
- * - * 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. - * - *
- * - */ -/*****************************************************************************/ -/* - This file contains the bison code for the parser that reads in CVC - commands in SMT-LIB language. -*/ +%{/******************* -*- C++ -*- */ +/** smtlib.ypp + ** This file is part of the CVC4 prototype. + ** + ** Reference-counted encapsulation of a pointer to an expression. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** + ** 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" +#include "parser_state.h" // Exported shared data -namespace CVC4 { +namespace CVC3 { extern ParserTemp* parserTemp; } // Define shortcuts for various things -#define TMP CVC4::parserTemp -#define EXPR CVC4::parserTemp->expr -#define VC (CVC4::parserTemp->vc) -#define ARRAYSENABLED (CVC4::parserTemp->arrFlag) -#define BVENABLED (CVC4::parserTemp->bvFlag) -#define BVSIZE (CVC4::parserTemp->bvSize) -#define RAT(args) CVC4::newRational args -#define QUERYPARSED CVC4::parserTemp->queryParsed +#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) @@ -51,9 +40,9 @@ extern int smtliblex(void); int smtliberror(const char *s) { std::ostringstream ss; - ss << CVC4::parserTemp->fileName << ":" << CVC4::parserTemp->lineNum + ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum << ": " << s; - return CVC4::parserTemp->error(ss.str()); + return CVC3::parserTemp->error(ss.str()); } @@ -66,9 +55,9 @@ int smtliberror(const char *s) %union { std::string *str; std::vector *strvec; - CVC4::Expr *node; - std::vector *vec; - std::pair, std::vector > *pat_ann; + CVC3::Expr *node; + std::vector *vec; + std::pair, std::vector > *pat_ann; }; @@ -1548,6 +1537,4 @@ fun_pred_symb: } ; - - %% diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp index d5bdaaf26..b78b27a0d 100644 --- a/src/parser/smtlib_scanner.lpp +++ b/src/parser/smtlib_scanner.lpp @@ -1,76 +1,31 @@ -%{ -/*****************************************************************************/ -/*! - * \file smtlib.lex - * - * Author: Clark Barrett - * - * Created: 2005 - * - *
- * - * 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. - * - *
- * - */ -/*****************************************************************************/ +/********************* -*- C++ -*- */ +/** smtlib_scanner.lpp + ** This file is part of the CVC4 prototype. + ** + ** Reference-counted encapsulation of a pointer to an expression. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ +%option interactive +%option noyywrap +%option nounput +%option noreject +%option noyymore +%option yylineno +%option prefix="smtlib" + +%{ #include -#include "parser_temp.h" -#include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */ -#include "parsesmtlib_defs.h" +#include "smtlib.h" #include "debug.h" namespace CVC4 { extern ParserTemp* parserTemp; } -/* prefixing hack from gdb (via automake docs) */ -#define yymaxdepth smtlib_maxdepth -#define yyparse smtlib_parse -#define yylex smtlib_lex -#define yyerror smtlib_error -#define yylval smtlib_lval -#define yychar smtlib_char -#define yydebug smtlib_debug -#define yypact smtlib_pact -#define yyr1 smtlib_r1 -#define yyr2 smtlib_r2 -#define yydef smtlib_def -#define yychk smtlib_chk -#define yypgo smtlib_pgo -#define yyact smtlib_act -#define yyexca smtlib_exca -#define yyerrflag smtlib_errflag -#define yynerrs smtlib_nerrs -#define yyps smtlib_ps -#define yypv smtlib_pv -#define yys smtlib_s -#define yy_yys smtlib_yys -#define yystate smtlib_state -#define yytmp smtlib_tmp -#define yyv smtlib_v -#define yy_yyv smtlib_yyv -#define yyval smtlib_val -#define yylloc smtlib_lloc -#define yyreds smtlib_reds -#define yytoks smtlib_toks -#define yylhs smtlib_yylhs -#define yylen smtlib_yylen -#define yydefred smtlib_yydefred -#define yydgoto smtlib_yydgoto -#define yysindex smtlib_yysindex -#define yyrindex smtlib_yyrindex -#define yygindex smtlib_yygindex -#define yytable smtlib_yytable -#define yycheck smtlib_yycheck -#define yyname smtlib_yyname -#define yyrule smtlib_yyrule - extern int smtlib_inputLine; extern char *smtlibtext; @@ -152,13 +107,6 @@ static std::string _string_lit; %} -%option interactive -%option noyywrap -%option nounput -%option noreject -%option noyymore -%option yylineno - %x COMMENT %x STRING_LITERAL %x USER_VALUE @@ -257,4 +205,3 @@ IDCHAR ({LETTER}|{DIGIT}|{OPCHAR}) . { smtliberror("Illegal input character."); } %% - -- 2.30.2