sca benchmarks and implementation

This contains work from the last two weeks

Author: ekiwi

Cargo.toml

@@ -1,6 +1,6 @@
 [workspace]
 resolver = "2"
-members = ["patronus", "patronus-egraphs", "patronus-dse", "tools/bmc", "tools/egraphs-cond-synth", "tools/sim", "tools/simplify", "tools/view", "python"]
+members = ["patronus", "patronus-egraphs", "patronus-dse", "patronus-sca", "tools/bmc", "tools/egraphs-cond-synth", "tools/sim", "tools/simplify", "tools/view", "python"]
 
 [workspace.package]
 edition = "2024"

inputs/coward/add_three.2_bit.smt2

@@ -0,0 +1,64 @@
+; solver scope 0
+(declare-const tmp (_ BitVec 2))
+(declare-const tmp_0 (_ BitVec 2))
+(declare-const tmp_1 (_ BitVec 2))
+(assert (let ((tmp_2 ((_ extract 0 0) tmp)))
+        (let ((tmp_3 ((_ extract 0 0) tmp_0)))
+        (let ((tmp_4 ((_ extract 0 0) tmp_1)))
+        (let ((tmp_5 (bvand tmp_4 tmp_3)))
+        (let ((tmp_6 (bvxor tmp_5 #b1)))
+        (let ((tmp_7 (bvxor tmp_3 #b1)))
+        (let ((tmp_8 (bvxor tmp_4 #b1)))
+        (let ((tmp_9 (bvand tmp_8 tmp_7)))
+        (let ((tmp_10 (bvxor tmp_9 #b1)))
+        (let ((tmp_11 (bvand tmp_10 tmp_6)))
+        (let ((tmp_12 (bvand tmp_11 tmp_2)))
+        (let ((tmp_13 (bvxor tmp_12 #b1)))
+        (let ((tmp_14 (bvxor tmp_2 #b1)))
+        (let ((tmp_15 (bvxor tmp_11 #b1)))
+        (let ((tmp_16 (bvand tmp_15 tmp_14)))
+        (let ((tmp_17 (bvxor tmp_16 #b1)))
+        (let ((tmp_18 (bvand tmp_17 tmp_13)))
+        (let ((tmp_19 ((_ extract 1 1) tmp)))
+        (let ((tmp_20 ((_ extract 1 1) tmp_0)))
+        (let ((tmp_21 ((_ extract 1 1) tmp_1)))
+        (let ((tmp_22 (bvand tmp_21 tmp_20)))
+        (let ((tmp_23 (bvxor tmp_22 #b1)))
+        (let ((tmp_24 (bvxor tmp_20 #b1)))
+        (let ((tmp_25 (bvxor tmp_21 #b1)))
+        (let ((tmp_26 (bvand tmp_25 tmp_24)))
+        (let ((tmp_27 (bvxor tmp_26 #b1)))
+        (let ((tmp_28 (bvand tmp_27 tmp_23)))
+        (let ((tmp_29 (bvand tmp_28 tmp_19)))
+        (let ((tmp_30 (bvxor tmp_29 #b1)))
+        (let ((tmp_31 (bvxor tmp_19 #b1)))
+        (let ((tmp_32 (bvxor tmp_28 #b1)))
+        (let ((tmp_33 (bvand tmp_32 tmp_31)))
+        (let ((tmp_34 (bvxor tmp_33 #b1)))
+        (let ((tmp_35 (bvand tmp_34 tmp_30)))
+        (let ((tmp_36 (bvand tmp_6 tmp_13)))
+        (let ((tmp_37 (bvxor tmp_36 #b1)))
+        (let ((tmp_38 (bvand tmp_37 tmp_35)))
+        (let ((tmp_39 (bvxor tmp_38 #b1)))
+        (let ((tmp_40 (bvxor tmp_35 #b1)))
+        (let ((tmp_41 (bvand tmp_36 tmp_40)))
+        (let ((tmp_42 (bvxor tmp_41 #b1)))
+        (let ((tmp_43 (bvand tmp_42 tmp_39)))
+        (let ((tmp_44 (bvand tmp_23 tmp_30)))
+        (let ((tmp_45 (bvxor tmp_44 #b1)))
+        (let ((tmp_46 (bvand tmp_45 tmp_38)))
+        (let ((tmp_47 (bvxor tmp_46 #b1)))
+        (let ((tmp_48 (bvand tmp_44 tmp_39)))
+        (let ((tmp_49 (bvxor tmp_48 #b1)))
+        (let ((tmp_50 (bvand tmp_49 tmp_47)))
+        (let ((tmp_51 (concat tmp_50 tmp_43)))
+        (let ((tmp_52 (concat tmp_51 tmp_18)))
+        (let ((tmp_53 (concat #b0 tmp_1)))
+        (let ((tmp_54 (concat #b0 tmp_0)))
+        (let ((tmp_55 (concat #b0 tmp)))
+        (let ((tmp_56 (bvadd tmp_55 tmp_54)))
+        (let ((tmp_57 (bvadd tmp_56 tmp_53)))
+        (let ((tmp_58 (distinct tmp_57 tmp_52)))
+        tmp_58))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(reset)