Move term eval to new module (#197)

src/ir/opt/mod.rs

@@ -15,7 +15,7 @@ mod visit;
 
 use super::term::*;
 
-use log::{debug, trace};
+use log::{debug, info, trace};
 
 #[derive(Clone, Debug)]
 /// An optimization pass
@@ -63,6 +63,9 @@ pub enum Opt {
 pub fn opt<I: IntoIterator<Item = Opt>>(mut cs: Computations, optimizations: I) -> Computations {
     for c in cs.comps.values() {
         trace!("Before all opts: {}", text::serialize_computation(c));
+        info!("Before all opts: {} terms", c.stats().main.n_terms);
+        debug!("Before all opts: {:#?}", c.stats());
+        debug!("Before all opts: {:#?}", c.detailed_stats());
     }
     for i in optimizations {
         debug!("Applying: {:?}", i);
@@ -162,10 +165,9 @@ pub fn opt<I: IntoIterator<Item = Opt>>(mut cs: Computations, optimizations: I)
                     fits_in_bits_ip::fits_in_bits_ip(c);
                 }
             }
-            debug!("After {:?}: {} outputs", i, c.outputs.len());
+            info!("After {:?}: {} terms", i, c.stats().main.n_terms);
+            debug!("After {:?}: {:#?}", i, c.stats());
             trace!("After {:?}: {}", i, text::serialize_computation(c));
-            //debug!("After {:?}: {}", i, Letified(cs.outputs[0].clone()));
-            debug!("After {:?}: {} terms", i, c.terms());
             #[cfg(debug_assertions)]
             c.precomputes.check_topo_orderable();
         }

src/ir/opt/sha.rs

@@ -6,6 +6,8 @@ use std::collections::HashSet;
 
 /// Detects common C-language SHA patterns and rewrites them.
 pub fn sha_rewrites(term_: &Term) -> Term {
+    let mut ch_count = 0;
+    let mut maj_count = 0;
     // what does a term rewrite to?
     let mut cache = TermMap::<Term>::default();
     for t in PostOrderIter::new(term_.clone()) {
@@ -54,7 +56,7 @@ pub fn sha_rewrites(term_: &Term) -> Term {
                             });
                         if let Some((c, t, f)) = opt_match {
                             if let Sort::BitVector(w) = check(t) {
-                                debug!("SHA CH");
+                                ch_count += 1;
                                 Some(term(
                                 BV_CONCAT,
                                 (0..w)
@@ -93,7 +95,7 @@ pub fn sha_rewrites(term_: &Term) -> Term {
                             && s1.intersection(&s2).count() == 1
                             && s2.intersection(&s0).count() == 1
                         {
-                            debug!("SHA MAJ");
+                            maj_count += 1;
                             let items = s0.union(&s1).collect::<Vec<_>>();
                             let w = check(c0).as_bv();
                             Some(term(
@@ -131,6 +133,8 @@ pub fn sha_rewrites(term_: &Term) -> Term {
         });
         cache.insert(t, new_t);
     }
+    debug!("SHA MAJ count: {}", maj_count);
+    debug!("SHA CH count: {}", ch_count);
     cache.get(term_).unwrap().clone()
 }