diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-06 02:21:46 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-06 02:21:46 +0000 |
commit | c16be5841e613818d5764e4de99e4694a0703685 (patch) | |
tree | 5bf7c07a8f7200c2830d50f5dd83ecbb4f02444d /src/util | |
parent | 200f36785acf7aac3e7e230795ea7ffdb6b1ed64 (diff) |
Big chunk of changes:
* Fixed bugs in option parsing
* Simplified the main.cpp significantly (more c++ like)
* Added the null kind, expr value, and expression, with the default constructor public
* Simplified commands, we need to discuss this in the meeting (what to do with command results?)
* Removed all the lex/yacc files
* Symbol table is now a templated class, as we will have tables for variables, predicates and functions
* The ANTLR parsing infrastructure/makefiles is all in. SMT lib Boolean benchmarks should parse + giving nice error such as
Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test4.smt:3:16: Undeclared variable p
Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test2.smt:2:11: unexpected token: sa
Didn't add any unit tests as the unit testing doesn't work with the updated build system -- it doesn't know how to create directories in the corresponding build directory.
TODO:
* add the PL grammar and unit test when the testing becomes available
* with this build setup my eclipse debugger doesn't work. Might have something to do with the visibility of symbols?
* i'm getting g++ depracated warnings regarding the hash_map from the symbol table, need to figure out how to use it in a standard manner. the new <unordered_map> header is for C++0x, and the <ext/hash_map> is getting deprecation warningns... weird.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/command.cpp | 68 | ||||
-rw-r--r-- | src/util/command.h | 44 | ||||
-rw-r--r-- | src/util/options.h | 16 |
3 files changed, 74 insertions, 54 deletions
diff --git a/src/util/command.cpp b/src/util/command.cpp index 9e541574a..e38695b46 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -7,71 +7,99 @@ #include "util/command.h" #include "smt/smt_engine.h" +#include "expr/expr.h" #include "util/result.h" +namespace std { +ostream& operator<<(ostream& out, const CVC4::Command& c) { + c.toString(out); + return out; +} +} + namespace CVC4 { EmptyCommand::EmptyCommand() { } -Result EmptyCommand::invoke(SmtEngine* smt_engine) { - return Result::VALIDITY_UNKNOWN; +void EmptyCommand::invoke(SmtEngine* smt_engine) { } AssertCommand::AssertCommand(const Expr& e) : d_expr(e) { } -Result AssertCommand::invoke(SmtEngine* smt_engine) { - return smt_engine->assert(d_expr); +void AssertCommand::invoke(SmtEngine* smt_engine) { + smt_engine->assert(d_expr); } -CheckSatCommand::CheckSatCommand() : - d_expr(Expr::null()) { +CheckSatCommand::CheckSatCommand() { } CheckSatCommand::CheckSatCommand(const Expr& e) : d_expr(e) { } -Result CheckSatCommand::invoke(SmtEngine* smt_engine) { - return smt_engine->checkSat(d_expr); +void CheckSatCommand::invoke(SmtEngine* smt_engine) { + smt_engine->checkSat(d_expr); } QueryCommand::QueryCommand(const Expr& e) : d_expr(e) { } -Result QueryCommand::invoke(CVC4::SmtEngine* smt_engine) { - return smt_engine->query(d_expr); +void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) { + smt_engine->query(d_expr); } CommandSequence::CommandSequence() : d_last_index(0) { } -CommandSequence::CommandSequence(Command* cmd) : - d_last_index(0) { - addCommand(cmd); -} - - CommandSequence::~CommandSequence() { for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) delete d_command_sequence[i]; } -Result CommandSequence::invoke(SmtEngine* smt_engine) { - Result r = Result::VALIDITY_UNKNOWN; +void CommandSequence::invoke(SmtEngine* smt_engine) { for(; d_last_index < d_command_sequence.size(); ++d_last_index) { - r = d_command_sequence[d_last_index]->invoke(smt_engine); + d_command_sequence[d_last_index]->invoke(smt_engine); delete d_command_sequence[d_last_index]; } - return r; } void CommandSequence::addCommand(Command* cmd) { d_command_sequence.push_back(cmd); } +// Printout methods + +using namespace std; + +void EmptyCommand::toString(ostream& out) const { + out << "EmptyCommand"; +} + +void AssertCommand::toString(ostream& out) const { + out << "Assert(" << d_expr << ")"; +} + +void CheckSatCommand::toString(ostream& out) const { + if(d_expr.isNull()) + out << "CheckSat()"; + else + out << "CheckSat(" << d_expr << ")"; +} + +void QueryCommand::toString(ostream& out) const { + out << "Query(" << d_expr << ")"; +} + +void CommandSequence::toString(ostream& out) const { + out << "CommandSequence[" << endl; + for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) + out << *d_command_sequence[i] << endl; + out << "]"; +} + }/* CVC4 namespace */ diff --git a/src/util/command.h b/src/util/command.h index c65429fdb..ce137896a 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -16,7 +16,6 @@ #include "cvc4_config.h" #include "expr/expr.h" -#include "util/result.h" namespace CVC4 { class SmtEngine; @@ -25,15 +24,14 @@ namespace CVC4 { }/* CVC4 namespace */ namespace std { -inline std::ostream& operator<<(std::ostream&, const CVC4::Command*) CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC; + std::ostream& operator<<(std::ostream&, const CVC4::Command&) CVC4_PUBLIC; } namespace CVC4 { class CVC4_PUBLIC Command { public: - virtual Result invoke(CVC4::SmtEngine* smt_engine) = 0; + virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; virtual ~Command() {}; virtual void toString(std::ostream&) const = 0; };/* class Command */ @@ -41,8 +39,8 @@ public: class CVC4_PUBLIC EmptyCommand : public Command { public: EmptyCommand(); - Result invoke(CVC4::SmtEngine* smt_engine); - void toString(std::ostream& out) const { out << "EmptyCommand"; } + void invoke(CVC4::SmtEngine* smt_engine); + void toString(std::ostream& out) const; };/* class EmptyCommand */ @@ -51,8 +49,8 @@ protected: Expr d_expr; public: AssertCommand(const Expr& e); - Result invoke(CVC4::SmtEngine* smt_engine); - void toString(std::ostream& out) const { out << "Assert(" << d_expr << ")"; } + void invoke(CVC4::SmtEngine* smt_engine); + void toString(std::ostream& out) const; };/* class AssertCommand */ @@ -60,8 +58,8 @@ class CVC4_PUBLIC CheckSatCommand : public Command { public: CheckSatCommand(); CheckSatCommand(const Expr& e); - Result invoke(SmtEngine* smt); - void toString(std::ostream& out) const { out << "CheckSat(" << d_expr << ")"; } + void invoke(SmtEngine* smt); + void toString(std::ostream& out) const; protected: Expr d_expr; };/* class CheckSatCommand */ @@ -70,8 +68,8 @@ protected: class CVC4_PUBLIC QueryCommand : public Command { public: QueryCommand(const Expr& e); - Result invoke(SmtEngine* smt); - void toString(std::ostream& out) const { out << "Query(" << d_expr << ")"; } + void invoke(SmtEngine* smt); + void toString(std::ostream& out) const; protected: Expr d_expr; };/* class QueryCommand */ @@ -80,21 +78,10 @@ protected: class CVC4_PUBLIC CommandSequence : public Command { public: CommandSequence(); - CommandSequence(Command* cmd); ~CommandSequence(); - Result invoke(SmtEngine* smt); + void invoke(SmtEngine* smt); void addCommand(Command* cmd); - void toString(std::ostream& out) const { - out << "CommandSequence("; - for(std::vector<Command*>::const_iterator i = d_command_sequence.begin(); - i != d_command_sequence.end(); - ++i) { - out << *i; - if(i != d_command_sequence.end()) - out << " ; "; - } - out << ")"; - } + void toString(std::ostream& out) const; private: /** All the commands to be executed (in sequence) */ std::vector<Command*> d_command_sequence; @@ -104,11 +91,4 @@ private: }/* CVC4 namespace */ -inline std::ostream& std::operator<<(std::ostream& out, const CVC4::Command* c) { - if(c) - c->toString(out); - else out << "(null)"; - return out; -} - #endif /* __CVC4__COMMAND_H */ diff --git a/src/util/options.h b/src/util/options.h index 54b4e2f9b..8d2d113a2 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -18,6 +18,7 @@ namespace CVC4 { struct Options { + std::string binary_name; bool smtcomp_mode; @@ -33,7 +34,18 @@ struct Options { /* with 3, the solver is slowed down by all the scrolling */ int verbosity; - std::string lang; + /** The input language option */ + enum InputLanguage { + /** The SMTLIB input language */ + LANG_SMTLIB, + /** The CVC4 input language */ + LANG_CVC4, + /** Auto-detect the language */ + LANG_AUTO + }; + + /** The input language */ + InputLanguage lang; Options() : binary_name(), smtcomp_mode(false), @@ -41,7 +53,7 @@ struct Options { out(0), err(0), verbosity(0), - lang() + lang(LANG_AUTO) {} };/* struct Options */ |