AC_CONFIG_MACRO_DIR([config])
AM_INIT_AUTOMAKE(cvc4, prerelease)
AC_CONFIG_HEADERS([config.h])
-AM_MAINTAINER_MODE
LT_INIT
AC_LIBTOOL_WIN32_DLL
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
contrib/Makefile
doc/Makefile
src/Makefile
+ src/core/Makefile
src/parser/Makefile
src/sat/Makefile
src/sat/minisat/Makefile
--- /dev/null
+#!/bin/bash
+
+cd `dirname "$0"`/../src
+
+cat <<EOF
+Warning: this script is dangerous. It will overwrite the header comments in your
+source files to match the template in the script, attempting to retain file-specific
+comments, but this isn't guaranteed. You should run this in an svn working directory
+and run "svn diff" after to ensure everything was correctly rewritten.
+
+The directory to search for and change sources is:
+ $(pwd)
+
+Continue? y or n:
+EOF
+
+read x
+if [ "$x" != 'y' -a "$x" != 'Y' -a "$x" != 'YES' -a "$x" != 'yes' ]; then
+ echo Aborting operation.
+ exit
+fi
+
+echo Updating sources...
+
+for FILE in $(find . -name '*.cpp' -o -name '*.h' -o -name '*.c' -o -name '*.cc' -o -name '*.hh' -o -name '*.hpp'); do
+echo $FILE
+
+perl -i -e '\
+if(m,^/\*\*\*\*\*,) {
+ print "/********************* -*- C++ -*- */\n";
+ print "/** (basename FILE)\n";
+ print " ** This file is part of the CVC4 prototype.\n";
+ print " ** Copyright (c) (date +%Y) The Analysis of Computer Systems Group (ACSys)\n";
+ print " ** Courant Institute of Mathematical Sciences\n";
+ print " ** New York University\n";
+ print " ** See the file COPYING in the top-level source directory for licensing\n";
+ print " ** information.\n";
+ print " **\n";
+ print " ** [[ Add file-specific comments here ]]\n";
+ print " **/\n\n";
+} else {
+ m,^/\*\* , || exit;
+ print "/********************* -*- C++ -*- */\n";
+ print "/** (basename FILE)\n";
+ print " ** This file is part of the CVC4 prototype.\n";
+ print " ** Copyright (c) $(date +%Y) The Analysis of Computer Systems Group (ACSys)\n";
+ print " ** Courant Institute of Mathematical Sciences\n";
+ print " ** New York University\n";
+ print " ** See the file COPYING in the top-level source directory for licensing\n";
+ print " ** information.\n";
+ print " **\n";
+ while(<>) {
+ next if !m,^ \*\* ,;
+ }
+}
+while(<>) {
+ print;
+}' "$FILE"
+
+done
+
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
--- /dev/null
+INCLUDES = -I@srcdir@/../include
+
+noinst_LIBRARIES = libcore.a
+
+libcore_a_SOURCES = \
+ expr.cpp \
+ expr_value.cpp
--- /dev/null
+/********************* -*- 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<Expr>& oldTerms,
+ const std::vector<Expr>& newTerms) const {
+ return ExprBuilder(*this).substExpr(oldTerms, newTerms);
+}
+
+} /* CVC4 namespace */
--- /dev/null
+/********************* -*- 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 <vector>
+#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<Expr> 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 */
--- /dev/null
+/*********************
+/** 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 */
--- /dev/null
+/********************* -*- 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 <cassert>
+
+#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 */
**/
#ifndef __CVC4_EXCEPTION_H
-#ifndef __CVC4_EXCEPTION_H
+#define __CVC4_EXCEPTION_H
#include <string>
#include <iostream>
#ifndef __CVC4_EXPR_H
#define __CVC4_EXPR_H
+#include <vector>
+#include <stdint.h>
+
namespace CVC4 {
class ExprValue;
* 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<Expr>& oldTerms,
+ const std::vector<Expr>& newTerms) const;
+
+ static Expr null() { return s_null; }
};/* class Expr */
} /* CVC4 namespace */
public:
+ ExprBuilder();
+ ExprBuilder(const Expr&);
+ ExprBuilder(const ExprBuilder&);
+
// Compound expression constructors
ExprBuilder& eqExpr(const Expr& right);
ExprBuilder& notExpr();
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<Expr> children);
+ Expr mkExpr(Kind kind, std::vector<Expr> 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<Expr> 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..
#ifndef __CVC4_EXPR_VALUE_H
#define __CVC4_EXPR_VALUE_H
+#include <stdint.h>
#include "expr.h"
namespace CVC4 {
/** 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
XOR,
NOT,
PLUS,
- MINUS
+ MINUS,
+ ITE,
+ IFF,
+ SKOLEM,
+ SUBST
};/* enum Kind */
}/* CVC4 namespace */
+++ /dev/null
-/********************* -*- 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 <iostream>
-
-#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 */
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 $@ $<
--- /dev/null
+/********************* -*- 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 <iostream>
+#include <sstream>
+#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 */
+/********************* -*- 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
- *
- * <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>
- *
- */
-/*****************************************************************************/
-/* 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
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());
}
+/********************* -*- 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
- *
- * <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 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;
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
// 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; }
%}
-%option interactive
-%option noyywrap
-%option nounput
-%option noreject
-%option noyymore
-%option yylineno
-
%x COMMENT
%x STRING_LITERAL
%%
-[\n] { CVC4::parserTemp->lineNum++; }
+[\n] { CVC4::parserState->lineNum++; }
[ \t\r\f] { /* skip whitespace */ }
"%" { BEGIN COMMENT; }
<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */
- CVC4::parserTemp->lineNum++; }
+ CVC4::parserState->lineNum++; }
<COMMENT>. { /* stay in comment mode */ }
<INITIAL>"\"" { BEGIN STRING_LITERAL;
-%{
-/*****************************************************************************/
-/*!
- * \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.
-*/
+%{/******************* -*- 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)
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());
}
%union {
std::string *str;
std::vector<std::string> *strvec;
- CVC4::Expr *node;
- std::vector<CVC4::Expr> *vec;
- std::pair<std::vector<CVC4::Expr>, std::vector<std::string> > *pat_ann;
+ CVC3::Expr *node;
+ std::vector<CVC3::Expr> *vec;
+ std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann;
};
}
;
-
-
%%
-%{
-/*****************************************************************************/
-/*!
- * \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>
- *
- */
-/*****************************************************************************/
+/********************* -*- 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 <iostream>
-#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;
%}
-%option interactive
-%option noyywrap
-%option nounput
-%option noreject
-%option noyymore
-%option yylineno
-
%x COMMENT
%x STRING_LITERAL
%x USER_VALUE
. { smtliberror("Illegal input character."); }
%%
-
projects / cvc5.git / commitdiff