cnfgen/
int_utils.rs

1// int_utils.rs - integer utilities
2
3#![cfg_attr(docsrs, feature(doc_cfg))]
4//! The module to generate CNF clauses from integer expressions.
5
6use std::cell::RefCell;
7use std::fmt::Debug;
8use std::ops::Neg;
9use std::rc::Rc;
10
11use crate::boolexpr::{bool_ite, half_adder, opt_full_adder, BoolExprNode};
12use crate::boolexpr_creator::ExprCreator;
13use crate::intexpr::BitVal;
14use crate::writer::VarLit;
15
16pub(super) fn gen_dadda_mult<T>(
17    creator: Rc<RefCell<ExprCreator<T>>>,
18    matrix: &mut [Vec<usize>],
19) -> Vec<usize>
20where
21    T: VarLit + Neg<Output = T> + Debug,
22    isize: TryFrom<T>,
23    <T as TryInto<usize>>::Error: Debug,
24    <T as TryFrom<usize>>::Error: Debug,
25    <isize as TryFrom<T>>::Error: Debug,
26{
27    let max_col_size = matrix.iter().map(|col| col.len()).max().unwrap();
28    let mut step_sizes = vec![];
29    {
30        let mut max_step_size = 2usize;
31        while max_step_size < max_col_size {
32            step_sizes.push(max_step_size);
33            max_step_size += max_step_size >> 1;
34        }
35    }
36    let mut extracol: Vec<usize> = vec![];
37    let mut next_extracol: Vec<usize> = vec![];
38    // main routine
39    let matrixlen = matrix.len();
40    for new_column_size in step_sizes.iter().rev() {
41        for (coli, col) in matrix.iter_mut().enumerate() {
42            next_extracol.clear();
43            if col.len() + extracol.len() > *new_column_size {
44                let cells_to_reduce = extracol.len() + col.len() - *new_column_size;
45                let mut src = col.len() - cells_to_reduce - ((cells_to_reduce + 1) >> 1);
46                let mut dest = src;
47                while src < col.len() {
48                    let a = BoolExprNode::new(creator.clone(), col[src]);
49                    let b = BoolExprNode::new(creator.clone(), col[src + 1]);
50                    // if src + 2 < col.len() {
51                    //     println!(
52                    //         "cell: {}: {}: {} {} {}",
53                    //         new_column_size,
54                    //         coli,
55                    //         src,
56                    //         src + 1,
57                    //         src + 2
58                    //     );
59                    // } else {
60                    //     println!("cell: {}: {}: {} {}", new_column_size, coli, src, src + 1);
61                    // }
62                    if coli + 1 < matrixlen {
63                        let (s, c) = if src + 2 < col.len() {
64                            // full adder
65                            opt_full_adder(a, b, BoolExprNode::new(creator.clone(), col[src + 2]))
66                        } else {
67                            // half adder
68                            half_adder(a, b)
69                        };
70                        col[dest] = s.index;
71                        next_extracol.push(c.index);
72                    } else {
73                        // only sum, ignore carry
74                        col[dest] = if src + 2 < col.len() {
75                            // full adder
76                            a ^ b ^ BoolExprNode::new(creator.clone(), col[src + 2])
77                        } else {
78                            // half adder
79                            a ^ b
80                        }
81                        .index;
82                    }
83                    src += 3;
84                    dest += 1;
85                }
86                col.resize(dest, 0);
87            }
88            col.extend(extracol.iter());
89            std::mem::swap(&mut extracol, &mut next_extracol);
90        }
91    }
92
93    // last phase
94    let mut output = vec![0; matrix.len()];
95    let mut c = BoolExprNode::new(creator.clone(), 0); // false
96    for (i, col) in matrix.iter().enumerate().take(matrix.len() - 1) {
97        (output[i], c) = if col.len() == 2 {
98            let (s0, c0) = opt_full_adder(
99                BoolExprNode::new(creator.clone(), col[0]),
100                BoolExprNode::new(creator.clone(), col[1]),
101                c,
102            );
103            (s0.index, c0)
104        } else {
105            let (s0, c0) = half_adder(BoolExprNode::new(creator.clone(), col[0]), c);
106            (s0.index, c0)
107        };
108    }
109    let col = matrix.last().unwrap();
110    output[matrix.len() - 1] = if col.len() == 2 {
111        BoolExprNode::new(creator.clone(), col[0]) ^ BoolExprNode::new(creator, col[1]) ^ c
112    } else if col.len() == 1 {
113        BoolExprNode::new(creator, col[0]) ^ c
114    } else {
115        c
116    }
117    .index;
118
119    output
120}
121
122pub(super) fn gen_dadda_matrix<'a, T>(
123    creator: Rc<RefCell<ExprCreator<T>>>,
124    avector: &'a [usize],
125    bvector: &'a [usize],
126    col_num: usize,
127) -> Vec<Vec<usize>>
128where
129    T: VarLit + Neg<Output = T> + Debug,
130    isize: TryFrom<T>,
131    <T as TryInto<usize>>::Error: Debug,
132    <T as TryFrom<usize>>::Error: Debug,
133    <isize as TryFrom<T>>::Error: Debug,
134{
135    let mut matrix = (0..col_num).into_iter().map(|_| vec![]).collect::<Vec<_>>();
136    for (i, a) in avector.iter().enumerate() {
137        for (j, b) in bvector.iter().enumerate() {
138            if i + j < col_num {
139                matrix[i + j].push(
140                    (BoolExprNode::new(creator.clone(), *a)
141                        & BoolExprNode::new(creator.clone(), *b))
142                    .index,
143                )
144            }
145        }
146    }
147    matrix
148}
149
150pub(super) const fn calc_log_bits(n: usize) -> usize {
151    if n == 0 {
152        return 0;
153    }
154    let nbits = usize::BITS - n.leading_zeros();
155    if (1 << (nbits - 1)) == n {
156        (nbits - 1) as usize
157    } else {
158        nbits as usize
159    }
160}
161
162pub(super) fn iter_shift_left<T, BV>(
163    output: &mut [usize],
164    input: BV,
165    rhs_bit: BoolExprNode<T>,
166    i: usize,
167) where
168    T: VarLit + Neg<Output = T> + Debug,
169    isize: TryFrom<T>,
170    <T as TryInto<usize>>::Error: Debug,
171    <T as TryFrom<usize>>::Error: Debug,
172    <isize as TryFrom<T>>::Error: Debug,
173    BV: BitVal<Output = BoolExprNode<T>> + Copy,
174{
175    output.iter_mut().enumerate().for_each(|(x, out)| {
176        *out = bool_ite(
177            rhs_bit.clone(),
178            // if no overflow then get bit(v)
179            if x >= (1usize << i) {
180                input.bit(x - (1 << i))
181            } else {
182                BoolExprNode::new(rhs_bit.creator.clone(), 0)
183            },
184            input.bit(x),
185        )
186        .index
187    });
188}
189
190pub(super) fn iter_shift_right<T, BV>(
191    output: &mut [usize],
192    input: BV,
193    rhs_bit: BoolExprNode<T>,
194    i: usize,
195    sign: bool,
196) where
197    T: VarLit + Neg<Output = T> + Debug,
198    isize: TryFrom<T>,
199    <T as TryInto<usize>>::Error: Debug,
200    <T as TryFrom<usize>>::Error: Debug,
201    <isize as TryFrom<T>>::Error: Debug,
202    BV: BitVal<Output = BoolExprNode<T>> + Copy,
203{
204    output.iter_mut().enumerate().for_each(|(x, out)| {
205        *out = bool_ite(
206            rhs_bit.clone(),
207            // if no overflow then get bit(v)
208            if x + (1usize << i) < input.bitnum() {
209                input.bit(x + (1 << i))
210            } else if sign {
211                input.bit(input.bitnum() - 1)
212            } else {
213                BoolExprNode::new(rhs_bit.creator.clone(), 0)
214            },
215            input.bit(x),
216        )
217        .index
218    });
219}
220
221pub(super) fn iter_rotate_left<T, BV>(
222    output: &mut [usize],
223    input: BV,
224    rhs_bit: BoolExprNode<T>,
225    i: usize,
226) where
227    T: VarLit + Neg<Output = T> + Debug,
228    isize: TryFrom<T>,
229    <T as TryInto<usize>>::Error: Debug,
230    <T as TryFrom<usize>>::Error: Debug,
231    <isize as TryFrom<T>>::Error: Debug,
232    BV: BitVal<Output = BoolExprNode<T>> + Copy,
233{
234    output.iter_mut().enumerate().for_each(|(x, out)| {
235        *out = bool_ite(
236            rhs_bit.clone(),
237            // if no overflow then get bit(v)
238            if x >= (1usize << i) {
239                input.bit(x - (1 << i))
240            } else {
241                input.bit(input.bitnum() + x - (1 << i))
242            },
243            input.bit(x),
244        )
245        .index
246    });
247}
248
249pub(super) fn iter_rotate_right<T, BV>(
250    output: &mut [usize],
251    input: BV,
252    rhs_bit: BoolExprNode<T>,
253    i: usize,
254) where
255    T: VarLit + Neg<Output = T> + Debug,
256    isize: TryFrom<T>,
257    <T as TryInto<usize>>::Error: Debug,
258    <T as TryFrom<usize>>::Error: Debug,
259    <isize as TryFrom<T>>::Error: Debug,
260    BV: BitVal<Output = BoolExprNode<T>> + Copy,
261{
262    output.iter_mut().enumerate().for_each(|(x, out)| {
263        *out = bool_ite(
264            rhs_bit.clone(),
265            // if no overflow then get bit(v)
266            if x + (1usize << i) < input.bitnum() {
267                input.bit(x + (1 << i))
268            } else {
269                input.bit(x + (1 << i) - input.bitnum())
270            },
271            input.bit(x),
272        )
273        .index
274    });
275}
276
277// return (carry_out and carry_out at last bit)
278pub(super) fn helper_addc_cout<T, BV>(
279    output: &mut [usize],
280    lhs: BV,
281    rhs: BV,
282    in_carry: BoolExprNode<T>,
283) -> (BoolExprNode<T>, BoolExprNode<T>)
284where
285    T: VarLit + Neg<Output = T> + Debug,
286    isize: TryFrom<T>,
287    <T as TryInto<usize>>::Error: Debug,
288    <T as TryFrom<usize>>::Error: Debug,
289    <isize as TryFrom<T>>::Error: Debug,
290    BV: BitVal<Output = BoolExprNode<T>> + Copy,
291{
292    let n = lhs.bitnum();
293    let mut c = in_carry;
294    for (i, out) in output.iter_mut().enumerate().take(n - 1) {
295        (*out, c) = {
296            let (s0, c0) = opt_full_adder(lhs.bit(i), rhs.bit(i), c);
297            (s0.index, c0)
298        };
299    }
300    let lastbit_c = c.clone();
301    (output[n - 1], c) = {
302        let (s0, c0) = opt_full_adder(lhs.bit(n - 1), rhs.bit(n - 1), c);
303        (s0.index, c0)
304    };
305    (c, lastbit_c)
306}
307
308// return (carry_out and carry_out at last bit)
309pub(super) fn helper_subc_cout<T, BV>(
310    output: &mut [usize],
311    lhs: BV,
312    rhs: BV,
313    in_carry: BoolExprNode<T>,
314) -> (BoolExprNode<T>, BoolExprNode<T>)
315where
316    T: VarLit + Neg<Output = T> + Debug,
317    isize: TryFrom<T>,
318    <T as TryInto<usize>>::Error: Debug,
319    <T as TryFrom<usize>>::Error: Debug,
320    <isize as TryFrom<T>>::Error: Debug,
321    BV: BitVal<Output = BoolExprNode<T>> + Copy,
322{
323    let n = lhs.bitnum();
324    let mut c = in_carry;
325    for (i, out) in output.iter_mut().enumerate().take(n - 1) {
326        (*out, c) = {
327            let (s0, c0) = opt_full_adder(lhs.bit(i), !rhs.bit(i), c);
328            (s0.index, c0)
329        };
330    }
331    let lastbit_c = c.clone();
332    (output[n - 1], c) = {
333        let (s0, c0) = opt_full_adder(lhs.bit(n - 1), !rhs.bit(n - 1), c);
334        (s0.index, c0)
335    };
336    (c, lastbit_c)
337}
338
339pub(super) fn helper_addc<T, BV>(output: &mut [usize], lhs: BV, rhs: BV, in_carry: BoolExprNode<T>)
340where
341    T: VarLit + Neg<Output = T> + Debug,
342    isize: TryFrom<T>,
343    <T as TryInto<usize>>::Error: Debug,
344    <T as TryFrom<usize>>::Error: Debug,
345    <isize as TryFrom<T>>::Error: Debug,
346    BV: BitVal<Output = BoolExprNode<T>> + Copy,
347{
348    let mut c = in_carry;
349    let n = lhs.bitnum();
350    for (i, out) in output.iter_mut().enumerate().take(n - 1) {
351        (*out, c) = {
352            let (s0, c0) = opt_full_adder(lhs.bit(i), rhs.bit(i), c);
353            (s0.index, c0)
354        };
355    }
356    output[n - 1] = (lhs.bit(n - 1) ^ rhs.bit(n - 1) ^ c).index;
357}
358
359pub(super) fn helper_subc<T, BV>(output: &mut [usize], lhs: BV, rhs: BV, in_carry: BoolExprNode<T>)
360where
361    T: VarLit + Neg<Output = T> + Debug,
362    isize: TryFrom<T>,
363    <T as TryInto<usize>>::Error: Debug,
364    <T as TryFrom<usize>>::Error: Debug,
365    <isize as TryFrom<T>>::Error: Debug,
366    BV: BitVal<Output = BoolExprNode<T>> + Copy,
367{
368    let mut c = in_carry;
369    let n = lhs.bitnum();
370    for (i, out) in output.iter_mut().enumerate().take(n - 1) {
371        (*out, c) = {
372            let (s0, c0) = opt_full_adder(lhs.bit(i), !rhs.bit(i), c);
373            (s0.index, c0)
374        };
375    }
376    output[n - 1] = (lhs.bit(n - 1) ^ !rhs.bit(n - 1) ^ c).index;
377}
378
379#[cfg(test)]
380mod tests {
381    use super::*;
382    use crate::boolexpr::test_utils::*;
383
384    use crate::intexpr::{IntExprNode, IntModAdd};
385    use generic_array::typenum::*;
386    use generic_array::GenericArray;
387
388    #[test]
389    fn test_gen_dadda_matrix() {
390        {
391            let ec = ExprCreator::new();
392            let a = IntExprNode::<isize, U3, false>::variable(ec.clone());
393            let b = IntExprNode::<isize, U4, false>::variable(ec.clone());
394            let res = gen_dadda_matrix(ec.clone(), &a.indexes, &b.indexes, 6);
395
396            let exp_ec = ExprCreator::new();
397            let a = alloc_boolvars(exp_ec.clone(), 3);
398            let b = alloc_boolvars(exp_ec.clone(), 4);
399            let a0b0 = a[0].clone() & b[0].clone();
400            let a0b1 = a[0].clone() & b[1].clone();
401            let a0b2 = a[0].clone() & b[2].clone();
402            let a0b3 = a[0].clone() & b[3].clone();
403            let a1b0 = a[1].clone() & b[0].clone();
404            let a1b1 = a[1].clone() & b[1].clone();
405            let a1b2 = a[1].clone() & b[2].clone();
406            let a1b3 = a[1].clone() & b[3].clone();
407            let a2b0 = a[2].clone() & b[0].clone();
408            let a2b1 = a[2].clone() & b[1].clone();
409            let a2b2 = a[2].clone() & b[2].clone();
410            let a2b3 = a[2].clone() & b[3].clone();
411            let exp = [
412                vec![a0b0],
413                vec![a0b1, a1b0],
414                vec![a0b2, a1b1, a2b0],
415                vec![a0b3, a1b2, a2b1],
416                vec![a1b3, a2b2],
417                vec![a2b3],
418            ]
419            .into_iter()
420            .map(|c| {
421                Vec::from(c)
422                    .into_iter()
423                    .map(|x| x.index)
424                    .collect::<Vec<_>>()
425            })
426            .collect::<Vec<_>>();
427
428            assert_eq!(exp, res);
429            assert_eq!(*exp_ec.borrow(), *ec.borrow());
430        }
431        {
432            let ec = ExprCreator::new();
433            let a = IntExprNode::<isize, U3, false>::variable(ec.clone());
434            let b = IntExprNode::<isize, U4, false>::variable(ec.clone());
435            let res = gen_dadda_matrix(ec.clone(), &a.indexes, &b.indexes, 4);
436
437            let exp_ec = ExprCreator::new();
438            let a = alloc_boolvars(exp_ec.clone(), 3);
439            let b = alloc_boolvars(exp_ec.clone(), 4);
440            let a0b0 = a[0].clone() & b[0].clone();
441            let a0b1 = a[0].clone() & b[1].clone();
442            let a0b2 = a[0].clone() & b[2].clone();
443            let a0b3 = a[0].clone() & b[3].clone();
444            let a1b0 = a[1].clone() & b[0].clone();
445            let a1b1 = a[1].clone() & b[1].clone();
446            let a1b2 = a[1].clone() & b[2].clone();
447            let a2b0 = a[2].clone() & b[0].clone();
448            let a2b1 = a[2].clone() & b[1].clone();
449            let exp = [
450                vec![a0b0],
451                vec![a0b1, a1b0],
452                vec![a0b2, a1b1, a2b0],
453                vec![a0b3, a1b2, a2b1],
454            ]
455            .into_iter()
456            .map(|c| {
457                Vec::from(c)
458                    .into_iter()
459                    .map(|x| x.index)
460                    .collect::<Vec<_>>()
461            })
462            .collect::<Vec<_>>();
463
464            assert_eq!(exp, res);
465            assert_eq!(*exp_ec.borrow(), *ec.borrow());
466        }
467    }
468
469    #[test]
470    fn test_gen_dadda_mult() {
471        {
472            let ec = ExprCreator::new();
473            let bvs = alloc_boolvars(ec.clone(), 4 * 3);
474            let mut matrix = vec![
475                vec![bvs[0].index],
476                vec![bvs[1].index, bvs[2].index],
477                vec![bvs[3].index, bvs[4].index, bvs[5].index],
478                vec![bvs[6].index, bvs[7].index, bvs[8].index],
479                vec![bvs[9].index, bvs[10].index],
480                vec![bvs[11].index],
481            ];
482            let res = gen_dadda_mult(ec.clone(), &mut matrix);
483
484            let exp_ec = ExprCreator::new();
485            let bvs = alloc_boolvars(exp_ec.clone(), 4 * 3);
486            //       5  8
487            //    2  4  7 10
488            // 0  1  3  6  9 11
489            let (s0, c0) = half_adder(bvs[4].clone(), bvs[5].clone());
490            let (s1, c1) = opt_full_adder(bvs[6].clone(), bvs[7].clone(), bvs[8].clone());
491            let (s2, c2) = half_adder(bvs[9].clone(), bvs[10].clone());
492            let a = IntExprNode::<isize, U6, false> {
493                creator: exp_ec.clone(),
494                indexes: GenericArray::clone_from_slice(&[
495                    bvs[0].index,
496                    bvs[1].index,
497                    bvs[3].index,
498                    s1.index,
499                    s2.index,
500                    bvs[11].index,
501                ]),
502            };
503            let b = IntExprNode::<isize, U6, false> {
504                creator: exp_ec.clone(),
505                indexes: GenericArray::clone_from_slice(&[
506                    0,
507                    bvs[2].index,
508                    s0.index,
509                    c0.index,
510                    c1.index,
511                    c2.index,
512                ]),
513            };
514            let exp = a.mod_add(b);
515
516            assert_eq!(exp.indexes.as_slice(), res.as_slice());
517            assert_eq!(*exp_ec.borrow(), *ec.borrow());
518        }
519        {
520            let ec = ExprCreator::new();
521            let bvs = alloc_boolvars(ec.clone(), 4 * 3);
522            let mut matrix = vec![
523                vec![bvs[0].index],
524                vec![bvs[1].index, bvs[2].index],
525                vec![bvs[3].index, bvs[4].index, bvs[5].index],
526                vec![bvs[6].index, bvs[7].index, bvs[8].index],
527                vec![bvs[9].index, bvs[10].index],
528                vec![bvs[11].index],
529                vec![],
530            ];
531            let res = gen_dadda_mult(ec.clone(), &mut matrix);
532
533            let exp_ec = ExprCreator::new();
534            let bvs = alloc_boolvars(exp_ec.clone(), 4 * 3);
535            //       5  8
536            //    2  4  7 10
537            // 0  1  3  6  9 11
538            let (s0, c0) = half_adder(bvs[4].clone(), bvs[5].clone());
539            let (s1, c1) = opt_full_adder(bvs[6].clone(), bvs[7].clone(), bvs[8].clone());
540            let (s2, c2) = half_adder(bvs[9].clone(), bvs[10].clone());
541            let a = IntExprNode::<isize, U7, false> {
542                creator: exp_ec.clone(),
543                indexes: GenericArray::clone_from_slice(&[
544                    bvs[0].index,
545                    bvs[1].index,
546                    bvs[3].index,
547                    s1.index,
548                    s2.index,
549                    bvs[11].index,
550                    0,
551                ]),
552            };
553            let b = IntExprNode::<isize, U7, false> {
554                creator: exp_ec.clone(),
555                indexes: GenericArray::clone_from_slice(&[
556                    0,
557                    bvs[2].index,
558                    s0.index,
559                    c0.index,
560                    c1.index,
561                    c2.index,
562                    0,
563                ]),
564            };
565            let exp = a.mod_add(b);
566
567            assert_eq!(exp.indexes.as_slice(), res.as_slice());
568            assert_eq!(*exp_ec.borrow(), *ec.borrow());
569        }
570        {
571            let ec = ExprCreator::new();
572            let bvs = alloc_boolvars(ec.clone(), 4 * 5);
573            let mut matrix = vec![
574                vec![bvs[0].index],
575                vec![bvs[1].index, bvs[2].index],
576                vec![bvs[3].index, bvs[4].index, bvs[5].index],
577                vec![bvs[6].index, bvs[7].index, bvs[8].index, bvs[9].index],
578                vec![bvs[10].index, bvs[11].index, bvs[12].index, bvs[13].index],
579                vec![bvs[14].index, bvs[15].index, bvs[16].index],
580                vec![bvs[17].index, bvs[18].index],
581                vec![bvs[19].index],
582            ];
583            let res = gen_dadda_mult(ec.clone(), &mut matrix);
584
585            let exp_ec = ExprCreator::new();
586            let bvs = alloc_boolvars(exp_ec.clone(), 4 * 5);
587            //          9 13
588            //       5  8 12 16
589            //    2  4  7 11 15 18
590            // 0  1  3  6 10 14 17 19
591            let (s0, c0) = half_adder(bvs[8].clone(), bvs[9].clone());
592            let (s1, c1) = opt_full_adder(bvs[11].clone(), bvs[12].clone(), bvs[13].clone());
593            let (s2, c2) = half_adder(bvs[15].clone(), bvs[16].clone());
594            //       5 s0 c0 c1 c2
595            //    2  4  7 s1 s2 18
596            // 0  1  3  6 10 14 17 19
597            let (s0_2, c0_2) = half_adder(bvs[4].clone(), bvs[5].clone());
598            let (s1_2, c1_2) = opt_full_adder(bvs[6].clone(), bvs[7].clone(), s0);
599            let (s2_2, c2_2) = opt_full_adder(bvs[10].clone(), s1, c0);
600            let (s3_2, c3_2) = opt_full_adder(bvs[14].clone(), s2, c1);
601            let (s4_2, c4_2) = opt_full_adder(bvs[17].clone(), bvs[18].clone(), c2);
602            //    2 s0 c0 c1 c2 c3 c4
603            // 0  1  3 s1 s2 s3 s4 19
604            let a = IntExprNode::<isize, U8, false> {
605                creator: exp_ec.clone(),
606                indexes: GenericArray::clone_from_slice(&[
607                    bvs[0].index,
608                    bvs[1].index,
609                    bvs[3].index,
610                    s1_2.index,
611                    s2_2.index,
612                    s3_2.index,
613                    s4_2.index,
614                    bvs[19].index,
615                ]),
616            };
617            let b = IntExprNode::<isize, U8, false> {
618                creator: exp_ec.clone(),
619                indexes: GenericArray::clone_from_slice(&[
620                    0,
621                    bvs[2].index,
622                    s0_2.index,
623                    c0_2.index,
624                    c1_2.index,
625                    c2_2.index,
626                    c3_2.index,
627                    c4_2.index,
628                ]),
629            };
630            let exp = a.mod_add(b);
631
632            assert_eq!(exp.indexes.as_slice(), res.as_slice());
633            assert_eq!(*exp_ec.borrow(), *ec.borrow());
634        }
635        {
636            let ec = ExprCreator::new();
637            let bvs = alloc_boolvars(ec.clone(), 4 * 5 - 3);
638            let mut matrix = vec![
639                vec![bvs[0].index],
640                vec![bvs[1].index, bvs[2].index],
641                vec![bvs[3].index, bvs[4].index, bvs[5].index],
642                vec![bvs[6].index, bvs[7].index, bvs[8].index, bvs[9].index],
643                vec![bvs[10].index, bvs[11].index, bvs[12].index, bvs[13].index],
644                vec![bvs[14].index, bvs[15].index, bvs[16].index],
645            ];
646            let res = gen_dadda_mult(ec.clone(), &mut matrix);
647
648            let exp_ec = ExprCreator::new();
649            let bvs = alloc_boolvars(exp_ec.clone(), 4 * 5 - 3);
650            //          9 13
651            //       5  8 12 16
652            //    2  4  7 11 15
653            // 0  1  3  6 10 14
654            let (s0, c0) = half_adder(bvs[8].clone(), bvs[9].clone());
655            let (s1, c1) = opt_full_adder(bvs[11].clone(), bvs[12].clone(), bvs[13].clone());
656            let s2 = bvs[15].clone() ^ bvs[16].clone();
657            //       5 s0 c0 c1
658            //    2  4  7 s1 s2
659            // 0  1  3  6 10 14
660            let (s0_2, c0_2) = half_adder(bvs[4].clone(), bvs[5].clone());
661            let (s1_2, c1_2) = opt_full_adder(bvs[6].clone(), bvs[7].clone(), s0);
662            let (s2_2, c2_2) = opt_full_adder(bvs[10].clone(), s1, c0);
663            let s3_2 = bvs[14].clone() ^ s2 ^ c1;
664            //    2 s0 c0 c1 c2
665            // 0  1  3 s1 s2 s3
666            let a = IntExprNode::<isize, U6, false> {
667                creator: exp_ec.clone(),
668                indexes: GenericArray::clone_from_slice(&[
669                    bvs[0].index,
670                    bvs[1].index,
671                    bvs[3].index,
672                    s1_2.index,
673                    s2_2.index,
674                    s3_2.index,
675                ]),
676            };
677            let b = IntExprNode::<isize, U6, false> {
678                creator: exp_ec.clone(),
679                indexes: GenericArray::clone_from_slice(&[
680                    0,
681                    bvs[2].index,
682                    s0_2.index,
683                    c0_2.index,
684                    c1_2.index,
685                    c2_2.index,
686                ]),
687            };
688            let exp = a.mod_add(b);
689
690            assert_eq!(exp.indexes.as_slice(), res.as_slice());
691            assert_eq!(*exp_ec.borrow(), *ec.borrow());
692        }
693        {
694            let ec = ExprCreator::new();
695            let bvs = alloc_boolvars(ec.clone(), 5 * 7);
696            let mut matrix = vec![
697                vec![bvs[0].index],
698                vec![bvs[1].index, bvs[2].index],
699                vec![bvs[3].index, bvs[4].index, bvs[5].index],
700                vec![bvs[6].index, bvs[7].index, bvs[8].index, bvs[9].index],
701                vec![
702                    bvs[10].index,
703                    bvs[11].index,
704                    bvs[12].index,
705                    bvs[13].index,
706                    bvs[14].index,
707                ],
708                vec![
709                    bvs[15].index,
710                    bvs[16].index,
711                    bvs[17].index,
712                    bvs[18].index,
713                    bvs[19].index,
714                ],
715                vec![
716                    bvs[20].index,
717                    bvs[21].index,
718                    bvs[22].index,
719                    bvs[23].index,
720                    bvs[24].index,
721                ],
722                vec![bvs[25].index, bvs[26].index, bvs[27].index, bvs[28].index],
723                vec![bvs[29].index, bvs[30].index, bvs[31].index],
724                vec![bvs[32].index, bvs[33].index],
725                vec![bvs[34].index],
726            ];
727            let res = gen_dadda_mult(ec.clone(), &mut matrix);
728
729            let exp_ec = ExprCreator::new();
730            let bvs = alloc_boolvars(exp_ec.clone(), 5 * 7);
731            //            14 19 24
732            //          9 13 18 23 28
733            //       5  8 12 17 22 27 31
734            //    2  4  7 11 16 21 26 30 33
735            // 0  1  3  6 10 15 20 25 29 32 34
736            let (s0, c0) = half_adder(bvs[13].clone(), bvs[14].clone());
737            let (s1, c1) = opt_full_adder(bvs[17].clone(), bvs[18].clone(), bvs[19].clone());
738            let (s2, c2) = opt_full_adder(bvs[22].clone(), bvs[23].clone(), bvs[24].clone());
739            let (s3, c3) = half_adder(bvs[27].clone(), bvs[28].clone());
740            //          9 s0 c0 c1 c2 c3
741            //       5  8 12 s1 s2 s3 31
742            //    2  4  7 11 16 21 26 30 33
743            // 0  1  3  6 10 15 20 25 29 32 34
744            let (s0_2, c0_2) = half_adder(bvs[8].clone(), bvs[9].clone());
745            let (s1_2, c1_2) = opt_full_adder(bvs[11].clone(), bvs[12].clone(), s0);
746            let (s2_2, c2_2) = opt_full_adder(bvs[16].clone(), s1, c0);
747            let (s3_2, c3_2) = opt_full_adder(bvs[21].clone(), s2, c1);
748            let (s4_2, c4_2) = opt_full_adder(bvs[26].clone(), s3, c2);
749            let (s5_2, c5_2) = opt_full_adder(bvs[30].clone(), bvs[31].clone(), c3);
750            //       5 s0 c0 c1 c2 c3 c4 c5
751            //    2  4  7 s1 s2 s3 s4 s5 33
752            // 0  1  3  6 10 15 20 25 29 32 34
753            let (s0_3, c0_3) = half_adder(bvs[4].clone(), bvs[5].clone());
754            let (s1_3, c1_3) = opt_full_adder(bvs[6].clone(), bvs[7].clone(), s0_2);
755            let (s2_3, c2_3) = opt_full_adder(bvs[10].clone(), s1_2, c0_2);
756            let (s3_3, c3_3) = opt_full_adder(bvs[15].clone(), s2_2, c1_2);
757            let (s4_3, c4_3) = opt_full_adder(bvs[20].clone(), s3_2, c2_2);
758            let (s5_3, c5_3) = opt_full_adder(bvs[25].clone(), s4_2, c3_2);
759            let (s6_3, c6_3) = opt_full_adder(bvs[29].clone(), s5_2, c4_2);
760            let (s7_3, c7_3) = opt_full_adder(bvs[32].clone(), bvs[33].clone(), c5_2);
761            //    2 s0 c0 c1 c2 c3 c4 c5 c6 c7
762            // 0  1  3 s1 s2 s3 s4 s5 s6 s7 34
763            let a = IntExprNode::<isize, U11, false> {
764                creator: exp_ec.clone(),
765                indexes: GenericArray::clone_from_slice(&[
766                    bvs[0].index,
767                    bvs[1].index,
768                    bvs[3].index,
769                    s1_3.index,
770                    s2_3.index,
771                    s3_3.index,
772                    s4_3.index,
773                    s5_3.index,
774                    s6_3.index,
775                    s7_3.index,
776                    bvs[34].index,
777                ]),
778            };
779            let b = IntExprNode::<isize, U11, false> {
780                creator: exp_ec.clone(),
781                indexes: GenericArray::clone_from_slice(&[
782                    0,
783                    bvs[2].index,
784                    s0_3.index,
785                    c0_3.index,
786                    c1_3.index,
787                    c2_3.index,
788                    c3_3.index,
789                    c4_3.index,
790                    c5_3.index,
791                    c6_3.index,
792                    c7_3.index,
793                ]),
794            };
795            let exp = a.mod_add(b);
796
797            assert_eq!(exp.indexes.as_slice(), res.as_slice());
798            assert_eq!(*exp_ec.borrow(), *ec.borrow());
799        }
800    }
801}
cnfgen/int_utils.rs

cnfgen/
int_utils.rs
