diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-04 20:29:24 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-09 17:21:42 -0400 |
commit | b747578dee53489326bf53743cfc4f83c467cbfd (patch) | |
tree | f37bbdcaa1f449a08ebf8172494ad485a735d318 /src/smt/smt_options_template.cpp | |
parent | 42d28850d4f2f4816af24dedf8d1cbd0a0d58b6f (diff) |
Support per-command verbosity settings.
Diffstat (limited to 'src/smt/smt_options_template.cpp')
-rw-r--r-- | src/smt/smt_options_template.cpp | 62 |
1 files changed, 60 insertions, 2 deletions
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp index 638cf2f83..228c18adb 100644 --- a/src/smt/smt_options_template.cpp +++ b/src/smt/smt_options_template.cpp @@ -44,11 +44,29 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) Dump("benchmark") << SetOptionCommand(key, value); } + if(key == "command-verbosity") { + if(!value.isAtom()) { + const vector<SExpr>& cs = value.getChildren(); + if(cs.size() == 2 && + (cs[0].isKeyword() || cs[0].isString()) && + cs[1].isInteger()) { + string c = cs[0].getValue(); + const Integer& v = cs[1].getIntegerValue(); + if(v < 0 || v > 2) { + throw OptionException("command-verbosity must be 0, 1, or 2"); + } + d_commandVerbosity[c] = v; + return; + } + } + throw OptionException("command-verbosity value must be a tuple (command-name, integer)"); + } + string optionarg = value.getValue(); ${smt_setoption_handlers} -#line 52 "${template}" +#line 70 "${template}" throw UnrecognizedOptionException(key); } @@ -63,9 +81,49 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const Dump("benchmark") << GetOptionCommand(key); } + if(key == "command-verbosity") { + vector<SExpr> result; + SExpr defaultVerbosity; + for(map<string, Integer>::const_iterator i = d_commandVerbosity.begin(); + i != d_commandVerbosity.end(); + ++i) { + vector<SExpr> v; + v.push_back((*i).first); + v.push_back((*i).second); + if((*i).first == "*") { + // put the default at the end of the SExpr + defaultVerbosity = v; + } else { + result.push_back(v); + } + } + // put the default at the end of the SExpr + if(!defaultVerbosity.isAtom()) { + result.push_back(defaultVerbosity); + } else { + // ensure the default is always listed + vector<SExpr> v; + v.push_back("*"); + v.push_back(Integer(2)); + result.push_back(v); + } + return result; + } else if(key.length() >= 18 && + key.compare(0, 18, "command-verbosity:") == 0) { + map<string, Integer>::const_iterator i = d_commandVerbosity.find(key.c_str() + 18); + if(i != d_commandVerbosity.end()) { + return (*i).second; + } + i = d_commandVerbosity.find("*"); + if(i != d_commandVerbosity.end()) { + return (*i).second; + } + return Integer(2); + } + ${smt_getoption_handlers} -#line 69 "${template}" +#line 127 "${template}" throw UnrecognizedOptionException(key); } |