minor interface improvements, compliance fixes

(this commit was certified error- and warning-free by the test-and-commit script.)

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) \