diff options
Diffstat (limited to 'src/smt/smt_options_template.cpp')
-rw-r--r-- | src/smt/smt_options_template.cpp | 138 |
1 files changed, 0 insertions, 138 deletions
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp deleted file mode 100644 index 376584636..000000000 --- a/src/smt/smt_options_template.cpp +++ /dev/null @@ -1,138 +0,0 @@ -/********************* */ -/*! \file smt_options_template.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Option handling for SmtEngine - ** - ** Option handling for SmtEngine. - **/ - -#include "smt/smt_engine.h" -#include "smt/modal_exception.h" -#include "util/sexpr.h" -#include "util/dump.h" -#include "expr/command.h" -#include "expr/node_manager.h" - -#include <string> -#include <sstream> - -${include_all_option_headers} -${option_handler_includes} - -#line 31 "${template}" - -using namespace std; - -namespace CVC4 { - -void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) - throw(OptionException, ModalException) { - - NodeManagerScope nms(d_nodeManager); - SmtEngine* const smt = this; - - Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; - if(Dump.isOn("benchmark")) { - 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)"); - } - - if(!value.isAtom()) { - throw OptionException("bad value for :" + key); - } - - string optionarg = value.getValue(); - - ${smt_setoption_handlers} - -#line 74 "${template}" - - throw UnrecognizedOptionException(key); -} - -CVC4::SExpr SmtEngine::getOption(const std::string& key) const - throw(OptionException) { - - NodeManagerScope nms(d_nodeManager); - - Trace("smt") << "SMT getOption(" << key << ")" << endl; - - 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); - } - - if(Dump.isOn("benchmark")) { - 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; - } - - ${smt_getoption_handlers} - -#line 134 "${template}" - - throw UnrecognizedOptionException(key); -} - -}/* CVC4 namespace */ |