cnfgen/dynintexpr/
extra_arith.rs

1// extra_arith.rs - extra arithmetic for dynintexpr.
2
3#![cfg_attr(docsrs, feature(doc_cfg))]
4//! The module contains extra operators definitions.
5
6use std::fmt::Debug;
7
8use crate::dynintexpr::DynIntExprNode;
9
10use super::*;
11use crate::VarLit;
12
13impl<T, const SIGN: bool> ExtraOps for DynIntExprNode<T, SIGN>
14where
15    T: VarLit + Neg<Output = T> + Debug,
16    isize: TryFrom<T>,
17    <T as TryInto<usize>>::Error: Debug,
18    <T as TryFrom<usize>>::Error: Debug,
19    <isize as TryFrom<T>>::Error: Debug,
20{
21    type Output = Self;
22    type BoolOutput = BoolExprNode<T>;
23
24    fn count_zeros(self) -> Self::Output {
25        (!self).count_ones()
26    }
27
28    fn count_ones(self) -> Self::Output {
29        let n = self.indexes.len();
30        let mut elems = (0..n)
31            .map(|x| DynIntExprNode::filled_expr(1, self.bit(x)))
32            .collect::<Vec<_>>();
33        let mut bits = 1;
34        let creator = self.creator.clone();
35        while bits < (n << 1) {
36            let elem_len = elems.len();
37            let mut new_elems = vec![];
38            for i in 0..(elem_len >> 1) {
39                // get elements: a + b with zero bit extension
40                let a =
41                    elems[i << 1]
42                        .clone()
43                        .concat(DynIntExprNode::filled(creator.clone(), 1, false));
44                let b = elems[(i << 1) + 1].clone().concat(DynIntExprNode::filled(
45                    creator.clone(),
46                    1,
47                    false,
48                ));
49                // summarize it
50                new_elems.push(a.addc(b, BoolExprNode::single_value(creator.clone(), false)));
51            }
52            if (elem_len & 1) != 0 {
53                // add last element if number of elements is odd
54                new_elems.push(elems.last().unwrap().clone().concat(DynIntExprNode::filled(
55                    creator.clone(),
56                    1,
57                    false,
58                )));
59            }
60            elems = new_elems;
61            bits <<= 1;
62        }
63        // conversion to int
64        DynIntExprNode::from_boolexprs((0..n).map(|x| {
65            if x < elems[0].bitnum() {
66                elems[0].bit(x)
67            } else {
68                BoolExprNode::single_value(creator.clone(), false)
69            }
70        }))
71    }
72
73    fn leading_zeros(self) -> Self::Output {
74        let n = self.indexes.len();
75        let creator = self.creator.clone();
76        let mut out_bits = vec![];
77        let mut enable = BoolExprNode::single_value(creator.clone(), true);
78        for i in 0..n {
79            let b = !self.bit(n - i - 1) & enable;
80            out_bits.push(b.clone());
81            enable = b;
82        }
83        DynIntExprNode::from_boolexprs(out_bits).count_ones()
84    }
85
86    fn leading_ones(self) -> Self::Output {
87        (!self).leading_zeros()
88    }
89
90    fn trailing_zeros(self) -> Self::Output {
91        let n = self.indexes.len();
92        let creator = self.creator.clone();
93        let mut out_bits = vec![];
94        let mut enable = BoolExprNode::single_value(creator.clone(), true);
95        for i in 0..n {
96            let b = !self.bit(i) & enable;
97            out_bits.push(b.clone());
98            enable = b;
99        }
100        DynIntExprNode::from_boolexprs(out_bits).count_ones()
101    }
102
103    fn trailing_ones(self) -> Self::Output {
104        (!self).trailing_zeros()
105    }
106
107    fn is_power_of_two(self) -> Self::BoolOutput {
108        let n = self.indexes.len();
109        let creator = self.creator.clone();
110        let mut s = BoolExprNode::single_value(creator.clone(), false);
111        let mut c = BoolExprNode::single_value(creator.clone(), false);
112        for i in 0..n {
113            let (s1, c1) = half_adder(s.clone(), self.bit(i));
114            s = s1;
115            c |= c1;
116        }
117        s & !c
118    }
119
120    fn reverse_bits(self) -> Self::Output {
121        let n = self.indexes.len();
122        DynIntExprNode::from_boolexprs((0..n).map(|x| self.bit(n - x - 1)))
123    }
124}
125
126#[cfg(test)]
127mod tests {
128    use super::*;
129    use crate::intexpr::IntExprNode;
130    use generic_array::typenum::*;
131
132    macro_rules! test_expr_node_op {
133        ($sign:expr, $op:ident) => {
134            let ec = ExprCreator::new();
135            let x1 = DynIntExprNode::<isize, $sign>::variable(ec.clone(), 12);
136            let res = x1.$op();
137
138            let exp_ec = ExprCreator::new();
139            let x1 = IntExprNode::<isize, U12, $sign>::variable(exp_ec.clone());
140            let exp = x1.$op();
141
142            assert_eq!(exp.indexes.as_slice(), res.indexes.as_slice());
143            assert_eq!(*exp_ec.borrow(), *ec.borrow());
144
145            let ec = ExprCreator::new();
146            let x1 = DynIntExprNode::<isize, $sign>::variable(ec.clone(), 10);
147            let res = x1.$op();
148
149            let exp_ec = ExprCreator::new();
150            let x1 = IntExprNode::<isize, U10, $sign>::variable(exp_ec.clone());
151            let exp = x1.$op();
152
153            assert_eq!(exp.indexes.as_slice(), res.indexes.as_slice());
154            assert_eq!(*exp_ec.borrow(), *ec.borrow());
155
156            let ec = ExprCreator::new();
157            let x1 = DynIntExprNode::<isize, $sign>::variable(ec.clone(), 8);
158            let res = x1.$op();
159
160            let exp_ec = ExprCreator::new();
161            let x1 = IntExprNode::<isize, U8, $sign>::variable(exp_ec.clone());
162            let exp = x1.$op();
163
164            assert_eq!(exp.indexes.as_slice(), res.indexes.as_slice());
165            assert_eq!(*exp_ec.borrow(), *ec.borrow());
166        };
167    }
168
169    macro_rules! test_expr_node_bitop {
170        ($sign:expr, $op:ident) => {
171            let ec = ExprCreator::new();
172            let x1 = DynIntExprNode::<isize, $sign>::variable(ec.clone(), 12);
173            let res = x1.$op();
174
175            let exp_ec = ExprCreator::new();
176            let x1 = IntExprNode::<isize, U12, $sign>::variable(exp_ec.clone());
177            let exp = x1.$op();
178
179            assert_eq!(exp.index, res.index);
180            assert_eq!(*exp_ec.borrow(), *ec.borrow());
181
182            let ec = ExprCreator::new();
183            let x1 = DynIntExprNode::<isize, $sign>::variable(ec.clone(), 10);
184            let res = x1.$op();
185
186            let exp_ec = ExprCreator::new();
187            let x1 = IntExprNode::<isize, U10, $sign>::variable(exp_ec.clone());
188            let exp = x1.$op();
189
190            assert_eq!(exp.index, res.index);
191            assert_eq!(*exp_ec.borrow(), *ec.borrow());
192
193            let ec = ExprCreator::new();
194            let x1 = DynIntExprNode::<isize, $sign>::variable(ec.clone(), 8);
195            let res = x1.$op();
196
197            let exp_ec = ExprCreator::new();
198            let x1 = IntExprNode::<isize, U8, $sign>::variable(exp_ec.clone());
199            let exp = x1.$op();
200
201            assert_eq!(exp.index, res.index);
202            assert_eq!(*exp_ec.borrow(), *ec.borrow());
203        };
204    }
205
206    #[test]
207    fn test_expr_node_ops() {
208        test_expr_node_op!(false, count_ones);
209        test_expr_node_op!(true, count_ones);
210        test_expr_node_op!(false, count_zeros);
211        test_expr_node_op!(true, count_zeros);
212        test_expr_node_op!(false, leading_zeros);
213        test_expr_node_op!(true, leading_zeros);
214        test_expr_node_op!(false, leading_ones);
215        test_expr_node_op!(true, leading_ones);
216        test_expr_node_op!(false, trailing_zeros);
217        test_expr_node_op!(true, trailing_zeros);
218        test_expr_node_op!(false, trailing_ones);
219        test_expr_node_op!(true, trailing_ones);
220        test_expr_node_op!(false, reverse_bits);
221        test_expr_node_op!(true, reverse_bits);
222        test_expr_node_bitop!(false, is_power_of_two);
223        test_expr_node_bitop!(true, is_power_of_two);
224    }
225}
cnfgen/dynintexpr/extra_arith.rs

cnfgen/dynintexpr/
extra_arith.rs
