diff options
| -rw-r--r-- | src/theory/bv/options | 4 | ||||
| -rw-r--r-- | src/theory/bv/options_handlers.h | 22 |
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 |