Merge branch 'master' of https://github.com/CVC4/CVC4

2 files changed, 24 insertions, 2 deletions

diff --git a/src/theory/bv/options b/src/theory/bv/options
index 462ed47e9..fc704a71a 100644
--- 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 bc01d4dc8..5d85a1be0 100644
--- 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