diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 09:27:55 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-20 16:54:27 -0400 |
| commit | dee8aad2f6e54738ad26266618ae71d98e31aa54 (patch) | |
| tree | 851559c93f28fbe0e92e3c151f022234f7a9dbd7 | |
| parent | 1edf48b7b2377603f066335a2d8d087cd803a152 (diff) | |
A couple of fixes to the get-option command for compliance with SMT-LIB.
Thanks to David Cok for reporting this issue.
| -rw-r--r-- | src/expr/command.cpp | 6 | ||||
| -rwxr-xr-x | src/options/mkoptions | 31 |
2 files changed, 31 insertions, 6 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 3a88a6cba..593f84ced 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1228,11 +1228,9 @@ std::string GetOptionCommand::getFlag() const throw() { void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() { try { - vector<SExpr> v; - v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); - v.push_back(smtEngine->getOption(d_flag)); + SExpr res = smtEngine->getOption(d_flag); stringstream ss; - ss << SExpr(v); + ss << res; d_result = ss.str(); d_commandStatus = CommandSuccess::instance(); } catch(UnrecognizedOptionException&) { diff --git a/src/options/mkoptions b/src/options/mkoptions index fa6c4c260..2e152ee07 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -666,13 +666,40 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options if [ -n "$smtname" ]; then if [ "$internal" != - ]; then - smt_getoption_handlers="${smt_getoption_handlers} + case "$type" in + bool) smt_getoption_handlers="${smt_getoption_handlers} +#line $lineno \"$kf\" + if(key == \"$smtname\") { +#line $lineno \"$kf\" + return SExprKeyword(options::$internal() ? \"true\" : \"false\"); + }";; + int|unsigned|int*_t|uint*_t|CVC4::Integer) smt_getoption_handlers="${smt_getoption_handlers} +#line $lineno \"$kf\" + if(key == \"$smtname\") { +#line $lineno \"$kf\" + return SExpr(Integer(options::$internal())); + }";; + float|double) smt_getoption_handlers="${smt_getoption_handlers} +#line $lineno \"$kf\" + if(key == \"$smtname\") { +#line $lineno \"$kf\" + stringstream ss; ss << std::fixed << options::$internal(); + return SExpr(Rational::fromDecimal(ss.str())); + }";; + CVC4::Rational) smt_getoption_handlers="${smt_getoption_handlers} +#line $lineno \"$kf\" + if(key == \"$smtname\") { +#line $lineno \"$kf\" + return SExpr(options::$internal()); + }";; + *) smt_getoption_handlers="${smt_getoption_handlers} #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" stringstream ss; ss << options::$internal(); return SExpr(ss.str()); - }" + }";; + esac fi if [ "$type" = bool ]; then |