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/command.cpp | |
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/command.cpp')
-rw-r--r-- | src/util/command.cpp | 68 |
1 files changed, 48 insertions, 20 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 */ |