From 2eef69eb63f3a5637f8711944e3d056672872f20 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Fri, 18 Dec 2009 05:07:19 +0000 Subject: Lots of parser changes to make Chris happy. Yet more to come later. --- src/util/command.cpp | 75 +++++++++++++++++++++++++++++++++++++++++++++++----- src/util/command.h | 50 ++++++++++++++++++++++++++++++----- src/util/options.h | 9 ++++--- 3 files changed, 117 insertions(+), 17 deletions(-) (limited to 'src/util') diff --git a/src/util/command.cpp b/src/util/command.cpp index 5a5b766cb..b80851233 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -20,8 +20,9 @@ * Author: dejan */ -#include +#include #include "util/command.h" +#include "util/Assert.h" #include "smt/smt_engine.h" using namespace std; @@ -29,10 +30,16 @@ using namespace std; namespace CVC4 { ostream& operator<<(ostream& out, const Command& c) { - c.toString(out); + c.toStream(out); return out; } +std::string Command::toString() const { + stringstream ss; + toStream(ss); + return ss.str(); +} + EmptyCommand::EmptyCommand(string name) : d_name(name) { } @@ -87,26 +94,26 @@ void CommandSequence::addCommand(Command* cmd) { d_command_sequence.push_back(cmd); } -void EmptyCommand::toString(ostream& out) const { +void EmptyCommand::toStream(ostream& out) const { out << "EmptyCommand(" << d_name << ")"; } -void AssertCommand::toString(ostream& out) const { +void AssertCommand::toStream(ostream& out) const { out << "Assert(" << d_expr << ")"; } -void CheckSatCommand::toString(ostream& out) const { +void CheckSatCommand::toStream(ostream& out) const { if(d_expr.isNull()) out << "CheckSat()"; else out << "CheckSat(" << d_expr << ")"; } -void QueryCommand::toString(ostream& out) const { +void QueryCommand::toStream(ostream& out) const { out << "Query(" << d_expr << ")"; } -void CommandSequence::toString(ostream& out) const { +void CommandSequence::toStream(ostream& out) const { out << "CommandSequence[" << endl; for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) { out << *d_command_sequence[i] << endl; @@ -114,4 +121,58 @@ void CommandSequence::toString(ostream& out) const { out << "]"; } +DeclarationCommand::DeclarationCommand(const std::vector& ids) : + d_declaredSymbols(ids) { +} + +void DeclarationCommand::toStream(std::ostream& out) const { + out << "Declare("; + bool first = true; + for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) { + if(first) { + out << ", "; + first = false; + } + out << d_declaredSymbols[i]; + } + out << ")"; +} + +SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : + d_status(status) { +} + +void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) { + // TODO: something to be done with the status +} + +void SetBenchmarkStatusCommand::toStream(std::ostream& out) const { + out << "SetBenchmarkStatus("; + switch(d_status) { + case SMT_SATISFIABLE: + out << "sat"; + break; + case SMT_UNSATISFIABLE: + out << "unsat"; + break; + case SMT_UNKNOWN: + out << "unknown"; + break; + default: + Unhandled("Unknown benchmark status"); + } + out << ")"; +} + +SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(string logic) : d_logic(logic) + {} + +void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) { + // TODO: something to be done with the logic +} + +void SetBenchmarkLogicCommand::toStream(std::ostream& out) const { + out << "SetBenchmarkLogic(" << d_logic << ")"; +} + }/* CVC4 namespace */ diff --git a/src/util/command.h b/src/util/command.h index 9cc009d01..b41be4592 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -35,14 +35,15 @@ class CVC4_PUBLIC Command { public: virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; virtual ~Command() {}; - virtual void toString(std::ostream&) const = 0; + virtual void toStream(std::ostream&) const = 0; + std::string toString() const; };/* class Command */ class CVC4_PUBLIC EmptyCommand : public Command { public: EmptyCommand(std::string name = ""); void invoke(CVC4::SmtEngine* smt_engine); - void toString(std::ostream& out) const; + void toStream(std::ostream& out) const; private: std::string d_name; };/* class EmptyCommand */ @@ -52,18 +53,26 @@ class CVC4_PUBLIC AssertCommand : public Command { public: AssertCommand(const BoolExpr& e); void invoke(CVC4::SmtEngine* smt_engine); - void toString(std::ostream& out) const; + void toStream(std::ostream& out) const; protected: BoolExpr d_expr; };/* class AssertCommand */ +class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { +public: + DeclarationCommand(const std::vector& ids); + void toStream(std::ostream& out) const; +protected: + std::vector d_declaredSymbols; +}; + class CVC4_PUBLIC CheckSatCommand : public Command { public: CheckSatCommand(); CheckSatCommand(const BoolExpr& e); void invoke(SmtEngine* smt); - void toString(std::ostream& out) const; + void toStream(std::ostream& out) const; protected: BoolExpr d_expr; };/* class CheckSatCommand */ @@ -73,19 +82,48 @@ class CVC4_PUBLIC QueryCommand : public Command { public: QueryCommand(const BoolExpr& e); void invoke(SmtEngine* smt); - void toString(std::ostream& out) const; + void toStream(std::ostream& out) const; protected: BoolExpr d_expr; };/* class QueryCommand */ +class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { +public: + /** The status an SMT benchmark can have */ + enum BenchmarkStatus { + /** Benchmark is satisfiable */ + SMT_SATISFIABLE, + /** Benchmark is unsatisfiable */ + SMT_UNSATISFIABLE, + /** The status of the benchmark is unknown */ + SMT_UNKNOWN + }; + SetBenchmarkStatusCommand(BenchmarkStatus status); + void invoke(SmtEngine* smt); + void toStream(std::ostream& out) const; +protected: + BenchmarkStatus d_status; +};/* class QueryCommand */ + +class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { +public: + SetBenchmarkLogicCommand(std::string logic); + void invoke(SmtEngine* smt); + void toStream(std::ostream& out) const; +protected: + std::string d_logic; +};/* class QueryCommand */ + + + class CVC4_PUBLIC CommandSequence : public Command { public: CommandSequence(); ~CommandSequence(); void invoke(SmtEngine* smt); void addCommand(Command* cmd); - void toString(std::ostream& out) const; + void toStream(std::ostream& out) const; private: /** All the commands to be executed (in sequence) */ std::vector d_command_sequence; diff --git a/src/util/options.h b/src/util/options.h index 2bfbf675f..d6c4e9009 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -13,11 +13,12 @@ ** Global (command-line or equivalent) tuning parameters. **/ -#include - #ifndef __CVC4__OPTIONS_H #define __CVC4__OPTIONS_H +#include +#include "parser/parser.h" + namespace CVC4 { struct Options { @@ -48,7 +49,7 @@ struct Options { }; /** The input language */ - InputLanguage lang; + parser::Parser::InputLanguage lang; Options() : binary_name(), smtcomp_mode(false), @@ -56,7 +57,7 @@ struct Options { out(0), err(0), verbosity(0), - lang(LANG_AUTO) + lang(parser::Parser::LANG_AUTO) {} };/* struct Options */ -- cgit v1.2.3