summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--configure.ac3
-rw-r--r--src/cvc4.i4
-rw-r--r--src/expr/command.cpp10
-rw-r--r--src/main/options3
-rw-r--r--src/options/Makefile.am4
-rwxr-xr-xsrc/options/mkoptions4
-rw-r--r--src/options/option_exception.h58
-rw-r--r--src/options/option_exception.i5
-rw-r--r--src/options/options.h10
-rw-r--r--src/smt/Makefile.am2
-rw-r--r--src/smt/bad_option_exception.h48
-rw-r--r--src/smt/bad_option_exception.i7
-rw-r--r--src/smt/options5
-rw-r--r--src/smt/options_handlers.h146
-rw-r--r--src/smt/smt_engine.cpp16
-rw-r--r--src/smt/smt_engine.h9
-rw-r--r--src/smt/smt_options_template.cpp15
17 files changed, 230 insertions, 119 deletions
diff --git a/configure.ac b/configure.ac
index 6820b2bb4..0e98152be 100644
--- a/configure.ac
+++ b/configure.ac
@@ -862,6 +862,9 @@ AC_CHECK_HEADERS([getopt.h unistd.h])
AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
+# check with which standard strerror_r() complies
+AC_FUNC_STRERROR_R
+
# require boost library
BOOST_REQUIRE()
diff --git a/src/cvc4.i b/src/cvc4.i
index cddd3891c..08b2c509f 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -117,8 +117,10 @@ using namespace CVC4;
%include "expr/expr_stream.i"
%include "smt/smt_engine.i"
-%include "smt/bad_option_exception.i"
%include "smt/no_such_function_exception.i"
%include "smt/modal_exception.i"
+%include "options/options.i"
+%include "options/option_exception.i"
+
%include "parser/cvc4parser.i"
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 576707fca..7f10c533e 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -25,7 +25,7 @@
#include "expr/command.h"
#include "smt/smt_engine.h"
-#include "smt/bad_option_exception.h"
+#include "options/options.h"
#include "util/output.h"
#include "util/dump.h"
#include "util/sexpr.h"
@@ -963,7 +963,7 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
try {
smtEngine->setInfo(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
- } catch(BadOptionException&) {
+ } catch(UnrecognizedOptionException&) {
d_commandStatus = new CommandUnsupported();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
@@ -997,7 +997,7 @@ void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
<< response;
d_result = ss.str();
d_commandStatus = CommandSuccess::instance();
- } catch(BadOptionException&) {
+ } catch(UnrecognizedOptionException&) {
d_commandStatus = new CommandUnsupported();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
@@ -1047,7 +1047,7 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
try {
smtEngine->setOption(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
- } catch(BadOptionException&) {
+ } catch(UnrecognizedOptionException&) {
d_commandStatus = new CommandUnsupported();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
@@ -1082,7 +1082,7 @@ void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
ss << SExpr(v);
d_result = ss.str();
d_commandStatus = CommandSuccess::instance();
- } catch(BadOptionException&) {
+ } catch(UnrecognizedOptionException&) {
d_commandStatus = new CommandUnsupported();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
diff --git a/src/main/options b/src/main/options
index 6defc8642..47e397d11 100644
--- a/src/main/options
+++ b/src/main/options
@@ -30,8 +30,7 @@ option threadArgv std::vector<std::string>
option thread_id int :default -1
Thread ID, for internal use in case of multi-threaded run
option separateOutput bool :default false
- In multi-threaded setting print output of each thread at the
- end of run, separated by a divider ("----").
+ In multi-threaded setting print output of each thread at the end of run, separated by a divider ("----").
option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
don't share lemmas strictly longer than N
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 2db54a4d9..e1cd721f3 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -28,7 +28,8 @@ noinst_LTLIBRARIES = liboptions.la
liboptions_la_SOURCES = \
options.h \
- base_options_handlers.h
+ base_options_handlers.h \
+ option_exception.h
nodist_liboptions_la_SOURCES = \
options.cpp \
@@ -60,6 +61,7 @@ EXTRA_DIST = \
options_template.cpp \
options_holder_template.h \
options.i \
+ option_exception.i \
$(OPTIONS_FILES:%=../%)
if CVC4_DEBUG
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 2bfd6a2d9..a551d5bd9 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -649,7 +649,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
for handler in $handlers; do
run_handlers="$run_handlers
#line $lineno \"$kf\"
- $handler(\"$smtname\", value, smt);
+ $handler(\"$smtname\", optarg, smt);
"
done
fi
@@ -665,7 +665,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
for handler in $handlers; do
run_handlers="$run_handlers
#line $lineno \"$kf\"
- $handler(\"$smtname\", value, smt);
+ $handler(\"$smtname\", optarg, smt);
"
done
smt_setoption_handlers="${smt_setoption_handlers}
diff --git a/src/options/option_exception.h b/src/options/option_exception.h
new file mode 100644
index 000000000..657bc7568
--- /dev/null
+++ b/src/options/option_exception.h
@@ -0,0 +1,58 @@
+/********************* */
+/*! \file option_exception.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: taking, cconway
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Options-related exceptions
+ **
+ ** Options-related exceptions.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__OPTION_EXCEPTION_H
+#define __CVC4__OPTION_EXCEPTION_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+
+/**
+ * Class representing an option-parsing exception such as badly-typed
+ * or missing arguments, arguments out of bounds, etc. If an option
+ * name is itself unrecognized, a UnrecognizedOptionException (a derived
+ * class, below) should be used instead.
+ */
+class CVC4_PUBLIC OptionException : public CVC4::Exception {
+public:
+ OptionException(const std::string& s) throw() :
+ CVC4::Exception("Error in option parsing: " + s) {
+ }
+};/* class OptionException */
+
+/**
+ * Class representing an exception in option processing due to an
+ * unrecognized or unsupported option key.
+ */
+class CVC4_PUBLIC UnrecognizedOptionException : public CVC4::OptionException {
+public:
+ UnrecognizedOptionException() :
+ CVC4::OptionException("Unrecognized informational or option key or setting") {
+ }
+
+ UnrecognizedOptionException(const std::string& msg) :
+ CVC4::OptionException(msg) {
+ }
+};/* class UnrecognizedOptionException */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OPTION_EXCEPTION_H */
diff --git a/src/options/option_exception.i b/src/options/option_exception.i
new file mode 100644
index 000000000..ae68d4e0f
--- /dev/null
+++ b/src/options/option_exception.i
@@ -0,0 +1,5 @@
+%{
+#include "options/option_exception.h"
+%}
+
+%include "options/option_exception.h"
diff --git a/src/options/options.h b/src/options/options.h
index a3abdd54b..c966670f5 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -25,7 +25,7 @@
#include <fstream>
#include <string>
-#include "util/exception.h"
+#include "options/option_exception.h"
#include "util/language.h"
#include "util/tls.h"
@@ -40,14 +40,6 @@ class NodeManager;
class NodeManagerScope;
class SmtEngine;
-/** Class representing an option-parsing exception. */
-class CVC4_PUBLIC OptionException : public CVC4::Exception {
-public:
- OptionException(const std::string& s) throw() :
- CVC4::Exception("Error in option parsing: " + s) {
- }
-};/* class OptionException */
-
class CVC4_PUBLIC Options {
/** The struct that holds all option values. */
options::OptionsHolder* d_holder;
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 9cc236a13..76cebbdd1 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -11,7 +11,6 @@ libsmt_la_SOURCES = \
smt_engine_scope.cpp \
smt_engine_scope.h \
modal_exception.h \
- bad_option_exception.h \
no_such_function_exception.h \
simplification_mode.h \
simplification_mode.cpp
@@ -22,7 +21,6 @@ nodist_libsmt_la_SOURCES = \
EXTRA_DIST = \
options_handlers.h \
smt_options_template.cpp \
- bad_option_exception.i \
no_such_function_exception.i \
modal_exception.i \
smt_engine.i
diff --git a/src/smt/bad_option_exception.h b/src/smt/bad_option_exception.h
deleted file mode 100644
index 8fafb952e..000000000
--- a/src/smt/bad_option_exception.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/********************* */
-/*! \file bad_option_exception.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief An exception that is thrown when an option setting is not
- ** understood.
- **
- ** An exception that is thrown when an interactive-only feature while
- ** CVC4 is being used in a non-interactive setting (for example, the
- ** "(get-assertions)" command in an SMT-LIBv2 script).
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__SMT__BAD_OPTION_EXCEPTION_H
-#define __CVC4__SMT__BAD_OPTION_EXCEPTION_H
-
-#include "util/exception.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC BadOptionException : public CVC4::Exception {
-public:
- BadOptionException() :
- Exception("Unrecognized informational or option key or setting") {
- }
-
- BadOptionException(const std::string& msg) :
- Exception(msg) {
- }
-
- BadOptionException(const char* msg) :
- Exception(msg) {
- }
-};/* class BadOptionException */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__BAD_OPTION_EXCEPTION_H */
diff --git a/src/smt/bad_option_exception.i b/src/smt/bad_option_exception.i
deleted file mode 100644
index eeded5a45..000000000
--- a/src/smt/bad_option_exception.i
+++ /dev/null
@@ -1,7 +0,0 @@
-%{
-#include "smt/bad_option_exception.h"
-%}
-
-%ignore CVC4::BadOptionException::BadOptionException(const char*);
-
-%include "smt/bad_option_exception.h"
diff --git a/src/smt/options b/src/smt/options
index 5ee65e50a..13b3b51f3 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -55,6 +55,11 @@ option repeatSimp --repeat-simp bool :read-write
common-option incrementalSolving incremental -i --incremental bool
enable incremental solving
+option - regular-output-channel argument :handler CVC4::smt::setRegularOutputChannel :handler-include "smt/options_handlers.h"
+ set the regular output channel of the solver
+option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h"
+ set the diagnostic output channel of the solver
+
common-option cumulativeMillisecondLimit --tlimit=MS "unsigned long"
enable time limiting (give milliseconds)
common-option perCallMillisecondLimit --tlimit-per=MS "unsigned long"
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index f111f512b..925f86d48 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -21,11 +21,47 @@
#ifndef __CVC4__SMT__OPTIONS_HANDLERS_H
#define __CVC4__SMT__OPTIONS_HANDLERS_H
+#include "cvc4autoconfig.h"
#include "util/dump.h"
+#include <cerrno>
+#include <cstring>
+#include <sstream>
+
namespace CVC4 {
namespace smt {
+static inline std::string __cvc4_errno_failreason() {
+#if HAVE_STRERROR_R
+#if STRERROR_R_CHAR_P
+ if(errno != 0) {
+ // GNU version of strerror_r: *might* use the given buffer,
+ // or might not. It returns a pointer to buf, or not.
+ char buf[80];
+ return std::string(strerror_r(errno, buf, sizeof buf));
+ } else {
+ return "unknown reason";
+ }
+#else /* STRERROR_R_CHAR_P */
+ if(errno != 0) {
+ // XSI version of strerror_r: always uses the given buffer.
+ // Returns an error code.
+ char buf[80];
+ if(strerror_r(errno, buf, sizeof buf) == 0) {
+ return std::string(buf);
+ } else {
+ // some error occurred while getting the error string
+ return "unknown reason";
+ }
+ } else {
+ return "unknown reason";
+ }
+#endif /* STRERROR_R_CHAR_P */
+#else /* HAVE_STRERROR_R */
+ return "unknown reason";
+#endif /* HAVE_STRERROR_R */
+}
+
static const std::string dumpHelp = "\
Dump modes currently supported by the --dump option:\n\
\n\
@@ -179,42 +215,107 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
#endif /* CVC4_DUMPING */
}
+inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ if(optarg == "batch") {
+ return SIMPLIFICATION_MODE_BATCH;
+ } else if(optarg == "incremental") {
+ return SIMPLIFICATION_MODE_INCREMENTAL;
+ } else if(optarg == "none") {
+ return SIMPLIFICATION_MODE_NONE;
+ } else if(optarg == "help") {
+ puts(simplificationHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --simplification: `") +
+ optarg + "'. Try --simplification help.");
+ }
+}
+
+// This macro is used for setting :regular-output-channel and :diagnostic-output-channel
+// to redirect a stream. It maintains all attributes set on the stream.
+#define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \
+ { \
+ int dagSetting = expr::ExprDag::getDag(__channel_get); \
+ size_t exprDepthSetting = expr::ExprSetDepth::getDepth(__channel_get); \
+ bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \
+ OutputLanguage languageSetting = expr::ExprSetLanguage::getLanguage(__channel_get); \
+ __channel_set; \
+ __channel_get << Expr::dag(dagSetting); \
+ __channel_get << Expr::setdepth(exprDepthSetting); \
+ __channel_get << Expr::printtypes(printtypesSetting); \
+ __channel_get << Expr::setlanguage(languageSetting); \
+ }
+
inline void dumpToFile(std::string option, std::string optarg, SmtEngine* smt) {
#ifdef CVC4_DUMPING
- size_t dagSetting = expr::ExprDag::getDag(Dump.getStream());
+ std::ostream* outStream = NULL;
if(optarg == "") {
throw OptionException(std::string("Bad file name for --dump-to"));
} else if(optarg == "-") {
- Dump.setStream(DumpOutC::dump_cout);
+ outStream = &DumpOutC::dump_cout;
} else {
- std::ostream* dumpTo = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
- if(!*dumpTo) {
- throw OptionException(std::string("Cannot open dump-to file (maybe it exists): `") + optarg + "'");
+ errno = 0;
+ outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+ if(outStream == NULL || !*outStream) {
+ std::stringstream ss;
+ ss << "Cannot open dump-to file: `" << optarg << "': " << __cvc4_errno_failreason();
+ throw OptionException(ss.str());
}
- Dump.setStream(*dumpTo);
}
- expr::ExprDag::setDag(Dump.getStream(), dagSetting);
+ __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Dump.getStream(), Dump.setStream(*outStream));
#else /* CVC4_DUMPING */
throw OptionException("The dumping feature was disabled in this build of CVC4.");
#endif /* CVC4_DUMPING */
}
-inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
- if(optarg == "batch") {
- return SIMPLIFICATION_MODE_BATCH;
- } else if(optarg == "incremental") {
- return SIMPLIFICATION_MODE_INCREMENTAL;
- } else if(optarg == "none") {
- return SIMPLIFICATION_MODE_NONE;
- } else if(optarg == "help") {
- puts(simplificationHelp.c_str());
- exit(1);
+inline void setRegularOutputChannel(std::string option, std::string optarg, SmtEngine* smt) {
+ std::ostream* outStream = NULL;
+ if(optarg == "") {
+ throw OptionException(std::string("Bad file name setting for regular output channel"));
+ } else if(optarg == "stdout") {
+ outStream = &std::cout;
+ } else if(optarg == "stderr") {
+ outStream = &std::cerr;
} else {
- throw OptionException(std::string("unknown option for --simplification: `") +
- optarg + "'. Try --simplification help.");
+ errno = 0;
+ outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+ if(outStream == NULL || !*outStream) {
+ std::stringstream ss;
+ ss << "Cannot open regular-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason();
+ throw OptionException(ss.str());
+ }
+ }
+ __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream));
+}
+
+inline void setDiagnosticOutputChannel(std::string option, std::string optarg, SmtEngine* smt) {
+ std::ostream* outStream = NULL;
+ if(optarg == "") {
+ throw OptionException(std::string("Bad file name setting for diagnostic output channel"));
+ } else if(optarg == "stdout") {
+ outStream = &std::cout;
+ } else if(optarg == "stderr") {
+ outStream = &std::cerr;
+ } else {
+ errno = 0;
+ outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+ if(outStream == NULL || !*outStream) {
+ std::stringstream ss;
+ ss << "Cannot open diagnostic-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason();
+ throw OptionException(ss.str());
+ }
}
+ __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Debug.getStream(), Debug.setStream(*outStream));
+ __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Warning.getStream(), Warning.setStream(*outStream));
+ __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Message.getStream(), Message.setStream(*outStream));
+ __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Notice.getStream(), Notice.setStream(*outStream));
+ __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Chat.getStream(), Chat.setStream(*outStream));
+ __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Trace.getStream(), Trace.setStream(*outStream));
+ __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream));
}
+#undef __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM
+
inline std::string checkReplayFilename(std::string option, std::string optarg, SmtEngine* smt) {
#ifdef CVC4_REPLAY
if(optarg == "") {
@@ -234,9 +335,12 @@ inline std::ostream* checkReplayLogFilename(std::string option, std::string opta
} else if(optarg == "-") {
return &std::cout;
} else {
+ errno = 0;
std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
- if(!*replayLog) {
- throw OptionException(std::string("Cannot open replay-log file: `") + optarg + "'");
+ if(replayLog == NULL || !*replayLog) {
+ std::stringstream ss;
+ ss << "Cannot open replay-log file: `" << optarg << "': " << __cvc4_errno_failreason();
+ throw OptionException(ss.str());
}
return replayLog;
}
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6b7ca8d2f..de5971306 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -38,7 +38,6 @@
#include "expr/metakind.h"
#include "expr/node_builder.h"
#include "prop/prop_engine.h"
-#include "smt/bad_option_exception.h"
#include "smt/modal_exception.h"
#include "smt/no_such_function_exception.h"
#include "smt/smt_engine.h"
@@ -50,6 +49,7 @@
#include "util/configuration.h"
#include "util/exception.h"
#include "smt/options.h"
+#include "options/option_exception.h"
#include "util/output.h"
#include "util/hash.h"
#include "theory/substitutions.h"
@@ -607,7 +607,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
}
void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
- throw(BadOptionException, ModalException) {
+ throw(OptionException, ModalException) {
SmtScope smts(this);
@@ -631,7 +631,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
string cvc4key = key.substr(6);
if(cvc4key == "logic") {
if(! value.isAtom()) {
- throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string");
+ throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
}
SmtScope smts(this);
d_logic = value.getValue();
@@ -656,17 +656,17 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
s = value.getValue();
}
if(s != "sat" && s != "unsat" && s != "unknown") {
- throw BadOptionException("argument to (set-info :status ..) must be "
- "`sat' or `unsat' or `unknown'");
+ throw OptionException("argument to (set-info :status ..) must be "
+ "`sat' or `unsat' or `unknown'");
}
d_status = Result(s);
return;
}
- throw BadOptionException();
+ throw UnrecognizedOptionException();
}
CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
- throw(BadOptionException, ModalException) {
+ throw(OptionException, ModalException) {
SmtScope smts(this);
@@ -721,7 +721,7 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
"last result wasn't unknown!");
}
} else {
- throw BadOptionException();
+ throw UnrecognizedOptionException();
}
}
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 52a2e0c27..505a2d8d8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -30,7 +30,6 @@
#include "expr/expr_manager.h"
#include "util/proof.h"
#include "util/model.h"
-#include "smt/bad_option_exception.h"
#include "smt/modal_exception.h"
#include "smt/no_such_function_exception.h"
#include "util/hash.h"
@@ -303,25 +302,25 @@ public:
* Set information about the script executing.
*/
void setInfo(const std::string& key, const CVC4::SExpr& value)
- throw(BadOptionException, ModalException);
+ throw(OptionException, ModalException);
/**
* Query information about the SMT environment.
*/
CVC4::SExpr getInfo(const std::string& key) const
- throw(BadOptionException, ModalException);
+ throw(OptionException, ModalException);
/**
* Set an aspect of the current SMT execution environment.
*/
void setOption(const std::string& key, const CVC4::SExpr& value)
- throw(BadOptionException, ModalException);
+ throw(OptionException, ModalException);
/**
* Get an aspect of the current SMT execution environment.
*/
CVC4::SExpr getOption(const std::string& key) const
- throw(BadOptionException);
+ throw(OptionException);
/**
* Add a formula to the current context: preprocess, do per-theory
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index f34a0e2db..b254a3b30 100644
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -17,7 +17,6 @@
**/
#include "smt/smt_engine.h"
-#include "smt/bad_option_exception.h"
#include "smt/modal_exception.h"
#include "util/sexpr.h"
#include "util/dump.h"
@@ -30,14 +29,14 @@
${include_all_option_headers}
${option_handler_includes}
-#line 34 "${template}"
+#line 33 "${template}"
using namespace std;
namespace CVC4 {
void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
- throw(BadOptionException, ModalException) {
+ throw(OptionException, ModalException) {
NodeManagerScope nms(d_nodeManager);
SmtEngine* const smt = this;
@@ -51,13 +50,13 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
${smt_setoption_handlers}
-#line 55 "${template}"
+#line 54 "${template}"
- throw BadOptionException();
+ throw UnrecognizedOptionException();
}
CVC4::SExpr SmtEngine::getOption(const std::string& key) const
- throw(BadOptionException) {
+ throw(OptionException) {
NodeManagerScope nms(d_nodeManager);
@@ -68,9 +67,9 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
${smt_getoption_handlers}
-#line 72 "${template}"
+#line 71 "${template}"
- throw BadOptionException();
+ throw UnrecognizedOptionException();
}
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback