Support per-command verbosity settings.

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);
 }