SUBDIRS = src test doc contrib
+.PHONY: production debug default competition
+production: ; @srcdir@/configure --with-build=production && $(MAKE)
+debug: ; @srcdir@/configure --with-build=debug && $(MAKE)
+default: ; @srcdir@/configure --with-build=default && $(MAKE)
+competition:; @srcdir@/configure --with-build=competition && $(MAKE)
# keep track of whether the user set these (check here, because
# autoconf might set a default later)
+AC_MSG_CHECKING([for user CPPFLAGS])
if test -z "${CPPFLAGS+set}"; then user_cppflags=no; else user_cppflags=yes; fi
+AC_MSG_RESULT([${CPPFLAGS-none}])
+AC_MSG_CHECKING([for user CXXFLAGS])
if test -z "${CXXFLAGS+set}"; then user_cxxflags=no; else user_cxxflags=yes; fi
+AC_MSG_RESULT([${CXXFLAGS-none}])
+AC_MSG_CHECKING([for user LDFLAGS])
if test -z "${LDFLAGS+set}" ; then user_ldflags=no ; else user_ldflags=yes ; fi
+AC_MSG_RESULT([${LDFLAGS-none}])
LT_INIT
# Prepare configure output
+if test "$user_cppflags" = no; then
+ CPPFLAGS="$CVC4CPPFLAGS"
+fi
+if test "$user_cxxflags" = no; then
+ CXXFLAGS="$CVC4CXXFLAGS"
+fi
+if test "$user_ldflags" = no; then
+ LDFLAGS="$CVC4LDFLAGS"
+fi
+
AC_CONFIG_FILES([
Makefile
contrib/Makefile
Now just type make, followed by make check or make install, as you like.
-You can also use 'make build_profile' to reconfigure for a different profile.
+You can use 'make <build_profile>' to reconfig/build a different profile.
Build profiles: production optimized default competition
EOF
AC_MSG_WARN([To support your options to configure, I would like to set CPPFLAGS to:])
AC_MSG_WARN([ $CVC4CPPFLAGS])
AC_MSG_WARN([])
-else
- CPPFLAGS="$CVC4CPPFLAGS"
fi
if test "$user_cxxflags" = yes; then
AC_MSG_WARN([])
AC_MSG_WARN([To support your options to configure, I would like to set CXXFLAGS to:])
AC_MSG_WARN([ $CVC4CXXFLAGS])
AC_MSG_WARN([])
-else
- CXXFLAGS="$CVC4CXXFLAGS"
fi
if test "$user_ldflags" = yes; then
AC_MSG_WARN([])
AC_MSG_WARN([To support your options to configure, I would like to set LDFLAGS to:])
AC_MSG_WARN([ $CVC4LDFLAGS])
AC_MSG_WARN([])
-else
- LDFLAGS="$CVC4LDFLAGS"
fi
non_standard=
/*
* Construct an SmtEngine with the given expression manager and user options.
*/
- SmtEngine(ExprManager*, Options*);
+ SmtEngine(ExprManager*, Options*) throw();
/**
* Execute a command.
cmd->invoke();
delete cmd;
}
-
- if(infile)
- infile.close();
} catch(CVC4::main::OptionException* e) {
if(opts.smtcomp_mode) {
printf("unknown");
noinst_LTLIBRARIES = libparser.la
libparser_la_SOURCES = \
+ parser.cpp \
+ parser_state.cpp \
+ symbol_table.cpp \
pl_scanner.lpp \
- pl.ypp # \
- # smtlib_scanner.lpp \
- # smtlib.ypp \
- # parser.cpp
+ pl.ypp
+# smtlib_scanner.lpp \
+# smtlib.ypp
BUILT_SOURCES = \
pl_scanner.cpp \
pl.cpp \
- pl.hpp # \
- # smtlib_scanner.cpp \
- # smtlib.cpp \
- # smtlib.hpp
+ pl.hpp \
+ smtlib_scanner.cpp \
+ smtlib.cpp \
+ smtlib.hpp
# produce headers too
AM_YFLAGS = -d
** information.
**
** Parser implementation.
- **
- ** The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
**/
-#include "parser.h"
-#include "parser_temp.h"
-#include "parser_exception.h"
+#include "parser/parser.h"
+#include "parser/parser_state.h"
+#include "parser/parser_exception.h"
+#include "parser/pl.hpp"
+//#include "parser/smtlib.hpp"
+
+// The communication entry points of the actual parsers
+
+// for presentation language (PL.y and PL.lex)
+extern int PLparse();
+extern void *PL_createBuffer(int);
+extern void PL_deleteBuffer(void *);
+extern void PL_switchToBuffer(void *);
+extern int PL_bufSize();
+extern void *PL_bufState();
+void PL_setInteractive(bool);
+
+// for smtlib language (smtlib.y and smtlib.lex)
+extern int smtlibparse();
+extern void *smtlib_createBuffer(int);
+extern void smtlib_deleteBuffer(void *);
+extern void smtlib_switchToBuffer(void *);
+extern int smtlib_bufSize();
+extern void *smtlibBufState();
+void smtlib_setInteractive(bool);
namespace CVC4 {
+namespace parser {
-ParserTemp *parserTemp;
+ParserState *parserState;
-}/* CVC4 namespace */
+Parser::Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive) throw()
+ : d_smt(smt),
+ d_is(is),
+ d_opts(opts),
+ d_lang(lang),
+ d_interactive(interactive),
+ d_buffer(0) {
+
+ parserState->lineNum = 1;
+ switch(d_lang) {
+ case PL:
+ d_buffer = ::PL_createBuffer(::PL_bufSize());
+ break;
+ case SMTLIB:
+ //d_buffer = ::smtlib_createBuffer(::smtlib_bufSize());
+ break;
+ default:
+ Unhandled();
+ }
+}
+Parser::~Parser() throw() {
+ switch(d_lang) {
+ case PL:
+ ::PL_deleteBuffer(d_buffer);
+ break;
+ case SMTLIB:
+ //::smtlib_deleteBuffer(d_buffer);
+ break;
+ default:
+ Unhandled();
+ }
+}
+
+CVC4::Command* Parser::next() throw() {
+ return 0;
+}
+
+bool Parser::done() const throw() {
+ return false;
+}
+
+void Parser::printLocation(std::ostream & out) const throw() {
+}
+
+void Parser::reset() throw() {
+}
+
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
#ifndef __CVC4__PARSER__PARSER_H
#define __CVC4__PARSER__PARSER_H
+#include <iostream>
+
#include "util/exception.h"
#include "parser/language.h"
+#include "parser/parser_state.h"
#include "util/command.h"
+#include "util/options.h"
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
+#include "util/assert.h"
namespace CVC4 {
namespace parser {
- class 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(CVC4::SmtEngine* smt, Language lang, std::istream& is, Options* opts, bool interactive = false);
- // Destructor
- ~Parser();
- // Read the next command.
- CVC4::Command* 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;
+class Parser {
+
+ CVC4::SmtEngine *d_smt;
+ std::istream &d_is;
+ CVC4::Options *d_opts;
+ Language d_lang;
+ bool d_interactive;
+ void *d_buffer;
+
+public:
+ // Constructors
+ Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive = false) throw();
+ // Destructor
+ ~Parser() throw();
+ // Read the next command.
+ CVC4::Command* next() throw();
+ // Check if we are done (end of input has been reached)
+ bool done() const throw();
+ // The same check can be done by using the class Parser's value as
+ // a Boolean
+ operator bool() const throw() { return done(); }
+ void printLocation(std::ostream & out) const throw();
+ // Reset any local data that depends on SmtEngine
+ void reset() throw();
+}; // end of class Parser
}/* CVC4::parser namespace */
}/* CVC4 namespace */
#define __CVC4__PARSER__PARSER_EXCEPTION_H
#include "util/exception.h"
+#include "cvc4_config.h"
#include <string>
#include <iostream>
namespace CVC4 {
namespace parser {
- 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
+class CVC4_PUBLIC 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
}/* CVC4::parser namespace */
}/* CVC4 namespace */
--- /dev/null
+/********************* -*- C++ -*- */
+/** parser_state.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Parser state implementation.
+ **/
+
+#include <string>
+#include "parser/parser_state.h"
+#include "parser/parser_exception.h"
+
+namespace CVC4 {
+namespace parser {
+
+void ParserState::error(const std::string& s) throw(ParserException*) {
+ throw new ParserException(s);
+}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "parser/symbol_table.h"
+#include "parser/parser_exception.h"
#include "util/exception.h"
namespace CVC4 {
// The currently used prompt
std::string prompt;
public:
- SmtEngine* smtEngine;
- ExprManager* exprManager;
+ CVC4::SmtEngine* smtEngine;
+ CVC4::ExprManager* exprManager;
SymbolTable* symbolTable;
std::istream* is;
// The current input line
// File name
std::string fileName;
// The last parsed Expr
- Expr expr;
+ CVC4::Expr expr;
// Whether we are done or not
bool done;
// Whether we are running interactive
// Did we encounter a formula query (smtlib)
bool queryParsed;
// Default constructor
- ParserState() : d_uid(0),
- prompt1("CVC> "),
- prompt2("- "),
- prompt("CVC> "),
- smtEngine(0),
- exprManager(0),
- symbolTable(0),
- is(0),
- lineNum(1),
- fileName(),
- expr(Expr::null()),
- done(false),
- interactive(false),
- arrFlag(false),
- bvFlag(false),
- bvSize(0),
- queryParsed(false) { }
+ ParserState() throw()
+ : d_uid(0),
+ prompt1("CVC> "),
+ prompt2("- "),
+ prompt("CVC> "),
+ smtEngine(0),
+ exprManager(0),
+ symbolTable(0),
+ is(0),
+ lineNum(1),
+ fileName(),
+ expr(CVC4::Expr::null()),
+ done(false),
+ interactive(false),
+ arrFlag(false),
+ bvFlag(false),
+ bvSize(0),
+ queryParsed(false) { }
// Parser error handling (implemented in parser.cpp)
- int error(const std::string& s);
+ void error(const std::string& s) throw(ParserException*) __attribute__((noreturn));
// Get the next uniqueID as a string
- std::string uniqueID() {
+ std::string uniqueID() throw() {
std::ostringstream ss;
ss << d_uid++;
return ss.str();
}
// Get the current prompt
- std::string getPrompt() { return prompt; }
+ std::string getPrompt() throw() { return prompt; }
// Set the prompt to the main one
- void setPrompt1() { prompt = prompt1; }
+ void setPrompt1() throw() { prompt = prompt1; }
// Set the prompt to the secondary one
- void setPrompt2() { prompt = prompt2; }
+ void setPrompt2() throw() { prompt = prompt2; }
};
}/* CVC4::parser namespace */
std::ostringstream ss;
ss << CVC4::parser::parserState->fileName << ":" << CVC4::parser::parserState->lineNum
<< ": " << s;
- return CVC4::parser::parserState->error(ss.str());
+ CVC4::parser::parserState->error(ss.str());
+ return 0;// dead code; error() above throws an exception
}
#define YYLTYPE_IS_TRIVIAL 1
--- /dev/null
+/********************* -*- C++ -*- */
+/** symbol_table.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ **/
+
+#include <string>
+#include <list>
+#include <vector>
+
+#include "expr/expr.h"
+#include "parser/symbol_table.h"
+
+namespace CVC4 {
+namespace parser {
+
+void SymbolTable::defineVar(const std::string, const void*) throw() {
+
+}
+
+void SymbolTable::defineVarList(const std::list<std::string>*, const void*) throw() {
+}
+
+void SymbolTable::defineVarList(const std::vector<std::string>*, const void*) throw() {
+}
+
+// Type& SymbolTable::lookupType(const std::string&);
+Expr& SymbolTable::lookupVar(const std::string*) throw() {
+}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** 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
**/
#include <string>
#include "expr/expr.h"
namespace CVC4 {
+namespace parser {
class SymbolTable {
public:
// FIXME: No definitions for Type yet
// void defineType(const std::string&, const Type&);
- void defineVar(const std::string, const void*);
- void defineVarList(const std::list<std::string>*, const void*);
- void defineVarList(const std::vector<std::string>*, const void*);
+ void defineVar(const std::string, const void*) throw();
+ void defineVarList(const std::list<std::string>*, const void*) throw();
+ void defineVarList(const std::vector<std::string>*, const void*) throw();
// Type& lookupType(const std::string&);
- Expr& lookupVar(const std::string*);
+ Expr& lookupVar(const std::string*) throw();
};
-}
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
**/
#include "smt/smt_engine.h"
+#include "util/exception.h"
+#include "util/command.h"
namespace CVC4 {
+void doCommand(Command* c) {
+ if(c->getSmtEngine() != this)
+ throw new IllegalArgumentException("SmtEngine does not match Command");
+
+ c->invoke();
+}
+
}/* CVC4 namespace */
#include <vector>
#include "expr/expr.h"
#include "expr/expr_manager.h"
-#include "util/command.h"
#include "util/result.h"
#include "util/model.h"
#include "util/options.h"
namespace CVC4 {
+class Command;
+
// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
// hood): use a type parameter and have check() delegate, or subclass
// SmtEngine and override check()?
/*
* Construct an SmtEngine with the given expression manager and user options.
*/
- SmtEngine(ExprManager* em, Options* opts) : d_em(em), d_opts(opts) {}
+ SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts) {}
/**
* Execute a command.
*/
Result query(Expr);
+ /**
+ * Add a formula to the current context and call check(). Returns
+ * true iff consistent.
+ */
+ Result checkSat(Expr);
+
/**
* Simplify a formula without doing "much" work. Requires assist
* from the SAT Engine.
noinst_LTLIBRARIES = libutil.la
-libutil_la_SOURCES =
+libutil_la_SOURCES = \
+ command.cpp
namespace CVC4 {
-class AssertionException : public Exception {
+class CVC4_PUBLIC AssertionException : public Exception {
public:
AssertionException() : Exception() {}
AssertionException(std::string msg) : Exception(msg) {}
AssertionException(const char* msg) : Exception(msg) {}
};/* class AssertionException */
-class UnreachableCodeException : public AssertionException {
+class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
public:
UnreachableCodeException() : AssertionException() {}
UnreachableCodeException(std::string msg) : AssertionException(msg) {}
UnreachableCodeException(const char* msg) : AssertionException(msg) {}
};/* class UnreachableCodeException */
+class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
+public:
+ UnhandledCaseException() : UnreachableCodeException() {}
+ UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {}
+ UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {}
+};/* class UnhandledCaseException */
+
#ifdef CVC4_ASSERTIONS
# define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg)
#else /* ! CVC4_ASSERTIONS */
#endif /* CVC4_ASSERTIONS */
#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg)
-#define Unreachable(cond, msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, __builtin_expect((cond), 1), ## msg)
+#define Unreachable(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg)
+#define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg)
#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg)
-#define __CVC4_UNREACHABLEGLUE(str, line, cond, msg...) AssertImpl(str #line, cond, ## msg)
+#define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg)
+#define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg)
inline void AssertImpl(const char* info, bool cond, std::string msg) {
if(EXPECT_FALSE( ! cond ))
throw new UnreachableCodeException(info);
}
+#ifdef __GNUC__
+inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn));
+inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn));
+inline void UnhandledImpl(const char* info) __attribute__ ((noreturn));
+#endif /* __GNUC__ */
+
+inline void UnhandledImpl(const char* info, std::string msg) {
+ throw new UnhandledCaseException(std::string(info) + "\n" + msg);
+}
+
+inline void UnhandledImpl(const char* info, const char* msg) {
+ throw new UnhandledCaseException(std::string(info) + "\n" + msg);
+}
+
+inline void UnhandledImpl(const char* info) {
+ throw new UnhandledCaseException(info);
+}
+
}/* CVC4 namespace */
#endif /* __CVC4__ASSERT_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** command.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ **/
+
+#include "util/command.h"
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+
+}/* CVC4 namespace */
#define __CVC4__COMMAND_H
#include "expr/expr.h"
+#include "smt/smt_engine.h"
namespace CVC4 {
-class SmtEngine;
-
class Command {
+protected:
SmtEngine* d_smt;
public:
Command(CVC4::SmtEngine* smt) : d_smt(smt) {}
+ SmtEngine* getSmtEngine() { return d_smt; }
virtual void invoke() = 0;
};
class AssertCommand : public Command {
+protected:
+ Expr d_expr;
+
public:
- AssertCommand(const Expr&);
- void invoke() { }
+ AssertCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
+ void invoke() { d_smt->assert(d_expr); }
};
class CheckSatCommand : public Command {
+protected:
+ Expr d_expr;
+
public:
- CheckSatCommand(void);
- CheckSatCommand(const Expr&);
- void invoke() { }
+ CheckSatCommand(CVC4::SmtEngine* smt) : Command(smt), d_expr(Expr::null()) {}
+ CheckSatCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
+ void invoke() { d_smt->checkSat(d_expr); }
};
class QueryCommand : public Command {
+protected:
+ Expr d_expr;
+
public:
- QueryCommand(const Expr&);
- void invoke() { }
+ QueryCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
+ void invoke() { d_smt->query(d_expr); }
};
-
}/* CVC4 namespace */
#endif /* __CVC4__COMMAND_H */
#include <string>
#include <iostream>
+#include "cvc4_config.h"
namespace CVC4 {
-class Exception {
+class CVC4_PUBLIC 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) { }
+ Exception() : d_msg("Unknown exception") {}
+ Exception(const std::string& msg) : d_msg(msg) {}
+ Exception(const char* msg) : d_msg(msg) {}
// Destructor
- virtual ~Exception() { }
+ 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,
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);
+};/* class Exception */
+
+
+class CVC4_PUBLIC IllegalArgumentException : public Exception {
+public:
+ IllegalArgumentException() : Exception("Illegal argument to method or function") {}
+ IllegalArgumentException(const std::string& msg) : Exception(msg) {}
+ IllegalArgumentException(const char* msg) : Exception(msg) {}
+};/* class IllegalArgumentException */
-}; // end of class Exception
inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
return os << e.toString();
}
+
}/* CVC4 namespace */
#endif /* __CVC4__EXCEPTION_H */
projects / cvc5.git / commitdiff