diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-15 22:41:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-15 22:41:03 +0000 |
commit | c00efa92e9d61d808a8346e1d8bb3523e24d8ee2 (patch) | |
tree | 85ecfd0e8770ef539f36ec04afd34a583e75cf38 /src/smt/options_handlers.h | |
parent | c09fae89b38b525c6e2ab1691be4363d0cb1157b (diff) |
minor interface improvements, compliance fixes
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/smt/options_handlers.h')
-rw-r--r-- | src/smt/options_handlers.h | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index fb6cd84d8..2c20e06bb 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -23,6 +23,8 @@ #include "cvc4autoconfig.h" #include "util/dump.h" +#include "smt/modal_exception.h" +#include "smt/smt_engine.h" #include <cerrno> #include <cstring> @@ -255,6 +257,32 @@ inline ModelFormatMode stringToModelFormatMode(std::string option, std::string o } } +// ensure we haven't started search yet +inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) { + if(smt != NULL && smt->d_fullyInited) { + std::stringstream ss; + ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)"; + throw ModalException(ss.str()); + } +} + +// ensure we are a proof-enabled build of CVC4 +inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) { +#ifndef CVC4_PROOF + if(value) { + std::stringstream ss; + ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_PROOF */ +} + +inline void unsatCoresEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) { + if(value) { + throw OptionException("CVC4 does not yet have support for unsatisfiable cores"); + } +} + // 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) \ |