diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-27 12:47:19 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-27 12:47:19 -0400 |
commit | cf022026fef28986666c0b5cd80944aa8a239280 (patch) | |
tree | 32af653cee206faa66ca1fb12509017de1c21bce | |
parent | 6eddd9d5206ac65bee665dc6acf629d42bc95036 (diff) | |
parent | 892dd18267c137f7797a4c97f7068b587cbf8c3a (diff) |
Merge branch '1.4.x'
-rw-r--r-- | src/theory/bv/options | 11 | ||||
-rw-r--r-- | src/theory/bv/options_handlers.h | 16 |
2 files changed, 20 insertions, 7 deletions
diff --git a/src/theory/bv/options b/src/theory/bv/options index a9c3b0f08..775a46088 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -12,13 +12,12 @@ option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :han # 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 diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h index c917aa9dd..a7a7101d2 100644 --- a/src/theory/bv/options_handlers.h +++ b/src/theory/bv/options_handlers.h @@ -46,7 +46,6 @@ inline void abcEnabledBuild(std::string option, std::string value, SmtEngine* sm #endif /* CVC4_USE_ABC */ } - static const std::string bitblastingModeHelp = "\ Bit-blasting modes currently supported by the --bitblast option:\n\ \n\ @@ -139,6 +138,21 @@ inline BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, } } +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 */ |