diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-15 22:41:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-15 22:41:03 +0000 |
commit | c00efa92e9d61d808a8346e1d8bb3523e24d8ee2 (patch) | |
tree | 85ecfd0e8770ef539f36ec04afd34a583e75cf38 /src/expr | |
parent | c09fae89b38b525c6e2ab1691be4363d0cb1157b (diff) |
minor interface improvements, compliance fixes
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 86 | ||||
-rw-r--r-- | src/expr/command.h | 27 |
2 files changed, 111 insertions, 2 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 1e4a266a5..53ca266f4 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -26,6 +26,8 @@ #include "expr/command.h" #include "smt/smt_engine.h" #include "options/options.h" +#include "smt/options.h" +#include "smt/smt_engine_scope.h" #include "util/output.h" #include "util/dump.h" #include "util/sexpr.h" @@ -691,7 +693,7 @@ Command* SetUserAttributeCommand::clone() const{ return new SetUserAttributeCommand( d_attr, d_expr ); } -/* class Simplify */ +/* class SimplifyCommand */ SimplifyCommand::SimplifyCommand(Expr term) throw() : d_term(term) { @@ -730,6 +732,45 @@ Command* SimplifyCommand::clone() const { return c; } +/* class ExpandDefinitionsCommand */ + +ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() : + d_term(term) { +} + +Expr ExpandDefinitionsCommand::getTerm() const throw() { + return d_term; +} + +void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() { + d_result = smtEngine->expandDefinitions(d_term); + d_commandStatus = CommandSuccess::instance(); +} + +Expr ExpandDefinitionsCommand::getResult() const throw() { + return d_result; +} + +void ExpandDefinitionsCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } +} + +Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap)); + c->d_result = d_result.exportTo(exprManager, variableMap); + return c; +} + +Command* ExpandDefinitionsCommand::clone() const { + ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term); + c->d_result = d_result; + return c; +} + /* class GetValueCommand */ GetValueCommand::GetValueCommand(Expr term) throw() : @@ -752,7 +793,10 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { NodeManager* nm = NodeManager::fromExprManager(smtEngine->getExprManager()); for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { Assert(nm == NodeManager::fromExprManager((*i).getExprManager())); - result.push_back(nm->mkNode(kind::TUPLE, Node::fromExpr(*i), Node::fromExpr(smtEngine->getValue(*i)))); + smt::SmtScope scope(smtEngine); + Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i); + Node value = Node::fromExpr(smtEngine->getValue(*i)); + result.push_back(nm->mkNode(kind::TUPLE, request, value)); } Node n = nm->mkNode(kind::TUPLE, result); d_result = nm->toExpr(n); @@ -908,6 +952,44 @@ Command* GetProofCommand::clone() const { return c; } +/* class GetUnsatCoreCommand */ + +GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { +} + +void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() { + /* + try { + d_result = smtEngine->getUnsatCore(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } + */ + d_commandStatus = new CommandFailure("unsat cores not supported yet"); +} + +void GetUnsatCoreCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + //do nothing -- unsat cores not yet supported + // d_result->toStream(out); + } +} + +Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); + //c->d_result = d_result; + return c; +} + +Command* GetUnsatCoreCommand::clone() const { + GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); + //c->d_result = d_result; + return c; +} + /* class GetAssertionsCommand */ GetAssertionsCommand::GetAssertionsCommand() throw() { diff --git a/src/expr/command.h b/src/expr/command.h index 70e71a111..5786f4e71 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -475,6 +475,21 @@ public: Command* clone() const; };/* class SimplifyCommand */ +class CVC4_PUBLIC ExpandDefinitionsCommand : public Command { +protected: + Expr d_term; + Expr d_result; +public: + ExpandDefinitionsCommand(Expr term) throw(); + ~ExpandDefinitionsCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; +};/* class ExpandDefinitionsCommand */ + class CVC4_PUBLIC GetValueCommand : public Command { protected: std::vector<Expr> d_terms; @@ -531,6 +546,18 @@ public: Command* clone() const; };/* class GetProofCommand */ +class CVC4_PUBLIC GetUnsatCoreCommand : public Command { +protected: + //UnsatCore* d_result; +public: + GetUnsatCoreCommand() throw(); + ~GetUnsatCoreCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; +};/* class GetUnsatCoreCommand */ + class CVC4_PUBLIC GetAssertionsCommand : public Command { protected: std::string d_result; |