Decrease the size of Op and Sort. (circify#199)

circ_hc/Cargo.toml

@@ -14,7 +14,7 @@ default = ["hashconsing", "lru", "raw", "rc"]
 fxhash = "0.2.1"
 hashconsing = { git = "https://github.com/alex-ozdemir/hashconsing.git", branch = "phash", optional = true }
 log = "0.4"
-lru = { version = "0.7.2", optional = true }
+lru = { version = "0.12", optional = true }
 
 [dev-dependencies]
 quickcheck = "1"

circ_hc/src/collections/lru.rs

@@ -1,5 +1,7 @@
 //! A LRU cache from terms to values which does not retain its keys.
 
+use std::num::NonZero;
+
 use crate::Table;
 
 /// A LRU cache from terms to values which does not retain its keys.
@@ -11,7 +13,7 @@ impl<Op, T: Table<Op>, V> NodeLruCache<Op, T, V> {
     /// Create an empty cache with room for `n` items.
     pub fn with_capacity(n: usize) -> Self {
         Self {
-            inner: lru::LruCache::new(n),
+            inner: lru::LruCache::new(NonZero::new(n).unwrap()),
         }
     }
 }

examples/circ.rs

@@ -404,7 +404,7 @@ fn main() {
                 .ordered_inputs()
                 .iter()
                 .map(|term| match term.op() {
-                    Op::Var(n, s) => (n.clone(), s.clone()),
+                    Op::Var(v) => (v.name.to_string(), v.sort.clone()),
                     _ => unreachable!(),
                 })
                 .collect();

examples/opa_bench.rs

@@ -20,7 +20,7 @@ fn main() {
         .format_timestamp(None)
         .init();
     let options = Options::parse();
-    let v = leaf_term(Op::Var("a".to_owned(), Sort::BitVector(32)));
+    let v = var("a".to_owned(), Sort::BitVector(32));
     let mut t = v.clone();
     for _i in 0..options.n_mults {
         t = term![BV_MUL; t.clone(), t.clone()];

src/circify/mem.rs

@@ -55,11 +55,11 @@ impl MemManager {
     /// Allocate a new stack array, equal to `array`.
     pub fn allocate(&mut self, array: Term) -> AllocId {
         let s = check(&array);
-        if let Sort::Array(box_addr_width, box_val_width, size) = s {
-            if let Sort::BitVector(addr_width) = *box_addr_width {
-                if let Sort::BitVector(val_width) = *box_val_width {
+        if let Sort::Array(a) = s {
+            if let Sort::BitVector(addr_width) = &a.key {
+                if let Sort::BitVector(val_width) = &a.val {
                     let id = self.take_next_id();
-                    let alloc = Alloc::new(addr_width, val_width, size, array);
+                    let alloc = Alloc::new(*addr_width, *val_width, a.size, array);
                     self.allocs.insert(id, alloc);
                     id
                 } else {
@@ -85,11 +85,11 @@ impl MemManager {
     ///
     /// Returns a (concrete) allocation identifier which can be used to access this allocation.
     pub fn zero_allocate(&mut self, size: usize, addr_width: usize, val_width: usize) -> AllocId {
-        self.allocate(term![Op::Const(Value::Array(Array::default(
+        self.allocate(const_(Value::Array(Array::default(
             Sort::BitVector(addr_width),
             &Sort::BitVector(val_width),
-            size
-        )))])
+            size,
+        ))))
     }
 
     /// Load the value of index `offset` from the allocation `id`.
@@ -130,28 +130,24 @@ impl MemManager {
     }
 }
 
-#[cfg(all(feature = "smt", feature = "test", feature = "zok"))]
+#[cfg(all(feature = "smt", test, feature = "zok"))]
 mod test {
     use super::*;
     use crate::target::smt::check_sat;
     use std::cell::RefCell;
     use std::rc::Rc;
 
     fn bv_var(s: &str, w: usize) -> Term {
-        leaf_term(Op::Var(s.to_owned(), Sort::BitVector(w)))
+        var(s.to_owned(), Sort::BitVector(w))
     }
 
+    #[test]
     fn sat_test() {
-        let cs = Rc::new(RefCell::new(Computation::new(false)));
+        let cs = Rc::new(RefCell::new(Computation::new()));
         let mut mem = MemManager::default();
         let id0 = mem.zero_allocate(6, 4, 8);
         let _id1 = mem.zero_allocate(6, 4, 8);
-        mem.store(
-            id0,
-            bv_lit(3, 4),
-            bv_lit(2, 8),
-            leaf_term(Op::Const(Value::Bool(true))),
-        );
+        mem.store(id0, bv_lit(3, 4), bv_lit(2, 8), const_(Value::Bool(true)));
         let a = mem.load(id0, bv_lit(3, 4));
         let b = mem.load(id0, bv_lit(1, 4));
         let t = term![Op::BvBinPred(BvBinPred::Ugt); a, b];
@@ -163,17 +159,13 @@ mod test {
         assert!(check_sat(&sys))
     }
 
+    #[test]
     fn unsat_test() {
-        let cs = Rc::new(RefCell::new(Computation::new(false)));
+        let cs = Rc::new(RefCell::new(Computation::new()));
         let mut mem = MemManager::default();
         let id0 = mem.zero_allocate(6, 4, 8);
         let _id1 = mem.zero_allocate(6, 4, 8);
-        mem.store(
-            id0,
-            bv_lit(3, 4),
-            bv_var("a", 8),
-            leaf_term(Op::Const(Value::Bool(true))),
-        );
+        mem.store(id0, bv_lit(3, 4), bv_var("a", 8), const_(Value::Bool(true)));
         let a = mem.load(id0, bv_lit(3, 4));
         let b = mem.load(id0, bv_lit(3, 4));
         let t = term![Op::Not; term![Op::Eq; a, b]];

src/circify/mod.rs

@@ -301,7 +301,7 @@ impl<Ty: Display> FnFrame<Ty> {
                 StateEntry::Break(name_, ref mut break_conds) => {
                     if name_ == name {
                         break_conds.push(if break_if.is_empty() {
-                            leaf_term(Op::Const(Value::Bool(true)))
+                            bool_lit(true)
                         } else {
                             term(Op::BoolNaryOp(BoolNaryOp::And), break_if)
                         });
@@ -437,7 +437,7 @@ impl<E: Embeddable> Circify<E> {
                 mem: Rc::new(RefCell::new(mem::MemManager::default())),
                 cs,
             },
-            condition: leaf_term(Op::Const(Value::Bool(true))),
+            condition: bool_lit(true),
             typedefs: HashMap::default(),
         }
     }
@@ -677,7 +677,7 @@ impl<E: Embeddable> Circify<E> {
         // TODO:  more precise conditions, depending on lex scopes.
         let cs: Vec<_> = self.fn_stack.iter().flat_map(|f| f.conditions()).collect();
         if cs.is_empty() {
-            leaf_term(Op::Const(Value::Bool(true)))
+            bool_lit(true)
         } else {
             term(Op::BoolNaryOp(BoolNaryOp::And), cs)
         }
@@ -935,7 +935,7 @@ mod test {
         impl Ty {
             fn default(&self) -> T {
                 match self {
-                    Ty::Bool => T::Base(leaf_term(Op::Const(Value::Bool(false)))),
+                    Ty::Bool => T::Base(bool_lit(false)),
                     Ty::Pair(a, b) => T::Pair(Box::new(a.default()), Box::new(b.default())),
                 }
             }

src/front/c/mod.rs

@@ -54,10 +54,11 @@ impl FrontEnd for C {
         let main_comp = g.circify().consume().borrow().clone();
         cs.comps.insert("main".to_string(), main_comp);
         while let Some(call_term) = g.function_queue.pop() {
-            if let Op::Call(name, arg_sorts, rets) = call_term.op() {
-                g.fn_call(name, arg_sorts, rets);
+            if let Op::Call(call) = call_term.op() {
+                let name = call.name.to_string();
+                g.fn_call(&name, &call.arg_sorts, &call.ret_sort);
                 let comp = g.circify().consume().borrow().clone();
-                cs.comps.insert(name.to_string(), comp);
+                cs.comps.insert(name, comp);
             } else {
                 panic!("Non-call term added to function queue.");
             }
@@ -1265,11 +1266,11 @@ impl CGen {
             assert!(p_sort == arg_sorts[i]);
             let p_ty = match &param.ty {
                 Ty::Ptr(_, t) => {
-                    if let Sort::Array(_, _, len) = p_sort {
-                        let dims = vec![len];
+                    if let Sort::Array(a) = p_sort {
+                        let dims = vec![a.size];
                         // Add reference
                         ret_names.push(p_name.clone());
-                        Ty::Array(len, dims, t.clone())
+                        Ty::Array(a.size, dims, t.clone())
                     } else {
                         panic!("Ptr type does not match with Array sort: {}", p_sort)
                     }

src/front/c/term.rs

@@ -499,8 +499,8 @@ pub fn uge(a: CTerm, b: CTerm) -> Result<CTerm, String> {
 
 pub fn const_int(a: CTerm) -> Integer {
     let s = match &a.term {
-        CTermData::Int(s, _, i) => match &i.op() {
-            Op::Const(Value::BitVector(f)) => {
+        CTermData::Int(s, _, i) => match i.as_value_opt() {
+            Some(Value::BitVector(f)) => {
                 if *s {
                     f.as_sint()
                 } else {
@@ -622,7 +622,7 @@ impl Embeddable for Ct {
                 };
                 for (i, t) in v.iter().enumerate() {
                     let val = t.term.term(ctx);
-                    let t_term = leaf_term(Op::Const(Value::Bool(true)));
+                    let t_term = bool_lit(true);
                     mem.store(id, bv_lit(i, 32), val, t_term);
                 }
                 arr

src/front/c/types.rs

@@ -82,9 +82,7 @@ impl Ty {
             Self::Void => Sort::Bool,
             Self::Bool => Sort::Bool,
             Self::Int(_s, w) => Sort::BitVector(*w),
-            Self::Array(n, _, b) => {
-                Sort::Array(Box::new(Sort::BitVector(32)), Box::new(b.sort()), *n)
-            }
+            Self::Array(n, _, b) => Sort::new_array(Sort::BitVector(32), b.sort(), *n),
             Self::Struct(_name, fs) => {
                 Sort::Tuple(fs.fields().map(|(_f_name, f_ty)| f_ty.sort()).collect())
             }

src/front/datalog/term.rs

@@ -33,7 +33,7 @@ impl T {
         match (ty, ir) {
             (Ty::Bool, Sort::Bool) | (Ty::Field, Sort::Field(_)) => {}
             (Ty::Uint(w), Sort::BitVector(w2)) if *w as usize == *w2 => {}
-            (Ty::Array(l, t), Sort::Array(_, t2, l2)) if l == l2 => Self::check_ty(t2, t),
+            (Ty::Array(l, t), Sort::Array(a)) if *l == a.size => Self::check_ty(&a.val, t),
             _ => panic!("IR sort {} doesn't match datalog type {}", ir, ty),
         }
     }
@@ -63,12 +63,12 @@ pub fn pf_ir_lit<I>(i: I) -> Term
 where
     Integer: From<I>,
 {
-    leaf_term(Op::Const(Value::Field(cfg().field().new_v(i))))
+    const_(Value::Field(cfg().field().new_v(i)))
 }
 
 /// Initialize a boolean literal
 pub fn bool_lit(b: bool) -> T {
-    T::new(leaf_term(Op::Const(Value::Bool(b))), Ty::Bool)
+    T::new(const_(Value::Bool(b)), Ty::Bool)
 }
 
 /// Initialize an unsigned integer literal
@@ -82,11 +82,7 @@ impl Ty {
             Self::Bool => Sort::Bool,
             Self::Uint(w) => Sort::BitVector(*w as usize),
             Self::Field => Sort::Field(cfg().field().clone()),
-            Self::Array(n, b) => Sort::Array(
-                Box::new(Sort::Field(cfg().field().clone())),
-                Box::new(b.sort()),
-                *n,
-            ),
+            Self::Array(n, b) => Sort::new_array(Sort::Field(cfg().field().clone()), b.sort(), *n),
         }
     }
     fn default_ir_term(&self) -> Term {
@@ -318,7 +314,7 @@ pub fn or(s: &T, t: &T) -> Result<T> {
 pub fn uint_to_field(s: &T) -> Result<T> {
     match &s.ty {
         Ty::Uint(_) => Ok(T::new(
-            term![Op::UbvToPf(cfg().field().clone()); s.ir.clone()],
+            term![Op::new_ubv_to_pf(cfg().field().clone()); s.ir.clone()],
             Ty::Field,
         )),
         _ => Err(ErrorKind::InvalidUnOp("to_field".into(), s.clone())),

src/front/zsharp/interp.rs

@@ -21,7 +21,7 @@ pub fn extract(
             let ir_val = scalar_input_values
                 .remove(name)
                 .ok_or_else(|| format!("Could not find scalar variable {name} in the input map"))?;
-            Ok(T::new(ty.clone(), leaf_term(Op::Const(ir_val))))
+            Ok(T::new(ty.clone(), const_(ir_val)))
         }
         Ty::Array(elem_count, elem_ty) => T::new_array(
             (0..*elem_count)