From 3cd79ee4c930b0456f15abf676e4b4f6d7320abc Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 1 Nov 2019 15:53:12 -0500 Subject: [PATCH] refactor(th_bool): cache tseitin on absolute values --- src/th-bool-static/Sidekick_th_bool_static.ml | 22 +++++++++++-------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 0d436ab9..8bff46fb 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -134,15 +134,19 @@ module Make(A : ARG) : S with module A = A = struct (* TODO: polarity? *) 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 = - match T.Tbl.find self.cnf t with - | lit -> lit (* cached *) - | exception Not_found -> - (* compute and cache *) - let lit = get_lit_uncached t in - if not (T.equal (Lit.term lit) (T.abs self.tst t |> fst)) then ( - T.Tbl.add self.cnf t lit; - ); - lit + let t_abs, t_sign = T.abs self.tst t in + let lit = + match T.Tbl.find self.cnf t_abs with + | lit -> lit (* cached *) + | exception Not_found -> + (* compute and cache *) + let lit = get_lit_uncached t_abs in + if not (T.equal (Lit.term lit) t_abs) then ( + 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 = match A.view_as_bool t with | B_bool b -> mk_lit (T.bool self.tst b)