diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-11-08 23:15:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-11-08 23:15:08 +0000 |
commit | 438e4336569f90adcb8c994df54bc410f56cde07 (patch) | |
tree | ab8d108445c362b017a30553bb7fcfbe84dbe305 /src/expr | |
parent | 15171a8c15cde42914a47f0d1b8bad5ebd6be6e6 (diff) |
cleanup, documentation, SMT-LIBv2 compliance
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 26 | ||||
-rw-r--r-- | src/expr/command.h | 2 |
2 files changed, 26 insertions, 2 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 60b48542b..b17e98b38 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -20,11 +20,13 @@ #include <vector> #include <utility> #include <iterator> +#include <sstream> #include "expr/command.h" #include "smt/smt_engine.h" #include "smt/bad_option_exception.h" #include "util/output.h" +#include "util/sexpr.h" using namespace std; @@ -337,7 +339,18 @@ SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : } void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) { - // FIXME: TODO: something to be done with the status + stringstream ss; + ss << d_status; + SExpr status = ss.str(); + try { + smtEngine->setInfo(":status", status); + //d_result = "success"; + } catch(ModalException& m) { + d_result = "error"; + } catch(BadOptionException& bo) { + // should not happen + d_result = "error"; + } } void SetBenchmarkStatusCommand::toStream(std::ostream& out) const { @@ -351,7 +364,12 @@ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) : } void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) { - // FIXME: TODO: something to be done with the logic + try { + smtEngine->setLogic(d_logic); + //d_result = "success"; + } catch(ModalException& m) { + d_result = "error"; + } } void SetBenchmarkLogicCommand::toStream(std::ostream& out) const { @@ -369,6 +387,8 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setInfo(d_flag, d_sexpr); //d_result = "success"; + } catch(ModalException& m) { + d_result = "error"; } catch(BadOptionException& bo) { d_result = "unsupported"; } @@ -429,6 +449,8 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setOption(d_flag, d_sexpr); //d_result = "success"; + } catch(ModalException& m) { + d_result = "error"; } catch(BadOptionException& bo) { d_result = "unsupported"; } diff --git a/src/expr/command.h b/src/expr/command.h index 172ddea86..fbb48b6b0 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -196,6 +196,7 @@ public: class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { protected: + std::string d_result; BenchmarkStatus d_status; public: SetBenchmarkStatusCommand(BenchmarkStatus status); @@ -205,6 +206,7 @@ public: class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { protected: + std::string d_result; std::string d_logic; public: SetBenchmarkLogicCommand(std::string logic); |