Fix infinite loop in --bitblast-aig/--bv-aig-simp options.
authorMorgan Deters <mdeters@cs.nyu.edu>
Sat, 27 Sep 2014 16:47:09 +0000 (12:47 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Sat, 27 Sep 2014 16:47:09 +0000 (12:47 -0400)
src/theory/bv/options
src/theory/bv/options_handlers.h

index a9c3b0f0802259daed75152f9f48d526c9403ede..775a460880a9082d3b9640c44a97150938b08ce7 100644 (file)
@@ -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
index c917aa9ddf230bb19a054fb15e804c101cfb28ef..a7a7101d2fd8a7f1fa049c1f5ebf9ee5958f1015 100644 (file)
@@ -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 */