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

refactor(th_bool): cache tseitin on absolute values

Browse source
This commit is contained in:
Simon Cruanes 2019-11-01 15:53:12 -05:00
parent b9965ca709
commit 3cd79ee4c9
1 changed files with 13 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -134,15 +134,19 @@ module Make(A : ARG) : S with module A = A = struct
(* TODO: polarity? *) (* TODO: polarity? *)
let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : T.t option = let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : T.t option =
let rec get_lit (t:T.t) : Lit.t = let rec get_lit (t:T.t) : Lit.t =
match T.Tbl.find self.cnf t with let t_abs, t_sign = T.abs self.tst t in
| lit -> lit (* cached *) let lit =
| exception Not_found -> match T.Tbl.find self.cnf t_abs with
(* compute and cache *) | lit -> lit (* cached *)
let lit = get_lit_uncached t in | exception Not_found ->
if not (T.equal (Lit.term lit) (T.abs self.tst t |> fst)) then ( (* compute and cache *)
T.Tbl.add self.cnf t lit; let lit = get_lit_uncached t_abs in
); if not (T.equal (Lit.term lit) t_abs) then (
lit T.Tbl.add self.cnf t_abs lit;
);
lit
in
if t_sign then lit else Lit.neg lit
and get_lit_uncached t : Lit.t = and get_lit_uncached t : Lit.t =
match A.view_as_bool t with match A.view_as_bool t with
| B_bool b -> mk_lit (T.bool self.tst b) | B_bool b -> mk_lit (T.bool self.tst b)