diff options
author | Guy <katz911@gmail.com> | 2016-06-03 14:27:00 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-03 14:27:00 -0700 |
commit | 8bfab32eed06973d53ce8ae066a9a26d4ae8a489 (patch) | |
tree | 4fb698b165bfe4aa80560d91f7334f27965dc641 /proofs/signatures/th_bv.plf | |
parent | 90b909a89c78c75afae69e119feea20b478c0795 (diff) |
Better infrastructure for proving constant disequality.
Added support for the BV case
Diffstat (limited to 'proofs/signatures/th_bv.plf')
-rw-r--r-- | proofs/signatures/th_bv.plf | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index 7f478d823..6012e052a 100644 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -49,6 +49,25 @@ (! v bv (term (BitVec n))))) +(program bv_constants_are_disequal ((x bv) (y bv)) formula + (match x + (bvn (fail formula)) + ((bvc bx x') + (match y + (bvn (fail formula)) + ((bvc by y') (match bx + (b0 (match by (b0 (bv_constants_are_disequal x' y')) (b1 (true)))) + (b1 (match by (b0 (true)) (b1 (bv_constants_are_disequal x' y')))) + )) + )) +)) + +(declare bv_disequal_constants + (! n mpz + (! x bv + (! y bv + (! c (^ (bv_constants_are_disequal x y) true) + (th_holds (not (= (BitVec n) (a_bv n x) (a_bv n y))))))))) ; a bv variable (declare var_bv type) |