diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
commit | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (patch) | |
tree | 8db12e260b24978bbbed3363846f6daf7c0da04f /src/expr/command.cpp | |
parent | 5e2f381b26d683691d9a040589536dc39c5831e0 (diff) |
parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r-- | src/expr/command.cpp | 402 |
1 files changed, 380 insertions, 22 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 6c466a74c..a1486fcab 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -16,13 +16,24 @@ ** Implementation of command objects. **/ +#include <iostream> +#include <vector> +#include <utility> +#include <iterator> + #include "expr/command.h" #include "smt/smt_engine.h" +#include "util/output.h" using namespace std; namespace CVC4 { +std::ostream& operator<<(std::ostream& out, const Command& c) { + c.toStream(out); + return out; +} + ostream& operator<<(ostream& out, const Command* command) { if(command == NULL) { out << "null"; @@ -32,12 +43,136 @@ ostream& operator<<(ostream& out, const Command* command) { return out; } +/* class Command */ + +void Command::invoke(SmtEngine* smtEngine, std::ostream& out) { + invoke(smtEngine); + printResult(out); +} + +std::string Command::toString() const { + std::stringstream ss; + toStream(ss); + return ss.str(); +} + +void Command::printResult(std::ostream& out) const { +} + +/* class EmptyCommand */ + +EmptyCommand::EmptyCommand(std::string name) : + d_name(name) { +} + +void EmptyCommand::invoke(SmtEngine* smtEngine) { + /* empty commands have no implementation */ +} + +void EmptyCommand::toStream(std::ostream& out) const { + out << "EmptyCommand(" << d_name << ")"; +} + +/* class AssertCommand */ + +AssertCommand::AssertCommand(const BoolExpr& e) : + d_expr(e) { +} + +void AssertCommand::invoke(SmtEngine* smtEngine) { + smtEngine->assertFormula(d_expr); +} + +void AssertCommand::toStream(std::ostream& out) const { + out << "Assert(" << d_expr << ")"; +} + +/* class PushCommand */ + +void PushCommand::invoke(SmtEngine* smtEngine) { + smtEngine->push(); +} + +void PushCommand::toStream(std::ostream& out) const { + out << "Push()"; +} + +/* class PopCommand */ + +void PopCommand::invoke(SmtEngine* smtEngine) { + smtEngine->pop(); +} + +void PopCommand::toStream(std::ostream& out) const { + out << "Pop()"; +} + +/* class CheckSatCommand */ + +CheckSatCommand::CheckSatCommand(const BoolExpr& expr) : + d_expr(expr) { +} + +void CheckSatCommand::invoke(SmtEngine* smtEngine) { + d_result = smtEngine->checkSat(d_expr); +} + +void CheckSatCommand::toStream(std::ostream& out) const { + if(d_expr.isNull()) { + out << "CheckSat()"; + } else { + out << "CheckSat(" << d_expr << ")"; + } +} + +Result CheckSatCommand::getResult() const { + return d_result; +} + +void CheckSatCommand::printResult(std::ostream& out) const { + out << d_result << endl; +} + +/* class QueryCommand */ + +QueryCommand::QueryCommand(const BoolExpr& e) : + d_expr(e) { +} + +void QueryCommand::invoke(SmtEngine* smtEngine) { + d_result = smtEngine->query(d_expr); +} + +Result QueryCommand::getResult() const { + return d_result; +} + +void QueryCommand::printResult(std::ostream& out) const { + out << d_result << endl; +} + +void QueryCommand::toStream(std::ostream& out) const { + out << "Query("; + d_expr.printAst(out, 0); + out << ")"; +} + +/* class CommandSequence */ + +CommandSequence::CommandSequence() : + d_index(0) { +} + CommandSequence::~CommandSequence() { for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { delete d_commandSequence[i]; } } +void CommandSequence::addCommand(Command* cmd) { + d_commandSequence.push_back(cmd); +} + void CommandSequence::invoke(SmtEngine* smtEngine) { for(; d_index < d_commandSequence.size(); ++d_index) { d_commandSequence[d_index]->invoke(smtEngine); @@ -45,11 +180,10 @@ void CommandSequence::invoke(SmtEngine* smtEngine) { } } -void CheckSatCommand::toStream(std::ostream& out) const { - if(d_expr.isNull()) { - out << "CheckSat()"; - } else { - out << "CheckSat(" << d_expr << ")"; +void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) { + for(; d_index < d_commandSequence.size(); ++d_index) { + d_commandSequence[d_index]->invoke(smtEngine, out); + delete d_commandSequence[d_index]; } } @@ -61,33 +195,257 @@ void CommandSequence::toStream(std::ostream& out) const { out << "]"; } +/* class DeclarationCommand */ + +DeclarationCommand::DeclarationCommand(const std::string& id, Type t) : + d_type(t) { + d_declaredSymbols.push_back(id); +} + +DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, Type t) : + d_declaredSymbols(ids), + d_type(t) { +} + void DeclarationCommand::toStream(std::ostream& out) const { - out << "Declare("; - bool first = true; - for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) { - if(!first) { - out << ", "; - } - out << d_declaredSymbols[i]; - first = false; + out << "Declare(["; + copy( d_declaredSymbols.begin(), d_declaredSymbols.end() - 1, + ostream_iterator<string>(out, ", ") ); + out << d_declaredSymbols.back(); + out << "])"; +} + +/* class DefineFunctionCommand */ + +DefineFunctionCommand::DefineFunctionCommand(const std::string& name, + const std::vector<std::pair<std::string, Type> >& args, + Type type, + Expr formula) : + d_name(name), + d_args(args), + d_type(type), + d_formula(formula) { +} + +void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { + smtEngine->defineFunction(d_name, d_args, d_type, d_formula); +} + +void DefineFunctionCommand::toStream(std::ostream& out) const { + out << "DefineFunction( \"" << d_name << "\", ["; + copy( d_args.begin(), d_args.end() - 1, + ostream_iterator<std::pair<std::string, Type> >(out, ", ") ); + out << d_args.back(); + out << "], << " << d_type << " >>, << " << d_formula << " >> )"; +} + +/* class GetValueCommand */ + +GetValueCommand::GetValueCommand(Expr term) : + d_term(term) { +} + +void GetValueCommand::invoke(SmtEngine* smtEngine) { + d_result = smtEngine->getValue(d_term); +} + +Expr GetValueCommand::getResult() const { + return d_result; +} + +void GetValueCommand::printResult(std::ostream& out) const { + out << d_result << endl; +} + +void GetValueCommand::toStream(std::ostream& out) const { + out << "GetValue( << " << d_term << " >> )"; +} + +/* class GetAssertionsCommand */ + +GetAssertionsCommand::GetAssertionsCommand() { +} + +void GetAssertionsCommand::invoke(SmtEngine* smtEngine) { + stringstream ss; + const vector<Expr> v = smtEngine->getAssertions(); + copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") ); + d_result = ss.str(); +} + +std::string GetAssertionsCommand::getResult() const { + return d_result; +} + +void GetAssertionsCommand::printResult(std::ostream& out) const { + out << d_result; +} + +void GetAssertionsCommand::toStream(std::ostream& out) const { + out << "GetAssertions()"; +} + +/* class SetBenchmarkStatusCommand */ + +SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : + d_status(status) { +} + +void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) { + // FIXME: TODO: something to be done with the status +} + +void SetBenchmarkStatusCommand::toStream(std::ostream& out) const { + out << "SetBenchmarkStatus(" << d_status << ")"; +} + +/* class SetBenchmarkLogicCommand */ + +SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) : + d_logic(logic) { +} + +void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) { + // FIXME: TODO: something to be done with the logic +} + +void SetBenchmarkLogicCommand::toStream(std::ostream& out) const { + out << "SetBenchmarkLogic(" << d_logic << ")"; +} + +/* class SetInfoCommand */ + +SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) : + d_flag(flag), + d_sexpr(sexpr) { +} + +void SetInfoCommand::invoke(SmtEngine* smtEngine) { + try { + smtEngine->setInfo(d_flag, d_sexpr); + //d_result = "success"; + } catch(BadOption& bo) { + d_result = "unsupported"; } - out << ")"; } -void PushCommand::invoke(SmtEngine* smtEngine) { - smtEngine->push(); +std::string SetInfoCommand::getResult() const { + return d_result; } -void PushCommand::toStream(std::ostream& out) const { - out << "Push()"; +void SetInfoCommand::printResult(std::ostream& out) const { + if(d_result != "") { + out << d_result << endl; + } } -void PopCommand::invoke(SmtEngine* smtEngine) { - smtEngine->pop(); +void SetInfoCommand::toStream(std::ostream& out) const { + out << "SetInfo(" << d_flag << ", " << d_sexpr << ")"; } -void PopCommand::toStream(std::ostream& out) const { - out << "Pop()"; +/* class GetInfoCommand */ + +GetInfoCommand::GetInfoCommand(std::string flag) : + d_flag(flag) { +} + +void GetInfoCommand::invoke(SmtEngine* smtEngine) { + try { + d_result = smtEngine->getInfo(d_flag).getValue(); + } catch(BadOption& bo) { + d_result = "unsupported"; + } +} + +std::string GetInfoCommand::getResult() const { + return d_result; +} + +void GetInfoCommand::printResult(std::ostream& out) const { + if(d_result != "") { + out << d_result << endl; + } +} + +void GetInfoCommand::toStream(std::ostream& out) const { + out << "GetInfo(" << d_flag << ")"; +} + +/* class SetOptionCommand */ + +SetOptionCommand::SetOptionCommand(std::string flag, SExpr& sexpr) : + d_flag(flag), + d_sexpr(sexpr) { +} + +void SetOptionCommand::invoke(SmtEngine* smtEngine) { + try { + smtEngine->setOption(d_flag, d_sexpr); + //d_result = "success"; + } catch(BadOption& bo) { + d_result = "unsupported"; + } +} + +std::string SetOptionCommand::getResult() const { + return d_result; +} + +void SetOptionCommand::printResult(std::ostream& out) const { + if(d_result != "") { + out << d_result << endl; + } +} + +void SetOptionCommand::toStream(std::ostream& out) const { + out << "SetOption(" << d_flag << ", " << d_sexpr << ")"; +} + +/* class GetOptionCommand */ + +GetOptionCommand::GetOptionCommand(std::string flag) : + d_flag(flag) { +} + +void GetOptionCommand::invoke(SmtEngine* smtEngine) { + try { + d_result = smtEngine->getOption(d_flag).getValue(); + } catch(BadOption& bo) { + d_result = "unsupported"; + } +} + +std::string GetOptionCommand::getResult() const { + return d_result; +} + +void GetOptionCommand::printResult(std::ostream& out) const { + if(d_result != "") { + out << d_result << endl; + } +} + +void GetOptionCommand::toStream(std::ostream& out) const { + out << "GetOption(" << d_flag << ")"; +} + +/* output stream insertion operator for benchmark statuses */ +std::ostream& operator<<(std::ostream& out, + BenchmarkStatus status) { + switch(status) { + + case SMT_SATISFIABLE: + return out << "sat"; + + case SMT_UNSATISFIABLE: + return out << "unsat"; + + case SMT_UNKNOWN: + return out << "unknown"; + + default: + return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]"; + } } }/* CVC4 namespace */ |