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

refactor(th-bool): remove cache and most recursion

Browse source 
the preprocessing framework already takes care of both.
This commit is contained in:
Simon Cruanes 2021-08-22 15:50:42 -04:00
parent baecce0946
commit fa04cb7997
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 6 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -102,13 +102,11 @@ module Make(A : ARG) : S with module A = A = struct
type state = { type state = {
tst: T.store; tst: T.store;
ty_st: Ty.store; ty_st: Ty.store;
cnf: Lit.t T.Tbl.t; (* tseitin CNF *)
gensym: A.Gensym.t; gensym: A.Gensym.t;
} }
let create tst ty_st : state = let create tst ty_st : state =
{ tst; ty_st; { tst; ty_st;
cnf=T.Tbl.create 128;
gensym=A.Gensym.create tst; gensym=A.Gensym.create tst;
} }
@ -220,31 +218,8 @@ module Make(A : ARG) : S with module A = A = struct
let mk_lit = PA.mk_lit in let mk_lit = PA.mk_lit in
let rec get_lit_opt (t:T.t) : Lit.t option = (* handle boolean equality *)
let t_abs, t_sign = T.abs self.tst t in let equiv_ si ~is_xor ~for_t t_a t_b : Lit.t =
let lit_abs =
match T.Tbl.find self.cnf t_abs with
| lit -> Some lit (* cached *)
| exception Not_found ->
(* compute and cache, if present *)
let lit = get_lit_uncached si t_abs in
begin match lit with
| None -> ()
| Some lit ->
if not (T.equal (Lit.term lit) t_abs) then (
T.Tbl.add self.cnf t_abs lit;
Log.debugf 20
(fun k->k "(@[sidekick.bool.add-lit@ :lit %a@ :for-t %a@])"
Lit.pp lit T.pp t_abs);
);
end;
lit
in
let lit = if t_sign then lit_abs else CCOpt.map Lit.neg lit_abs in
lit
and equiv_ si ~is_xor ~for_t t_a t_b : Lit.t =
let a = mk_lit t_a in let a = mk_lit t_a in
let b = mk_lit t_b in let b = mk_lit t_b in
let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *) let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
@ -272,14 +247,15 @@ module Make(A : ARG) : S with module A = A = struct
(if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_b] (if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_b]
else A.lemma_bool_c "eq-i-" [t_proxy]); else A.lemma_bool_c "eq-i-" [t_proxy]);
proxy proxy
in
(* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
and get_lit_uncached si t : Lit.t option = let rec get_lit_for_term_ t : Lit.t option =
match A.view_as_bool t with match A.view_as_bool t with
| B_opaque_bool _ -> None | B_opaque_bool _ -> None
| B_bool _ -> None | B_bool _ -> None
| B_not u -> | B_not u ->
let lit = get_lit_opt u in let lit = get_lit_for_term_ u in
CCOpt.map Lit.neg lit CCOpt.map Lit.neg lit
| B_and l -> | B_and l ->
@ -343,7 +319,7 @@ module Make(A : ARG) : S with module A = A = struct
| B_atom _ -> None | B_atom _ -> None
in in
begin match get_lit_opt t with begin match get_lit_for_term_ t with
| None -> None | None -> None
| Some lit -> | Some lit ->
let u = Lit.term lit in let u = Lit.term lit in