diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-14 17:42:47 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-14 17:42:47 +0000 |
commit | 4c956f292906c59ba77c000084a08a4e7888e49b (patch) | |
tree | b068a48c9fc8579eb078432ad6335b48e9a820d6 /src/smt | |
parent | 69693d7c8e5ca84b76fa807cb0797823058caa9a (diff) |
some changes to make CVC4 work nicely with trace executor for application track; (set-option :print-success true) supported, (exit) causes immediate exit regardless of EOF, etc.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 91c43a1de..5e51900a9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -650,6 +650,9 @@ SExpr SmtEngine::getInfo(const std::string& key) const void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOptionException, ModalException) { + + NodeManagerScope nms(d_nodeManager); + Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; if(Dump.isOn("benchmark")) { Dump("benchmark") << SetOptionCommand(key, value); @@ -657,7 +660,9 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value) if(key == ":print-success") { if(value.isAtom() && value.getValue() == "false") { - // fine; don't need to do anything + *Options::current()->out << Command::printsuccess(false); + } else if(value.isAtom() && value.getValue() == "true") { + *Options::current()->out << Command::printsuccess(true); } else { throw BadOptionException(); } @@ -696,12 +701,19 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value) SExpr SmtEngine::getOption(const std::string& key) const throw(BadOptionException) { + + NodeManagerScope nms(d_nodeManager); + Trace("smt") << "SMT getOption(" << key << ")" << endl; if(Dump.isOn("benchmark")) { Dump("benchmark") << GetOptionCommand(key); } if(key == ":print-success") { - return SExpr("true"); + if(Command::printsuccess::getPrintSuccess(*Options::current()->out)) { + return SExpr("true"); + } else { + return SExpr("false"); + } } else if(key == ":expand-definitions") { throw BadOptionException(); } else if(key == ":interactive-mode") { |