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

feat(th-bool): more direct encoding of =>

Browse source
This commit is contained in:
Simon Cruanes 2021-03-18 18:04:20 -04:00
parent 0b351ea67e
commit 9fea7462dc
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

@ -219,12 +219,16 @@ module Make(A : ARG) : S with module A = A = struct
add_clause (Lit.neg proxy :: subs);
proxy
| B_imply (args, u) ->
let t' =
let args =
args |> Iter.map (not_ self.tst) |> IArray.of_iter
in
or_a self.tst @@ IArray.append args (IArray.singleton u) in
get_lit t'
(* transform into [¬args \/ u] on the fly *)
let args = args |> Iter.map get_lit |> Iter.map Lit.neg |> Iter.to_list in
let u = get_lit u in
let subs = u :: args in
(* now the or-encoding *)
let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"implies_" self in
(* add clauses *)
List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs;
add_clause (Lit.neg proxy :: subs);
proxy
| B_ite _ | B_eq _ | B_neq _ -> mk_lit t
| B_equiv (a,b) -> equiv_ ~for_:t ~is_xor:false a b
| B_xor (a,b) -> equiv_ ~for_:t ~is_xor:true a b