From 91e9b6cc2c4319c5f35d998ec00a1dde9fb62ca1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 07:08:23 -0600 Subject: [PATCH] feat: initial support for is-a/select --- src/cc/Sidekick_cc.ml | 31 ++++++++------- src/core/Sidekick_core.ml | 9 ++++- src/main/sidekick_version.ml | 2 +- src/th-data/Sidekick_th_data.ml | 70 +++++++++++++++++++++++++++++++-- 4 files changed, 92 insertions(+), 20 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 64b587c5..43cacb61 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -279,8 +279,9 @@ module Make (A: CC_ARG) and ev_on_propagate = t -> lit -> (unit -> lit list) -> unit let[@inline] size_ (r:repr) = r.n_size - let[@inline] true_ cc = Lazy.force cc.true_ - let[@inline] false_ cc = Lazy.force cc.false_ + let[@inline] n_true cc = Lazy.force cc.true_ + let[@inline] n_false cc = Lazy.force cc.false_ + let n_bool cc b = if b then n_true cc else n_false cc let[@inline] term_state cc = cc.tst let allocate_bitfield ~descr cc = Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr); @@ -557,7 +558,7 @@ module Make (A: CC_ARG) n.n_as_lit <- Some lit let n_is_bool (self:t) n : bool = - N.equal n (true_ self) || N.equal n (false_ self) + N.equal n (n_true self) || N.equal n (n_false self) (* main CC algo: add terms from [pending] to the signature table, check for collisions *) @@ -581,17 +582,17 @@ module Make (A: CC_ARG) let expl = Expl.mk_merge a b in Log.debugf 5 (fun k->k "(pending.eq@ %a@ :r1 %a@ :r2 %a@])" N.pp n N.pp a N.pp b); - merge_classes cc n (true_ cc) expl + merge_classes cc n (n_true cc) expl ) | Some (Not u) -> (* [u = bool ==> not u = not bool] *) let r_u = find_ u in - if N.equal r_u (true_ cc) then ( - let expl = Expl.mk_merge u (true_ cc) in - merge_classes cc n (false_ cc) expl - ) else if N.equal r_u (false_ cc) then ( - let expl = Expl.mk_merge u (false_ cc) in - merge_classes cc n (true_ cc) expl + if N.equal r_u (n_true cc) then ( + let expl = Expl.mk_merge u (n_true cc) in + merge_classes cc n (n_false cc) expl + ) else if N.equal r_u (n_false cc) then ( + let expl = Expl.mk_merge u (n_false cc) in + merge_classes cc n (n_true cc) expl ) | Some s0 -> (* update the signature by using [find] on each sub-node *) @@ -622,8 +623,8 @@ module Make (A: CC_ARG) assert (N.is_root rb); Stat.incr cc.count_merge; (* check we're not merging [true] and [false] *) - if (N.equal ra (true_ cc) && N.equal rb (false_ cc)) || - (N.equal rb (true_ cc) && N.equal ra (false_ cc)) then ( + if (N.equal ra (n_true cc) && N.equal rb (n_false cc)) || + (N.equal rb (n_true cc) && N.equal ra (n_false cc)) then ( Log.debugf 5 (fun k->k "(@[cc.merge.true_false_conflict@ \ @[:r1 %a@ :t1 %a@]@ @[:r2 %a@ :t2 %a@]@ :e_ab %a@])" @@ -644,9 +645,9 @@ module Make (A: CC_ARG) in (* when merging terms with [true] or [false], possibly propagate them to SAT *) let merge_bool r1 t1 r2 t2 = - if N.equal r1 (true_ cc) then ( + if N.equal r1 (n_true cc) then ( propagate_bools cc acts r2 t2 r1 t1 e_ab true - ) else if N.equal r1 (false_ cc) then ( + ) else if N.equal r1 (n_false cc) then ( propagate_bools cc acts r2 t2 r1 t1 e_ab false ) in @@ -788,7 +789,7 @@ module Make (A: CC_ARG) merge_classes cc a b (Expl.mk_lit lit) | _ -> (* equate t and true/false *) - let rhs = if sign then true_ cc else false_ cc in + let rhs = if sign then n_true cc else n_false cc in let n = add_term cc t in (* TODO: ensure that this is O(1). basically, just have [n] point to true/false and thus acquire diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 2688a5db..165f025f 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -282,6 +282,10 @@ module type CC_S = sig it must be a theory tautology that [expl ==> absurd]. To be used in theories. *) + val n_true : t -> N.t + val n_false : t -> N.t + val n_bool : t -> bool -> N.t + val merge : t -> N.t -> N.t -> Expl.t -> unit (** Merge these two nodes given this explanation. It must be a theory tautology that [expl ==> n1 = n2]. @@ -715,7 +719,10 @@ end = struct assert (if res then N_tbl.mem self.values n else true); res - let get self n = N_tbl.get self.values n + let get self n = + if N.get_field self.field_has_value n + then N_tbl.get self.values n + else None let on_new_term self cc n (t:T.t) : unit = let maybe_m, l = M.of_term n t in diff --git a/src/main/sidekick_version.ml b/src/main/sidekick_version.ml index 2c10c6ef..068fdc87 100644 --- a/src/main/sidekick_version.ml +++ b/src/main/sidekick_version.ml @@ -1,2 +1,2 @@ -let version = {git|858ffb6f2587ca5593417be1c9f95fe727390e9e +let version = {git|6aafaad48f3f58db2eec039347a42ba1c4511a6c |git} \ No newline at end of file diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 1ede288c..f7f0ac78 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -313,15 +313,78 @@ module Make(A : ARG) : S with module A = A = struct ) | _ -> () - let on_new_term self _solver n t = - on_new_term_look_at_ty self n t; - () + let on_new_term (self:t) cc (n:N.t) (t:T.t) : unit = + on_new_term_look_at_ty self n t; (* might have to decide [t] *) + match A.view_as_data t with + | T_is_a (c_t, u) -> + let n_u = SI.CC.add_term cc u in + let repr_u = SI.CC.find cc n_u in + begin match ST_cstors.get self.cstors repr_u with + | None -> () + | Some cstor -> + let is_true = A.Cstor.equal cstor.c_cstor c_t in + Log.debugf 5 + (fun k->k "(@[%s.on-new-term.is-a.reduce@ :to %B@ :n %a@ :sub-cstor %a@])" + name is_true N.pp n Monoid_cstor.pp cstor); + SI.CC.merge cc n (SI.CC.n_bool cc is_true) (Expl.mk_merge n_u repr_u) + end + | T_select (c_t, i, u) -> + let n_u = SI.CC.add_term cc u in + let repr_u = SI.CC.find cc n_u in + begin match ST_cstors.get self.cstors repr_u with + | Some cstor when A.Cstor.equal cstor.c_cstor c_t -> + Log.debugf 5 + (fun k->k "(@[%s.on-new-term.select.reduce@ :n %a@ :sel get[%d]-%a@])" + name N.pp n i A.Cstor.pp c_t); + assert (i < IArray.length cstor.c_args); + let u_i = IArray.get cstor.c_args i in + let n_u_i = SI.CC.add_term cc u_i in + SI.CC.merge cc n n_u_i (Expl.mk_merge n_u repr_u) + | _ -> () + end + | T_cstor _ | T_other _ -> () let cstors_of_ty (ty:Ty.t) : A.Cstor.t Iter.t = match A.as_datatype ty with | Ty_data {cstors} -> cstors | _ -> assert false + let on_pre_merge (self:t) (cc:SI.CC.t) acts n1 n2 expl : unit = + let merge_is_a n1 (c1:Monoid_cstor.t) n2 (is_a2:Monoid_parents.is_a) = + let is_true = A.Cstor.equal c1.c_cstor is_a2.is_a_cstor in + Log.debugf 50 + (fun k->k "(@[%s.on-new-term.is-a.reduce@ :to %B@ :n %a@ :sub-cstor %a@])" + name is_true N.pp n2 Monoid_cstor.pp c1); + SI.CC.merge cc n2 (SI.CC.n_bool cc is_true) + Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n2 is_a2.is_a_n]) + in + let merge_select n1 (c1:Monoid_cstor.t) n2 (sel2:Monoid_parents.select) = + if A.Cstor.equal c1.c_cstor sel2.sel_cstor then ( + Log.debugf 5 + (fun k->k "(@[%s.on-new-term.select.reduce@ :n %a@ :sel get[%d]-%a@])" + name N.pp n2 sel2.sel_idx Monoid_cstor.pp c1); + assert (sel2.sel_idx < IArray.length c1.c_args); + let u_i = IArray.get c1.c_args sel2.sel_idx in + let n_u_i = SI.CC.add_term cc u_i in + SI.CC.merge cc n2 n_u_i + Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n2 sel2.sel_n]); + ) + in + let merge_c_p n1 n2 = + match ST_cstors.get self.cstors n1, ST_parents.get self.parents n2 with + | None, _ + | _, None -> () + | Some c1, Some p2 -> + Log.debugf 50 + (fun k->k "(@[%s.pre-merge@ @[:n1 %a@ :c1 %a@]@ @[:n2 %a@ :p2 %a@]@])" + name N.pp n1 Monoid_cstor.pp c1 N.pp n2 Monoid_parents.pp p2); + List.iter (fun is_a2 -> merge_is_a n1 c1 n2 is_a2) p2.parent_is_a; + List.iter (fun s2 -> merge_select n1 c1 n2 s2) p2.parent_select; + in + merge_c_p n1 n2; + merge_c_p n2 n1; + () + module Acyclicity_ = struct type st = { n: N.t; @@ -462,6 +525,7 @@ module Make(A : ARG) : S with module A = A = struct } in Log.debugf 1 (fun k->k "(setup :%s)" name); SI.on_cc_new_term solver (on_new_term self); + SI.on_cc_pre_merge solver (on_pre_merge self); SI.on_final_check solver (on_final_check self); self