add simple adder test

Author: ekiwi

patronus-sca/src/lib.rs

@@ -532,6 +532,31 @@ mod tests {
         }
     }
 
+    #[test]
+    fn test_simple_adder() {
+        let mut ctx = Context::default();
+        let a = ctx.bv_symbol("a", 2);
+        let b = ctx.bv_symbol("b", 2);
+        let word_level = ctx.add(a, b);
+        let a_0 = ctx.slice(a, 0, 0);
+        let a_1 = ctx.slice(a, 1, 1);
+        let b_0 = ctx.slice(b, 0, 0);
+        let b_1 = ctx.slice(b, 1, 1);
+        let gate_level_0 = ctx.xor(a_0, b_0);
+        let carry_1 = ctx.and(a_0, b_0);
+        let gate_level_1 = ctx.majority(a_1, b_1, carry_1);
+        let gate_level = ctx.concat(gate_level_1, gate_level_0);
+        let equality = ctx.equal(word_level, gate_level);
+
+        let problem = ScaEqualityProblem {
+            equality,
+            gate_level,
+            word_level,
+        };
+
+        simplify_word_level_equality(&mut ctx, problem).unwrap();
+    }
+
     #[test]
     fn test_simplify_coward_three_add() {
         simplify_coward_smt("../inputs/coward/add_three.4_bit.smt2").unwrap();

patronus/src/expr/context.rs

@@ -308,6 +308,20 @@ impl Context {
         debug_assert_eq!(a.get_bv_type(self).unwrap(), b.get_bv_type(self).unwrap());
         self.add_expr(Expr::BVXor(a, b, b.get_bv_type(self).unwrap()))
     }
+
+    pub fn xor3(&mut self, a: ExprRef, b: ExprRef, c: ExprRef) -> ExprRef {
+        let x = self.xor(a, b);
+        self.xor(x, c)
+    }
+
+    pub fn majority(&mut self, a: ExprRef, b: ExprRef, c: ExprRef) -> ExprRef {
+        let a_and_b = self.and(a, b);
+        let a_and_c = self.and(a, c);
+        let b_and_c = self.and(b, c);
+        let x = self.or(a_and_b, a_and_c);
+        self.or(x, b_and_c)
+    }
+
     pub fn shift_left(&mut self, a: ExprRef, b: ExprRef) -> ExprRef {
         debug_assert_eq!(a.get_bv_type(self).unwrap(), b.get_bv_type(self).unwrap());
         self.add_expr(Expr::BVShiftLeft(a, b, b.get_bv_type(self).unwrap()))
@@ -512,6 +526,12 @@ impl<'a> Builder<'a> {
     pub fn xor(&self, a: ExprRef, b: ExprRef) -> ExprRef {
         self.ctx.borrow_mut().xor(a, b)
     }
+    pub fn xor3(&mut self, a: ExprRef, b: ExprRef, c: ExprRef) -> ExprRef {
+        self.ctx.borrow_mut().xor3(a, b, c)
+    }
+    pub fn majority(&mut self, a: ExprRef, b: ExprRef, c: ExprRef) -> ExprRef {
+        self.ctx.borrow_mut().majority(a, b, c)
+    }
     pub fn shift_left(&self, a: ExprRef, b: ExprRef) -> ExprRef {
         self.ctx.borrow_mut().shift_left(a, b)
     }