# Options for eager bit-blasting
-option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild :predicate-include "theory/bv/options_handlers.h" :read-write :link --bitblast=eager :link --bv-aig-simp="balance;drw"
- bitblast by first converting to AIG (only if --bitblast=eager)
+option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild CVC4::theory::bv::setBitblastAig :predicate-include "theory/bv/options_handlers.h" :read-write
+ bitblast by first converting to AIG (implies --bitblast=eager)
+expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :default "" :predicate CVC4::theory::bv::abcEnabledBuild :read-write :link --bitblast-aig :link-smt bitblast-aig
+ abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw")
-expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :default "" :predicate CVC4::theory::bv::abcEnabledBuild :read-write :link --bitblast-aig
- abc command to run AIG simplifications
-
-# Options for lazy bit-blasting
+# Options for lazy bit-blasting
option bitvectorPropagate --bv-propagate bool :default true :read-write :link --bitblast=lazy
use bit-vector propagation in the bit-blaster
#endif /* CVC4_USE_ABC */
}
-
static const std::string bitblastingModeHelp = "\
Bit-blasting modes currently supported by the --bitblast option:\n\
\n\
}
}
+inline void setBitblastAig(std::string option, bool arg, SmtEngine* smt) throw(OptionException) {
+ if(arg) {
+ if(options::bitblastMode.wasSetByUser()) {
+ if(options::bitblastMode() != BITBLAST_MODE_EAGER) {
+ throw OptionException("bitblast-aig must be used with eager bitblaster");
+ }
+ } else {
+ options::bitblastMode.set(stringToBitblastMode("", "eager", smt));
+ }
+ if(!options::bitvectorAigSimplifications.wasSetByUser()) {
+ options::bitvectorAigSimplifications.set("balance;drw");
+ }
+ }
+}
+
}/* CVC4::theory::bv namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */