Also some cleanup of option-related exceptions infrastructure.
AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
+# check with which standard strerror_r() complies
+AC_FUNC_STRERROR_R
+
# require boost library
BOOST_REQUIRE()
%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"
#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"
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());
<< 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());
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());
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());
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
liboptions_la_SOURCES = \
options.h \
- base_options_handlers.h
+ base_options_handlers.h \
+ option_exception.h
nodist_liboptions_la_SOURCES = \
options.cpp \
options_template.cpp \
options_holder_template.h \
options.i \
+ option_exception.i \
$(OPTIONS_FILES:%=../%)
if CVC4_DEBUG
for handler in $handlers; do
run_handlers="$run_handlers
#line $lineno \"$kf\"
- $handler(\"$smtname\", value, smt);
+ $handler(\"$smtname\", optarg, smt);
"
done
fi
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}
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+%{
+#include "options/option_exception.h"
+%}
+
+%include "options/option_exception.h"
#include <fstream>
#include <string>
-#include "util/exception.h"
+#include "options/option_exception.h"
#include "util/language.h"
#include "util/tls.h"
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;
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
EXTRA_DIST = \
options_handlers.h \
smt_options_template.cpp \
- bad_option_exception.i \
no_such_function_exception.i \
modal_exception.i \
smt_engine.i
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-%{
-#include "smt/bad_option_exception.h"
-%}
-
-%ignore CVC4::BadOptionException::BadOptionException(const char*);
-
-%include "smt/bad_option_exception.h"
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"
#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\
#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 == "") {
} 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;
}
#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"
#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"
}
void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
- throw(BadOptionException, ModalException) {
+ throw(OptionException, ModalException) {
SmtScope smts(this);
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();
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);
"last result wasn't unknown!");
}
} else {
- throw BadOptionException();
+ throw UnrecognizedOptionException();
}
}
#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"
* 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
**/
#include "smt/smt_engine.h"
-#include "smt/bad_option_exception.h"
#include "smt/modal_exception.h"
#include "util/sexpr.h"
#include "util/dump.h"
${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;
${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);
${smt_getoption_handlers}
-#line 72 "${template}"
+#line 71 "${template}"
- throw BadOptionException();
+ throw UnrecognizedOptionException();
}
}/* CVC4 namespace */
projects / cvc5.git / commitdiff