diff options
Diffstat (limited to 'proofs/signatures/th_bv_bitblast.plf')
| -rw-r--r-- | proofs/signatures/th_bv_bitblast.plf | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf index 3cc1ec296..2b2fe0868 100644 --- a/proofs/signatures/th_bv_bitblast.plf +++ b/proofs/signatures/th_bv_bitblast.plf @@ -533,6 +533,29 @@ (! c (^ (bblast_bvslt bx by n) f) (th_holds (iff (bvslt n x y) f)))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVCOMP +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvcomp ((x bblt) (y bblt) (n mpz)) bblt + (match x ((bbltc bx x') (match y ((bbltc by y') + (bbltc (bblast_eq_rec x' y' (iff bx by)) bbltn)) + (default (fail bblt)))) + (default (fail bblt)) + )) + +(declare bv_bbl_bvcomp (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvcomp xb yb n) rb) + (bblast_term 1 (bvcomp n x y) rb))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; BITBLASTING CONNECTORS |