From 4fd291b11795617abdf6ffc5ee7e12216db5fdde Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 25 Aug 2021 23:51:20 -0400 Subject: [PATCH] wip: continue refactor --- src/cc/Sidekick_cc.ml | 65 +++++++++------ src/cc/dune | 2 +- src/core/Sidekick_core.ml | 14 ++-- src/dune | 2 +- src/lra/sidekick_arith_lra.ml | 33 ++++---- src/smt-solver/Sidekick_smt_solver.ml | 12 +-- src/th-bool-static/Sidekick_th_bool_static.ml | 12 +-- src/th-cstor/Sidekick_th_cstor.ml | 5 +- src/th-data/Sidekick_th_data.ml | 83 ++++++++++++------- 9 files changed, 135 insertions(+), 93 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 98792614..e31608ec 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -118,28 +118,34 @@ module Make (A: CC_ARG) let alloc (self:store) (t:term) : t = let { - n_term; n_sig0; n_parents; n_root; n_next; n_size + n_term; n_sig0; n_parents; n_root; n_next; n_size; n_expl; + n_as_lit=_; n_bitfields; } = self in let n = Node0.of_int_unsafe (Vec.size n_term) in Vec.push n_term t; Vec.push n_sig0 (Opaque n); (* will be updated *) Vec.push n_parents Bag.empty; + Vec.push n_expl FL_none; NVec.push n_root n; NVec.push n_next n; VecI32.push n_size 1; + Vec.iter (fun bv -> Bitvec.ensure_size bv ((n:t:>int)+1)) n_bitfields; + assert (term self n == t); n (* dealloc node. It must be the last node allocated. *) let dealloc (self:store) (n:t) : unit = assert ((n:>int) + 1 = Vec.size self.n_term); let { - n_term; n_sig0; n_parents; n_root; n_next; n_size + n_term; n_sig0; n_parents; n_root; n_next; n_size; n_expl; + n_as_lit=_; n_bitfields=_; } = self in ignore (Vec.pop_exn n_term : term); ignore (Vec.pop_exn n_sig0 : signature); ignore (Vec.pop_exn n_parents : _ Bag.t); ignore (NVec.pop n_root : t); ignore (NVec.pop n_next : t); + ignore (Vec.pop_exn n_expl : explanation_forest_link); ignore (VecI32.pop n_size : int); () @@ -170,7 +176,9 @@ module Make (A: CC_ARG) let alloc_bitfield ~descr (self:store) : bitfield = Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr); let field = Bit_field.of_int_unsafe (Vec.size self.n_bitfields) in - Vec.push self.n_bitfields (Bitvec.create()); + let bv = Bitvec.create() in + Bitvec.ensure_size bv (Vec.size self.n_term); + Vec.push self.n_bitfields bv; field let create () : store = { @@ -315,7 +323,7 @@ module Make (A: CC_ARG) mutable on_conflict: ev_on_conflict list; mutable on_propagate: ev_on_propagate list; mutable on_is_subterm : ev_on_is_subterm list; - mutable new_merges: bool; + mutable new_merges: bool; (* true if >=1 class was modified since last check *) field_marked_explain: N.bitfield; (* used to mark traversed nodes when looking for a common ancestor *) true_ : node lazy_t; false_ : node lazy_t; @@ -424,7 +432,7 @@ module Make (A: CC_ARG) Vec.push cc.pending t let merge_classes cc t u e : unit = - if t != u && not (N.same_class cc.nstore t u) then ( + if not (N.equal t u) && not (N.same_class cc.nstore t u) then ( Log.debugf 50 (fun k->let nstore=cc.nstore in k "(@[cc.push-combine@ %a ~@ %a@ :expl %a@])" @@ -573,34 +581,35 @@ module Make (A: CC_ARG) with Not_found -> add_new_term_ cc t (* add [t] to [cc] when not present already *) - and add_new_term_ cc (t:term) : node = - assert (not @@ mem cc t); + and add_new_term_ self (t:term) : node = + assert (not @@ mem self t); Log.debugf 15 (fun k->k "(@[cc.add-term@ %a@])" Term.pp t); - let n = N.alloc cc.nstore t in + let n = N.alloc self.nstore t in (* register sub-terms, add [t] to their parent list, and return the corresponding initial signature *) - let sig0 = compute_sig0 cc n in + let sig0 = compute_sig0 self n in + N.set_sig0 self.nstore n sig0; (* remove term when we backtrack *) - on_backtrack cc + on_backtrack self (fun () -> Log.debugf 15 (fun k->k "(@[cc.remove-term@ %a@])" Term.pp t); - N.dealloc cc.nstore n; - T_tbl.remove cc.tbl t); + N.dealloc self.nstore n; + T_tbl.remove self.tbl t); (* add term to the table *) - T_tbl.add cc.tbl t n; + T_tbl.add self.tbl t n; begin match sig0 with - | Opaque _ | Bool _ -> () - | App_ho _ | App_fun _ | If _ | Eq _ | Not _ -> + | Opaque _ -> () + | App_ho _ | Bool _ | App_fun _ | If _ | Eq _ | Not _ -> (* [n] might be merged with other equiv classes *) - push_pending cc n; + push_pending self n; end; - List.iter (fun f -> f cc n t) cc.on_new_term; + List.iter (fun f -> f self n t) self.on_new_term; n (* compute the initial signature of the given node *) @@ -608,23 +617,25 @@ module Make (A: CC_ARG) (* add sub-term to [cc], and register [n] to its parents. Note that we return the exact sub-term, to get proper explanations, but we add to the sub-term's root's parent list. *) + let nstore = self.nstore in let deref_sub (u:term) : node = let sub = add_term_rec_ self u in (* add [n] to [sub.root]'s parent list *) begin - let sub_r = N.find self.nstore sub in - let old_parents = N.parents self.nstore sub_r in + let sub_r = N.find nstore sub in + let old_parents = N.parents nstore sub_r in if Bag.is_empty old_parents then ( (* first time it has parents: tell watchers that this is a subterm *) List.iter (fun f -> f sub u) self.on_is_subterm; ); - on_backtrack self (fun () -> N.set_parents self.nstore sub_r old_parents); - N.upd_parents self.nstore sub_r ~f:(fun p -> Bag.cons n p); + on_backtrack self (fun () -> N.set_parents nstore sub_r old_parents); + N.upd_parents nstore sub_r ~f:(fun p -> Bag.cons n p); end; sub in - begin match A.cc_view (N.term self.nstore n) with - | Bool _ | Opaque _ -> Opaque n + begin match A.cc_view (N.term nstore n) with + | Opaque _ -> Opaque n + | Bool b -> Bool b | Eq (a,b) -> let a = deref_sub a in let b = deref_sub b in @@ -673,11 +684,14 @@ module Make (A: CC_ARG) done and task_pending_ (self:t) (n:node) : unit = + Log.debugf 10 (fun k->k"task pending %a" (N.pp self.nstore) n); (* check if some parent collided *) begin match N.sig0 self.nstore n with | Opaque _ -> () (* no-op *) | Eq (a,b) -> (* if [a=b] is now true, merge [(a=b)] and [true] *) + Log.debugf 10 (fun k->k"TASK PENDING EQ %a %a (same? %B)" (N.pp self.nstore) a + (N.pp self.nstore) b (N.same_class self.nstore a b)); if N.same_class self.nstore a b then ( let expl = Expl.mk_merge a b in Log.debugf 5 @@ -786,7 +800,8 @@ module Make (A: CC_ARG) (* for each node in [r_from]'s class, make it point to [r_into] *) N.iter_class nstore r_from (fun u -> - assert (N.root nstore u == r_from); + assert (N.equal (N.root nstore u) r_from); + Log.debugf 10 (fun k->k"%a now points to %a" (N.pp nstore) u (N.pp nstore) r_into); N.set_root nstore u r_into); (* capture current state *) let r_into_old_next = N.next nstore r_into in @@ -822,7 +837,7 @@ module Make (A: CC_ARG) N.set_parents nstore r_into r_into_old_parents; (* NOTE: this must come after the restoration of [next] pointers, otherwise we'd iterate on too big a class *) - N.iter_class nstore r_from (fun u -> N.set_root nstore u r_from); + N.iter_class_ nstore r_from (fun u -> N.set_root nstore u r_from); N.set_size nstore r_into (N.size nstore r_into - N.size nstore r_from); ); end; diff --git a/src/cc/dune b/src/cc/dune index d86f371f..03f718d4 100644 --- a/src/cc/dune +++ b/src/cc/dune @@ -4,4 +4,4 @@ (name Sidekick_cc) (public_name sidekick.cc) (libraries containers iter sidekick.core sidekick.util) - (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util)) + (flags :standard -open Sidekick_util)) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index eb46e2b7..74279316 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -1132,7 +1132,7 @@ module type MONOID_ARG = sig type t (** Some type with a monoid structure *) - val pp : t Fmt.printer + val pp : SI.CC.N.store -> t Fmt.printer val name : string (** name of the monoid structure (short) *) @@ -1227,7 +1227,7 @@ end = struct | Some v -> Log.debugf 20 (fun k->k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])" - M.name (N.pp nstore) n M.pp v); + M.name (N.pp nstore) n (M.pp nstore) v); SI.CC.set_bitfield cc self.field_has_value true n; N_tbl.add self.values n v | None -> () @@ -1236,7 +1236,7 @@ end = struct (fun (n_u,m_u) -> Log.debugf 20 (fun k->k "(@[monoid[%s].on-new-term.sub@ :n %a@ :sub-t %a@ :value %a@])" - M.name (N.pp nstore) n (N.pp nstore) n_u M.pp m_u); + M.name (N.pp nstore) n (N.pp nstore) n_u (M.pp nstore) m_u); let n_u = CC.find cc n_u in if CC.get_bitfield self.cc self.field_has_value n_u then ( let m_u' = @@ -1249,12 +1249,12 @@ end = struct Error.errorf "when merging@ @[for node %a@],@ \ values %a and %a:@ conflict %a" - (N.pp nstore) n_u M.pp m_u M.pp m_u' (CC.Expl.pp nstore) expl + (N.pp nstore) n_u (M.pp nstore) m_u (M.pp nstore) m_u' (CC.Expl.pp nstore) expl | Ok m_u_merged -> Log.debugf 20 (fun k->k "(@[monoid[%s].on-new-term.sub.merged@ \ :n %a@ :sub-t %a@ :value %a@])" - M.name (N.pp nstore) n (N.pp nstore) n_u M.pp m_u_merged); + M.name (N.pp nstore) n (N.pp nstore) n_u (M.pp nstore) m_u_merged); N_tbl.add self.values n_u m_u_merged; ) else ( (* just add to [n_u] *) @@ -1275,7 +1275,7 @@ end = struct Log.debugf 5 (fun k->k "(@[monoid[%s].on_pre_merge@ (@[:n1 %a@ :val1 %a@])@ (@[:n2 %a@ :val2 %a@])@])" - M.name (N.pp nstore) n1 M.pp v1 (N.pp nstore) n2 M.pp v2); + M.name (N.pp nstore) n1 (M.pp nstore) v1 (N.pp nstore) n2 (M.pp nstore) v2); begin match M.merge cc n1 v1 n2 v2 e_n1_n2 with | Ok v' -> N_tbl.remove self.values n2; (* only keep repr *) @@ -1292,7 +1292,7 @@ end = struct let pp out (self:t) : unit = let nstore = CC.n_store self.cc in - let pp_e out (t,v) = Fmt.fprintf out "(@[%a@ :has %a@])" (N.pp nstore) t M.pp v in + let pp_e out (t,v) = Fmt.fprintf out "(@[%a@ :has %a@])" (N.pp nstore) t (M.pp nstore) v in Fmt.fprintf out "(@[%a@])" (Fmt.iter pp_e) (iter_all self) let create_and_setup ?size (solver:SI.t) : t = diff --git a/src/dune b/src/dune index 955acfd9..741c8333 100644 --- a/src/dune +++ b/src/dune @@ -1,5 +1,5 @@ (env (_ - (flags :standard -warn-error -3-32 -color always -safe-string -short-paths) + (flags :standard -warn-error -a+8+9 -w +a-4-32 -color always -safe-string -short-paths) (ocamlopt_flags :standard -O3 -color always -unbox-closures -unbox-closures-factor 20))) diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 9dc60761..4b68ac62 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -95,24 +95,27 @@ module Make(A : ARG) : S with module A = A = struct module T = A.S.T.Term module Lit = A.S.Solver_internal.Lit module SI = A.S.Solver_internal - module N = A.S.Solver_internal.CC.N + module CC = SI.CC + module N = CC.N module Tag = struct type t = | By_def | Lit of Lit.t - | CC_eq of N.t * N.t + | CC_eq of CC.t * N.t * N.t let pp out = function | By_def -> Fmt.string out "by-def" | Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l - | CC_eq (n1,n2) -> Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" N.pp n1 N.pp n2 + | CC_eq (cc,n1,n2) -> + let nstore = CC.n_store cc in + Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" (N.pp nstore) n1 (N.pp nstore) n2 - let to_lits si = function + let to_lits = function | By_def -> [] | Lit l -> [l] - | CC_eq (n1,n2) -> - SI.CC.explain_eq (SI.cc si) n1 n2 + | CC_eq (cc,n1,n2) -> + SI.CC.explain_eq cc n1 n2 end module SimpVar @@ -416,7 +419,7 @@ module Make(A : ARG) : S with module A = A = struct Profile.with1 "simplex.check-cert" SimpSolver._check_cert cert; let confl = SimpSolver.Unsat_cert.lits cert - |> CCList.flat_map (Tag.to_lits si) + |> CCList.flat_map Tag.to_lits |> List.rev_map SI.Lit.neg in let pr = A.lemma_lra (Iter.of_list confl) in @@ -428,9 +431,9 @@ module Make(A : ARG) : S with module A = A = struct (* TODO: more detailed proof certificate *) SI.propagate si acts lit ~reason:(fun() -> - let lits = CCList.flat_map (Tag.to_lits si) reason in + let lits = CCList.flat_map Tag.to_lits reason in let pr = A.lemma_lra Iter.(cons lit (of_list lits)) in - CCList.flat_map (Tag.to_lits si) reason, pr) + CCList.flat_map Tag.to_lits reason, pr) | _ -> () let check_simplex_ self si acts : SimpSolver.Subst.t = @@ -453,9 +456,10 @@ module Make(A : ARG) : S with module A = A = struct (* TODO: trivial propagations *) let add_local_eq (self:state) si acts n1 n2 : unit = - Log.debugf 20 (fun k->k "(@[lra.add-local-eq@ %a@ %a@])" N.pp n1 N.pp n2); - let t1 = N.term n1 in - let t2 = N.term n2 in + let nstore = CC.n_store (SI.cc si) in + Log.debugf 20 (fun k->k "(@[lra.add-local-eq@ %a@ %a@])" (N.pp nstore) n1 (N.pp nstore) n2); + let t1 = N.term nstore n1 in + let t2 = N.term nstore n2 in let t1, t2 = if T.compare t1 t2 > 0 then t2, t1 else t1, t2 in let le = LE.(as_linexp_id t1 - as_linexp_id t2) in @@ -463,7 +467,7 @@ module Make(A : ARG) : S with module A = A = struct let le_const = A.Q.neg le_const in let v = var_encoding_comb ~pre:"le_local_eq" self le_comb in - let lit = Tag.CC_eq (n1,n2) in + let lit = Tag.CC_eq (SI.cc si,n1,n2) in begin try let c1 = SimpSolver.Constraint.geq v le_const in @@ -611,9 +615,10 @@ module Make(A : ARG) : S with module A = A = struct SI.on_final_check si (final_check_ st); SI.on_partial_check si (partial_check_ st); SI.on_cc_is_subterm si (on_subterm st); + let nstore = CC.n_store @@ SI.cc si in SI.on_cc_post_merge si (fun _ _ n1 n2 -> - if A.has_ty_real (N.term n1) then ( + if A.has_ty_real (N.term nstore n1) then ( Backtrack_stack.push st.local_eqs (n1, n2) )); st diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index 1eface44..5508b6c9 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -612,6 +612,7 @@ module Make(A : ARG) let[@inline] solver self = self.solver let[@inline] cc self = Solver_internal.cc self.si + let[@inline] n_store self = CC.n_store (cc self) let[@inline] stats self = self.stat let[@inline] tst self = Solver_internal.tst self.si let[@inline] ty_st self = Solver_internal.ty_st self.si @@ -712,6 +713,7 @@ module Make(A : ARG) let module M = Term.Tbl in let model = M.create 128 in let {Solver_internal.tst; cc=lazy cc; mk_model=model_hooks; _} = self.si in + let nstore = n_store self in (* first, add all literals to the model using the given propositional model [lits]. *) @@ -725,13 +727,13 @@ module Make(A : ARG) let repr = CC.find cc n in (* see if a value is found already (always the case if it's a boolean) *) - match M.get model (N.term repr) with + match M.get model (N.term nstore repr) with | Some t_val -> t_val | None -> (* try each model hook *) let rec aux = function - | [] -> N.term repr + | [] -> N.term nstore repr | h :: hooks -> begin match h ~recurse:(fun _ n -> val_for_class n) self.si repr with | None -> aux hooks @@ -740,7 +742,7 @@ module Make(A : ARG) in let t_val = aux model_hooks in - M.replace model (N.term repr) t_val; (* be sure to cache the value *) + M.replace model (N.term nstore repr) t_val; (* be sure to cache the value *) t_val in @@ -748,9 +750,9 @@ module Make(A : ARG) Solver_internal.CC.all_classes (Solver_internal.cc self.si) (fun repr -> let t_val = val_for_class repr in (* value for this class *) - N.iter_class repr + N.iter_class nstore repr (fun u -> - let t_u = N.term u in + let t_u = N.term nstore u in if not (N.equal u repr) && not (Term.equal t_u t_val) then ( M.replace model t_u t_val; ))); diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 703fd9f7..126bf481 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -331,12 +331,12 @@ module Make(A : ARG) : S with module A = A = struct (* check if new terms were added to the congruence closure, that can be turned into clauses *) let check_new_terms (self:state) si (acts:SI.theory_actions) (_trail:_ Iter.t) : unit = - let cc_ = SI.cc si in + let cc = SI.cc si in + let nstore = SI.CC.n_store cc in let all_terms = - let open SI in - CC.all_classes cc_ - |> Iter.flat_map CC.N.iter_class - |> Iter.map CC.N.term + SI.CC.all_classes cc + |> Iter.flat_map (SI.CC.N.iter_class nstore) + |> Iter.map (SI.CC.N.term nstore) in let cnf_of t = let pacts = SI.preprocess_acts_of_acts si acts in @@ -350,7 +350,7 @@ module Make(A : ARG) : S with module A = A = struct Log.debugf 5 (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])" T.pp t T.pp u); - SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []); + SI.CC.merge_t cc t u (SI.CC.Expl.mk_list []); ()); end; () diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 993ce743..87196fcb 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -37,7 +37,7 @@ module Make(A : ARG) : S with module A = A = struct } let name = name - let pp out (v:t) = + let pp _nstore out (v:t) = Fmt.fprintf out "(@[cstor %a@ :term %a@])" Fun.pp v.cstor T.pp v.t (* attach data to constructor terms *) @@ -49,9 +49,10 @@ module Make(A : ARG) : S with module A = A = struct | _ -> None, [] let merge cc n1 v1 n2 v2 e_n1_n2 : _ result = + let nstore = SI.CC.n_store cc in Log.debugf 5 (fun k->k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])" - name N.pp n1 T.pp v1.t N.pp n2 T.pp v2.t); + name (N.pp nstore) n1 T.pp v1.t (N.pp nstore) n2 T.pp v2.t); (* build full explanation of why the constructor terms are equal *) (* FIXME: add a (fun p -> A.lemma_cstor p …) here. probably we need [Some a=Some b => a=b] as a lemma for inj, diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 51a3b42d..528eac7a 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -209,6 +209,7 @@ module Make(A : ARG) : S with module A = A = struct if any *) module Monoid_cstor = struct module SI = SI + module CC = SI.CC let name = "th-data.cstor" (* associate to each class a unique constructor term in the class (if any) *) @@ -218,10 +219,10 @@ module Make(A : ARG) : S with module A = A = struct c_args: N.t IArray.t; } - let pp out (v:t) = + let pp nstore out (v:t) = Fmt.fprintf out "(@[%s@ :cstor %a@ :n %a@ :args [@[%a@]]@])" - name A.Cstor.pp v.c_cstor N.pp v.c_n - (Util.pp_iarray N.pp) v.c_args + name A.Cstor.pp v.c_cstor (N.pp nstore) v.c_n + (Util.pp_iarray (N.pp nstore)) v.c_args (* attach data to constructor terms *) let of_term cc n (t:T.t) : _ option * _ list = @@ -232,9 +233,10 @@ module Make(A : ARG) : S with module A = A = struct | _ -> None, [] let merge cc n1 c1 n2 c2 e_n1_n2 : _ result = + let nstore = CC.n_store cc in Log.debugf 5 (fun k->k "(@[%s.merge@ (@[:c1 %a@ %a@])@ (@[:c2 %a@ %a@])@])" - name N.pp n1 pp c1 N.pp n2 pp c2); + name (N.pp nstore) n1 (pp nstore) c1 (N.pp nstore) n2 (pp nstore) c2); (* build full explanation of why the constructor terms are equal *) (* TODO: have a sort of lemma (injectivity) here to justify this in the proof *) let expl = @@ -284,14 +286,17 @@ module Make(A : ARG) : S with module A = A = struct parent_select: select list; (* parents that are [select] *) } - let pp_select out s = Fmt.fprintf out "(@[sel[%d]-%a@ :n %a@])" s.sel_idx A.Cstor.pp s.sel_cstor N.pp s.sel_n - let pp_is_a out s = Fmt.fprintf out "(@[is-%a@ :n %a@])" A.Cstor.pp s.is_a_cstor N.pp s.is_a_n - let pp out (v:t) = + let pp_select nstore out s = + Fmt.fprintf out "(@[sel[%d]-%a@ :n %a@])" + s.sel_idx A.Cstor.pp s.sel_cstor (N.pp nstore) s.sel_n + let pp_is_a nstore out s = + Fmt.fprintf out "(@[is-%a@ :n %a@])" A.Cstor.pp s.is_a_cstor (N.pp nstore) s.is_a_n + let pp nstore out (v:t) = Fmt.fprintf out "(@[%s@ @[:sel [@[%a@]]@]@ @[:is-a [@[%a@]]@]@])" name - (Util.pp_list pp_select) v.parent_select - (Util.pp_list pp_is_a) v.parent_is_a + (Util.pp_list @@ pp_select nstore) v.parent_select + (Util.pp_list @@ pp_is_a nstore) v.parent_is_a (* attach data to constructor terms *) let of_term cc n (t:T.t) : _ option * _ list = @@ -313,9 +318,10 @@ module Make(A : ARG) : S with module A = A = struct | T_cstor _ | T_other _ -> None, [] let merge cc n1 v1 n2 v2 _e : _ result = + let nstore = SI.CC.n_store cc in Log.debugf 5 (fun k->k "(@[%s.merge@ @[:c1 %a %a@]@ @[:c2 %a %a@]@])" - name N.pp n1 pp v1 N.pp n2 pp v2); + name (N.pp nstore) n1 (pp nstore) v1 (N.pp nstore) n2 (pp nstore) v2); let parent_is_a = v1.parent_is_a @ v2.parent_is_a in let parent_select = v1.parent_select @ v2.parent_select in Ok {parent_is_a; parent_select;} @@ -371,6 +377,7 @@ module Make(A : ARG) : S with module A = A = struct 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] *) + let nstore = SI.CC.n_store cc in match A.view_as_data t with | T_is_a (c_t, u) -> let n_u = SI.CC.add_term cc u in @@ -382,7 +389,7 @@ module Make(A : ARG) : S with module A = A = struct 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@ :t %a@ :to %B@ :n %a@ :sub-cstor %a@])" - name T.pp t is_true N.pp n Monoid_cstor.pp cstor); + name T.pp t is_true (N.pp nstore) n (Monoid_cstor.pp nstore) cstor); SI.CC.merge cc n (SI.CC.n_bool cc is_true) Expl.(mk_theory @@ mk_merge n_u cstor.c_n) end @@ -393,7 +400,7 @@ module Make(A : ARG) : S with module A = A = struct | 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); + name (N.pp nstore) n i A.Cstor.pp c_t); assert (i < IArray.length cstor.c_args); let u_i = IArray.get cstor.c_args i in SI.CC.merge cc n u_i Expl.(mk_theory @@ mk_merge n_u cstor.c_n) @@ -409,11 +416,13 @@ module Make(A : ARG) : S with module A = A = struct | _ -> assert false let on_pre_merge (self:t) (cc:SI.CC.t) acts n1 n2 expl : unit = + let nstore = SI.CC.n_store cc in 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-merge.is-a.reduce@ %a@ :to %B@ :n1 %a@ :n2 %a@ :sub-cstor %a@])" - name Monoid_parents.pp_is_a is_a2 is_true N.pp n1 N.pp n2 Monoid_cstor.pp c1); + name (Monoid_parents.pp_is_a nstore) is_a2 is_true + (N.pp nstore) n1 (N.pp nstore) n2 (Monoid_cstor.pp nstore) c1); SI.CC.merge cc is_a2.is_a_n (SI.CC.n_bool cc is_true) Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2; mk_merge n2 is_a2.is_a_arg] |> mk_theory) @@ -422,7 +431,7 @@ module Make(A : ARG) : S with module A = A = struct if A.Cstor.equal c1.c_cstor sel2.sel_cstor then ( Log.debugf 5 (fun k->k "(@[%s.on-merge.select.reduce@ :n2 %a@ :sel get[%d]-%a@])" - name N.pp n2 sel2.sel_idx Monoid_cstor.pp c1); + name (N.pp nstore) n2 sel2.sel_idx (Monoid_cstor.pp nstore) c1); assert (sel2.sel_idx < IArray.length c1.c_args); let u_i = IArray.get c1.c_args sel2.sel_idx in SI.CC.merge cc sel2.sel_n u_i @@ -437,7 +446,8 @@ module Make(A : ARG) : S with module A = A = struct | 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); + name (N.pp nstore) n1 (Monoid_cstor.pp nstore) c1 + (N.pp nstore) n2 (Monoid_parents.pp nstore) 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 @@ -459,14 +469,16 @@ module Make(A : ARG) : S with module A = A = struct type graph = node N_tbl.t - let pp_node out (n:node) = + let pp_node nstore out (n:node) = + let ppn = N.pp nstore in Fmt.fprintf out "(@[node@ :repr %a@ :cstor_n %a@ @[:cstor_args %a@]@])" - N.pp n.repr N.pp n.cstor_n - Fmt.(Dump.list @@ hvbox @@ pair ~sep:(return "@ --> ") N.pp N.pp) n.cstor_args - let pp_path = Fmt.Dump.(list@@pair N.pp pp_node) - let pp_graph out (g:graph) : unit = + ppn n.repr ppn n.cstor_n + Fmt.(Dump.list @@ hvbox @@ pair ~sep:(return "@ --> ") ppn ppn) n.cstor_args + let pp_path nstore = Fmt.Dump.(list@@pair (N.pp nstore) (pp_node nstore)) + let pp_graph nstore out (g:graph) : unit = let pp_entry out (n,node) = - Fmt.fprintf out "@[<1>@[graph_node[%a]@]@ := %a@]" N.pp n pp_node node + Fmt.fprintf out "@[<1>@[graph_node[%a]@]@ := %a@]" + (N.pp nstore) n (pp_node nstore) node in if N_tbl.length g = 0 then ( Fmt.string out "(graph ø)" @@ -475,6 +487,7 @@ module Make(A : ARG) : S with module A = A = struct ) let mk_graph (self:t) cc : graph = + let nstore = SI.CC.n_store cc in let g: graph = N_tbl.create ~size:32 () in let traverse_sub cstor : _ list = IArray.to_list_map @@ -485,7 +498,7 @@ module Make(A : ARG) : S with module A = A = struct (* populate tbl with [repr->node] *) ST_cstors.iter_all self.cstors (fun (repr, cstor) -> - assert (N.is_root repr); + assert (N.is_root nstore repr); assert (not @@ N_tbl.mem g repr); let node = { repr; cstor_n=cstor.Monoid_cstor.c_n; @@ -498,13 +511,14 @@ module Make(A : ARG) : S with module A = A = struct let check (self:t) (solver:SI.t) (acts:SI.theory_actions) : unit = let cc = SI.cc solver in + let nstore = SI.CC.n_store cc in (* create graph *) let g = mk_graph self cc in Log.debugf 50 - (fun k->k"(@[%s.acyclicity.graph@ %a@])" name pp_graph g); + (fun k->k"(@[%s.acyclicity.graph@ %a@])" name (pp_graph nstore) g); (* traverse the graph, looking for cycles *) let rec traverse ~path (n:N.t) (r:repr) : unit = - assert (N.is_root r); + assert (N.is_root nstore r); match N_tbl.find g r with | exception Not_found -> () | {flag=Done; _} -> () (* no need *) @@ -523,7 +537,7 @@ module Make(A : ARG) : S with module A = A = struct Stat.incr self.stat_acycl_conflict; Log.debugf 5 (fun k->k "(@[%s.acyclicity.raise_confl@ %a@ @[:path %a@]@])" - name Expl.pp expl pp_path path); + name (Expl.pp nstore) expl (pp_path nstore) path); SI.CC.raise_conflict_from_expl cc acts expl | {flag=New; _} as node_r -> node_r.flag <- Open; @@ -559,7 +573,8 @@ module Make(A : ARG) : S with module A = A = struct (* add clauses [∨_c is-c(n)] and [¬(is-a n) ∨ ¬(is-b n)] *) let decide_class_ (self:t) (solver:SI.t) acts (n:N.t) : unit = - let t = N.term n in + let nstore = SI.CC.n_store (SI.cc solver) in + let t = N.term nstore n in (* [t] might have been expanded already, in case of duplicates in [l] *) if not @@ T.Tbl.mem self.case_split_done t then ( T.Tbl.add self.case_split_done t (); @@ -589,6 +604,7 @@ module Make(A : ARG) : S with module A = A = struct let on_final_check (self:t) (solver:SI.t) (acts:SI.theory_actions) trail = Profile.with_ "data.final-check" @@ fun () -> check_is_a self solver acts trail; + let nstore = SI.CC.n_store (SI.cc solver) in (* acyclicity check first *) Acyclicity_.check self solver acts; @@ -600,7 +616,7 @@ module Make(A : ARG) : S with module A = A = struct |> Iter.filter (fun n -> not (ST_cstors.mem self.cstors n) && - not (T.Tbl.mem self.case_split_done (N.term n))) + not (T.Tbl.mem self.case_split_done (N.term nstore n))) |> Iter.to_rev_list in begin match remaining_to_decide with @@ -611,7 +627,8 @@ module Make(A : ARG) : S with module A = A = struct () | l -> Log.debugf 10 - (fun k->k "(@[%s.final-check.must-decide@ %a@])" name (Util.pp_list N.pp) l); + (fun k->k "(@[%s.final-check.must-decide@ %a@])" + name (Util.pp_list (N.pp nstore)) l); Profile.instant "data.case-split"; List.iter (decide_class_ self solver acts) l end; @@ -621,21 +638,21 @@ module Make(A : ARG) : S with module A = A = struct N_tbl.to_iter self.to_decide_for_complete_model |> Iter.map (fun (n,_) -> SI.cc_find solver n) |> Iter.filter - (fun n -> not (T.Tbl.mem self.case_split_done (N.term n)) + (fun n -> not (T.Tbl.mem self.case_split_done (N.term nstore n)) && not (ST_cstors.mem self.cstors n)) |> Iter.head in match next_decision with | None -> () (* all decided *) | Some n -> - let t = N.term n in + let t = N.term nstore n in Profile.instant "data.decide"; (* use a constructor that will not lead to an infinite loop *) let base_cstor = match Card.base_cstor self.cards (T.ty t) with - | None -> Error.errorf "th-data:@ %a should have base cstor" N.pp n + | None -> Error.errorf "th-data:@ %a should have base cstor" (N.pp nstore) n | Some c -> c in let cstor_app = @@ -657,11 +674,13 @@ module Make(A : ARG) : S with module A = A = struct let on_model_gen (self:t) ~recurse (si:SI.t) (n:N.t) : T.t option = (* TODO: option to complete model or not (by picking sth at leaves)? *) let cc = SI.cc si in + let nstore = SI.CC.n_store cc in let repr = SI.CC.find cc n in match ST_cstors.get self.cstors repr with | None -> None | Some c -> - Log.debugf 20 (fun k->k "(@[th-data.mk-model.find-cstor@ %a@])" Monoid_cstor.pp c); + Log.debugf 20 (fun k->k "(@[th-data.mk-model.find-cstor@ %a@])" + (Monoid_cstor.pp nstore) c); let args = IArray.map (recurse si) c.c_args in let t = A.mk_cstor self.tst c.c_cstor args in Some t