added optionException for trying to use abc in an non-abc build

diff --git a/src/theory/bv/options b/src/theory/bv/options
index 462ed47e9e2542d482540e6c453a2244b993a99b..fc704a71a7f849a8d9cca021239589e8945e360e 100644 (file)
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -12,10 +12,10 @@ option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :han
 
 # Options for eager bit-blasting
  
-option bitvectorAig --bitblast-aig bool :default false :read-write :link --bitblast=eager
+option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild :predicate-include "theory/bv/options_handlers.h" :read-write :link --bitblast=eager
  bitblast by first converting to AIG (only if --bitblast=eager)
 
-expert-option bitvectorAigSimplifications --bv-aig-simp=FILE std::string :default "" :read-write :link --bitblast-aig
+expert-option bitvectorAigSimplifications --bv-aig-simp=FILE std::string :default "" :predicate CVC4::theory::bv::abcEnabledBuild :read-write :link --bitblast-aig
  abc command to run AIG simplifications
 
 # Options for lazy bit-blasting  

diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h
index bc01d4dc8e5f8cd14d7df533c11c439cf808708a..5d85a1be0411c52f40444840c5694ef0fa92a7ed 100644 (file)
--- a/src/theory/bv/options_handlers.h
+++ b/src/theory/bv/options_handlers.h
@@ -26,6 +26,27 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
+inline void abcEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
+#ifndef CVC4_USE_ABC
+  if(value) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
+    throw OptionException(ss.str());
+  }
+#endif /* CVC4_USE_ABC */
+}
+
+inline void abcEnabledBuild(std::string option, std::string value, SmtEngine* smt) throw(OptionException) {
+#ifndef CVC4_USE_ABC
+  if(!value.empty()) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
+    throw OptionException(ss.str());
+  }
+#endif /* CVC4_USE_ABC */
+}
+
+
 static const std::string bitblastingModeHelp = "\
 Bit-blasting modes currently supported by the --bitblast option:\n\
 \n\
@@ -77,6 +98,7 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg,
     
     if (!options::bitvectorAig.wasSetByUser()) {
       options::bitvectorAig.set(true);
+      abcEnabledBuild("--bitblast-aig", true, NULL); 
     }
     if (!options::bitvectorAigSimplifications.wasSetByUser()) {
       // due to a known bug in abc switching to using drw instead of rw