add optimization to bounds search

lion/microbenchmark.c

@@ -13,7 +13,7 @@ uint64_t main() {
   x = malloc(8);
   *x = 0;
 
-  b = read(0, x, SIZEOFUINT32);
+  b = read(0, x, SIZEOFUINT64);
   d = *x;
 
   c = b;

lion/script2.sh

@@ -315,14 +315,14 @@ echo "insertion-sort n=10000 boolector input-limit 12"
 time (gtimeout --foreground -v 35m ../target/release/unicorn beator insertion-sort.m --unroll 10000 -p --solver boolector --find-bounds --input-limit 12 -t 200000)
 '
 
- : '
-i=8
+: '
+i=4
 
-while [ $i -le 64 ]
+while [ $i -le 32 ]
 do
   echo "insertion-sort1 n=10000 boolector input-limit $i"
   time (gtimeout --foreground -v 35m ../target/release/unicorn beator insertion-sort1.m --unroll 10000 -p --solver boolector --find-bounds --input-limit $i -t 200000 --fast-minimize)
-  ((i += 8))
+  ((i += 4))
 done
 '
 
@@ -353,16 +353,18 @@ do
 time (gtimeout --foreground -v 35m ../target/release/unicorn beator microbenchmark.m --unroll 10000 -p --solver z3 --find-bounds --input-limit $i -t 200000 --fast-minimize)
   ((i += 1))
 done
+'
+
 
 i=0
 
-while [ $i -le 3 ]
+while [ $i -le 5 ]
 do
   echo "microbenchmark n=256 boolector input-limit $i"
 time (gtimeout --foreground -v 35m ../target/release/unicorn beator microbenchmark.m --unroll 256 -p --solver boolector --find-bounds --input-limit $i -t 200000 --fast-minimize)
   ((i += 1))
 done
-'
+
 
 : '
 i=0
@@ -388,7 +390,7 @@ i=0
 while [ $i -le 3 ]
 do
   echo "microbenchmark n=256 boolector input-limit $i"
-  time (gtimeout --foreground -v 35m ../target/release/unicorn beator microbenchmark.m --unroll 256 -p --solver boolector --input-limit $i -t200000 --fast-minimize --out biere/microbenchmark-il${i}.btor2)
+  time (gtimeout --foreground -v 35m ../target/release/unicorn beator microbenchmark.m --unroll 256 -p --solver boolector --input-limit $i -t 200000 --fast-minimize --out biere/microbenchmark-il${i}.btor2)
   ((i += 1))
 done
 
@@ -400,7 +402,6 @@ do
   time (gtimeout --foreground -v 35m ../target/release/unicorn beator insertion-sort1.m --unroll 10000 -p --solver boolector --input-limit $i -t 200000 --fast-minimize --out biere/insertion-sort-il${i}.btor2)
   ((i += 8))
 done
-'
 
 echo "insertion-sort1 n=10000 boolector input-limit 2"
 time (gtimeout --foreground -v 35m ../target/release/unicorn beator insertion-sort1.m --unroll 10000 -p --solver boolector --input-limit 2 -t 200000 --fast-minimize --out biere/insertion-sort-il2.btor2)
@@ -410,3 +411,4 @@ time (gtimeout --foreground -v 35m ../target/release/unicorn beator insertion-so
 
 echo "insertion-sort1 n=10000 boolector input-limit 12"
 time (gtimeout --foreground -v 35m ../target/release/unicorn beator insertion-sort1.m --unroll 10000 -p --solver boolector --input-limit 12 -t 200000 --fast-minimize --out biere/insertion-sort-il12.btor2)
+'

src/main.rs

@@ -164,6 +164,7 @@ fn main() -> Result<()> {
                                 unroll_depth,
                                 prune,
                                 timeout,
+                                one_query,
                                 0
                             ),
                             #[cfg(feature = "z3")]
@@ -174,6 +175,7 @@ fn main() -> Result<()> {
                                 unroll_depth,
                                 prune,
                                 timeout,
+                                one_query,
                                 0
                             ),
                         }

src/unicorn/builder.rs

@@ -221,6 +221,15 @@ impl ModelBuilder {
         })
     }
 
+    fn new_const_bit(&mut self, imm: u64) -> NodeRef {
+        assert!(imm == 0 || imm == 1, "const bit must be 0 or 1!");
+        self.add_node(Node::Const {
+            nid: self.current_nid,
+            sort: NodeType::Bit,
+            imm,
+        })
+    }
+
     fn new_read(&mut self, address: NodeRef) -> NodeRef {
         self.add_node(Node::Read {
             nid: self.current_nid,
@@ -382,6 +391,14 @@ impl ModelBuilder {
         self.new_not_bit(and_node)
     }
 
+    fn new_or_bits(&mut self, nodes: &[&NodeRef]) -> NodeRef {
+        let mut result = self.new_const_bit(0);
+        for &node in nodes {
+            result = self.new_or_bit(result, node.clone());
+        }
+        result
+    }
+
     // We represent `xor(a, b)` as `sub(or(a, b), and(a, b))` instead.
     fn new_xor(&mut self, left: NodeRef, right: NodeRef) -> NodeRef {
         let or_node = self.new_or(left.clone(), right.clone());
@@ -1752,6 +1769,7 @@ impl ModelBuilder {
 
         let term_cond = self.new_and_bit(self.terminate_mode.clone(), is_exit);
         let term_cond_depleted_input = self.new_and_bit(term_cond.clone(), is_input_depleted);
+
         self.new_good(if less_input { term_cond_depleted_input } else { term_cond }, "exit-state");
 
         Ok(())

src/unicorn/horizon.rs

@@ -32,6 +32,7 @@ pub fn compute_bounds<S: SMTSolver>(
     unroll_depth: usize,
     prune: bool,
     timeout: Option<Duration>,
+    one_query: bool,
     start: usize
 ) {
     let mut prev_depth = 0;
@@ -55,9 +56,11 @@ pub fn compute_bounds<S: SMTSolver>(
             }
         }
 
-        let good_states_initial = maybe_prune_and_get_good_states(
+        let good_states_initial = optimize_and_get_good_states::<S>(
             &mut model.clone(),
-            prune
+            prune,
+            timeout,
+            one_query
         );
 
         let good = &good_states_initial[0];
@@ -146,12 +149,16 @@ pub fn compute_bounds<S: SMTSolver>(
     }
 }
 
-fn maybe_prune_and_get_good_states(
+fn optimize_and_get_good_states<S: SMTSolver>(
     model: &mut Model,
-    prune: bool
+    prune: bool,
+    timeout: Option<Duration>,
+    one_query: bool,
 ) -> Vec<NodeRef> {
     if prune {
         prune_model(model);
+
+        optimize_model_with_solver::<S>(model, timeout, true, false, one_query, false);
     }
 
     model.good_states_initial.clone()