simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(th-bool): properly preprocess in equiv

Browse source
This commit is contained in:
Simon Cruanes 2022-09-09 22:16:48 -04:00
parent e94a7bd31c
commit e9c2491380
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/th-bool-static/Sidekick_th_bool_static.ml
View file

@ -164,7 +164,9 @@ end = struct
let[@inline] mk_step_ r = Proof_trace.add_step PA.proof r in let[@inline] mk_step_ r = Proof_trace.add_step PA.proof r in
(* handle boolean equality *) (* handle boolean equality *)
let equiv_ (self : state) ~is_xor ~t t_a t_b : unit = let equiv_ (self : state) ~is_xor ~t ~box_t t_a t_b : unit =
let t_a = recurse t_a in
let t_b = recurse t_b in
let a = PA.mk_lit t_a in let a = PA.mk_lit t_a in
let b = PA.mk_lit t_b in let b = PA.mk_lit t_b in
let a = let a =
@ -174,7 +176,7 @@ end = struct
a a
in in
(* [a xor b] is [(¬a) = b] *) (* [a xor b] is [(¬a) = b] *)
let lit = PA.mk_lit t in let lit = PA.mk_lit box_t in
(* proxy => a<=> b, (* proxy => a<=> b,
¬proxy => a xor b *) ¬proxy => a xor b *)
@ -298,11 +300,13 @@ end = struct
Some box_t Some box_t
| B_eq _ | B_neq _ -> None | B_eq _ | B_neq _ -> None
| B_equiv (a, b) -> | B_equiv (a, b) ->
equiv_ self ~t ~is_xor:false a b; let box_t = Box.box self.tst t in
None (* FIXME *) equiv_ self ~t ~box_t ~is_xor:false a b;
Some box_t
| B_xor (a, b) -> | B_xor (a, b) ->
equiv_ self ~t ~is_xor:true a b; let box_t = Box.box self.tst t in
None (* FIXME *) equiv_ self ~t ~box_t ~is_xor:true a b;
Some box_t
| B_atom _ -> None | B_atom _ -> None
let create_and_setup ~id:_ si = let create_and_setup ~id:_ si =