diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-06 22:05:12 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-06 22:05:12 +0000 |
commit | a99a3693b2c69ffd6a4268c9020593f62a3474eb (patch) | |
tree | f71e299b8ba2de95141d5ccfc3a150fd8b1b97b1 /src/smt | |
parent | cc8385b0dbb58419d91e3349a0fd52f6b8452d90 (diff) |
Support setting :regular-output-channel and :diagnostic-output-channel.
Also some cleanup of option-related exceptions infrastructure.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/Makefile.am | 2 | ||||
-rw-r--r-- | src/smt/bad_option_exception.h | 48 | ||||
-rw-r--r-- | src/smt/bad_option_exception.i | 7 | ||||
-rw-r--r-- | src/smt/options | 5 | ||||
-rw-r--r-- | src/smt/options_handlers.h | 146 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 16 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 9 | ||||
-rw-r--r-- | src/smt/smt_options_template.cpp | 15 |
8 files changed, 149 insertions, 99 deletions
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 */ |