From 633a658e0c0c94e4d1611fb85410515c3d64ea8a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 15 Jul 2022 23:51:53 -0400 Subject: [PATCH] wip: use new sigs --- src/cc/Sidekick_cc.ml | 411 ++++++++---- src/cc/Sidekick_cc.mli | 21 +- src/cc/dune | 2 +- src/core/Sidekick_core.ml | 1021 +----------------------------- src/core/dune | 4 +- src/mini-cc/Sidekick_mini_cc.ml | 6 +- src/mini-cc/Sidekick_mini_cc.mli | 8 +- src/mini-cc/dune | 2 +- 8 files changed, 326 insertions(+), 1149 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 606cd5b5..d2f1ea2f 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -1,41 +1,37 @@ -open Sidekick_core -module View = Sidekick_core.CC_view +include Sidekick_sigs_cc +open View -type ('f, 't, 'ts) view = ('f, 't, 'ts) View.t = - | Bool of bool - | App_fun of 'f * 'ts - | App_ho of 't * 't - | If of 't * 't * 't - | Eq of 't * 't - | Not of 't - | Opaque of 't -(* do not enter *) - -module type S = Sidekick_core.CC_S - -module Make (A : CC_ARG) : +module Make (A : ARG) : S with module T = A.T and module Lit = A.Lit - and type proof = A.proof - and type proof_step = A.proof_step - and module Actions = A.Actions = struct + and module Proof_trace = A.Proof_trace = struct module T = A.T module Lit = A.Lit - module Actions = A.Actions - module P = Actions.P + module Proof_trace = A.Proof_trace + module Term = T.Term + module Fun = T.Fun + + open struct + (* proof rules *) + module Rules_ = A.CC.Proof_rules + module P = Sidekick_sigs_proof_trace.Utils_ (Proof_trace) + end type term = T.Term.t type value = term type term_store = T.Term.store type lit = Lit.t type fun_ = T.Fun.t - type proof = A.proof - type proof_step = A.proof_step - type actions = Actions.t + type proof = A.Proof_trace.t + type proof_step = A.Proof_trace.step_id - module Term = T.Term - module Fun = T.Fun + type actions = + (module ACTIONS + with type term = T.Term.t + and type lit = Lit.t + and type proof = proof + and type proof_step = proof_step) module Bits : sig type t = private int @@ -97,7 +93,7 @@ module Make (A : CC_ARG) : An equivalence class is represented by its "root" element, the representative. *) - and signature = (fun_, node, node list) view + and signature = (fun_, node, node list) View.t and explanation_forest_link = | FL_none @@ -117,7 +113,7 @@ module Make (A : CC_ARG) : type repr = node - module N = struct + module Class = struct type t = node let[@inline] equal (n1 : t) n2 = n1 == n2 @@ -171,11 +167,11 @@ module Make (A : CC_ARG) : (* non-recursive, inlinable function for [find] *) let[@inline] find_ (n : node) : repr = let n2 = n.n_root in - assert (N.is_root n2); + assert (Class.is_root n2); n2 let[@inline] same_class (n1 : node) (n2 : node) : bool = - N.equal (find_ n1) (find_ n2) + Class.equal (find_ n1) (find_ n2) let[@inline] find _ n = find_ n @@ -187,8 +183,9 @@ module Make (A : CC_ARG) : | E_trivial -> Fmt.string out "reduction" | E_lit lit -> Lit.pp out lit | E_congruence (n1, n2) -> - Fmt.fprintf out "(@[congruence@ %a@ %a@])" N.pp n1 N.pp n2 - | E_merge (a, b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b + Fmt.fprintf out "(@[congruence@ %a@ %a@])" Class.pp n1 Class.pp n2 + | E_merge (a, b) -> + Fmt.fprintf out "(@[merge@ %a@ %a@])" Class.pp a Class.pp b | E_merge_t (a, b) -> Fmt.fprintf out "(@[merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b @@ -199,13 +196,13 @@ module Make (A : CC_ARG) : es | E_and (a, b) -> Format.fprintf out "(@[and@ %a@ %a@])" pp a pp b | E_same_val (n1, n2) -> - Fmt.fprintf out "(@[same-value@ %a@ %a@])" N.pp n1 N.pp n2 + Fmt.fprintf out "(@[same-value@ %a@ %a@])" Class.pp n1 Class.pp n2 let mk_trivial : t = E_trivial let[@inline] mk_congruence n1 n2 : t = E_congruence (n1, n2) let[@inline] mk_merge a b : t = - if N.equal a b then + if Class.equal a b then mk_trivial else E_merge (a, b) @@ -220,7 +217,7 @@ module Make (A : CC_ARG) : let[@inline] mk_theory t u es pr = E_theory (t, u, es, pr) let[@inline] mk_same_value t u = - if N.equal t u then + if Class.equal t u then mk_trivial else E_same_val (t, u) @@ -239,7 +236,7 @@ module Make (A : CC_ARG) : module Resolved_expl = struct type t = { lits: lit list; - same_value: (N.t * N.t) list; + same_value: (Class.t * Class.t) list; pr: proof -> proof_step; } @@ -256,7 +253,7 @@ module Make (A : CC_ARG) : let { lits; same_value; pr = _ } = self in Fmt.fprintf out "(@[resolved-expl@ (@[%a@])@ :same-val (@[%a@])@])" (Util.pp_list Lit.pp) lits - (Util.pp_list @@ Fmt.Dump.pair N.pp N.pp) + (Util.pp_list @@ Fmt.Dump.pair Class.pp Class.pp) same_value ) end @@ -271,13 +268,14 @@ module Make (A : CC_ARG) : | Bool b1, Bool b2 -> b1 = b2 | App_fun (f1, []), App_fun (f2, []) -> Fun.equal f1 f2 | App_fun (f1, l1), App_fun (f2, l2) -> - Fun.equal f1 f2 && CCList.equal N.equal l1 l2 - | App_ho (f1, a1), App_ho (f2, a2) -> N.equal f1 f2 && N.equal a1 a2 - | Not a, Not b -> N.equal a b + Fun.equal f1 f2 && CCList.equal Class.equal l1 l2 + | App_ho (f1, a1), App_ho (f2, a2) -> + Class.equal f1 f2 && Class.equal a1 a2 + | Not a, Not b -> Class.equal a b | If (a1, b1, c1), If (a2, b2, c2) -> - N.equal a1 a2 && N.equal b1 b2 && N.equal c1 c2 - | Eq (a1, b1), Eq (a2, b2) -> N.equal a1 a2 && N.equal b1 b2 - | Opaque u1, Opaque u2 -> N.equal u1 u2 + Class.equal a1 a2 && Class.equal b1 b2 && Class.equal c1 c2 + | Eq (a1, b1), Eq (a2, b2) -> Class.equal a1 a2 && Class.equal b1 b2 + | Opaque u1, Opaque u2 -> Class.equal u1 u2 | Bool _, _ | App_fun _, _ | App_ho _, _ @@ -291,24 +289,25 @@ module Make (A : CC_ARG) : let module H = CCHash in match s with | Bool b -> H.combine2 10 (H.bool b) - | App_fun (f, l) -> H.combine3 20 (Fun.hash f) (H.list N.hash l) - | App_ho (f, a) -> H.combine3 30 (N.hash f) (N.hash a) - | Eq (a, b) -> H.combine3 40 (N.hash a) (N.hash b) - | Opaque u -> H.combine2 50 (N.hash u) - | If (a, b, c) -> H.combine4 60 (N.hash a) (N.hash b) (N.hash c) - | Not u -> H.combine2 70 (N.hash u) + | App_fun (f, l) -> H.combine3 20 (Fun.hash f) (H.list Class.hash l) + | App_ho (f, a) -> H.combine3 30 (Class.hash f) (Class.hash a) + | Eq (a, b) -> H.combine3 40 (Class.hash a) (Class.hash b) + | Opaque u -> H.combine2 50 (Class.hash u) + | If (a, b, c) -> + H.combine4 60 (Class.hash a) (Class.hash b) (Class.hash c) + | Not u -> H.combine2 70 (Class.hash u) let pp out = function | Bool b -> Fmt.bool out b | App_fun (f, []) -> Fun.pp out f | App_fun (f, l) -> - Fmt.fprintf out "(@[%a@ %a@])" Fun.pp f (Util.pp_list N.pp) l - | App_ho (f, a) -> Fmt.fprintf out "(@[%a@ %a@])" N.pp f N.pp a - | Opaque t -> N.pp out t - | Not u -> Fmt.fprintf out "(@[not@ %a@])" N.pp u - | Eq (a, b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" N.pp a N.pp b + Fmt.fprintf out "(@[%a@ %a@])" Fun.pp f (Util.pp_list Class.pp) l + | App_ho (f, a) -> Fmt.fprintf out "(@[%a@ %a@])" Class.pp f Class.pp a + | Opaque t -> Class.pp out t + | Not u -> Fmt.fprintf out "(@[not@ %a@])" Class.pp u + | Eq (a, b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" Class.pp a Class.pp b | If (a, b, c) -> - Fmt.fprintf out "(@[ite@ %a@ %a@ %a@])" N.pp a N.pp b N.pp c + Fmt.fprintf out "(@[ite@ %a@ %a@ %a@])" Class.pp a Class.pp b Class.pp c end module Sig_tbl = CCHashtbl.Make (Signature) @@ -360,12 +359,12 @@ module Make (A : CC_ARG) : several times. See "fast congruence closure and extensions", Nieuwenhuis&al, page 14 *) - and ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unit - and ev_on_post_merge = t -> actions -> N.t -> N.t -> unit - and ev_on_new_term = t -> N.t -> term -> unit + and ev_on_pre_merge = t -> actions -> Class.t -> Class.t -> Expl.t -> unit + and ev_on_post_merge = t -> actions -> Class.t -> Class.t -> unit + and ev_on_new_term = t -> Class.t -> term -> unit and ev_on_conflict = t -> th:bool -> lit list -> unit and ev_on_propagate = t -> lit -> (unit -> lit list * proof_step) -> unit - and ev_on_is_subterm = N.t -> term -> unit + and ev_on_is_subterm = Class.t -> term -> unit let[@inline] size_ (r : repr) = r.n_size let[@inline] n_true cc = Lazy.force cc.true_ @@ -387,13 +386,13 @@ module Make (A : CC_ARG) : let[@inline] on_backtrack cc f : unit = Backtrack_stack.push_if_nonzero_level cc.undo f - let[@inline] get_bitfield _cc field n = N.get_field field n + let[@inline] get_bitfield _cc field n = Class.get_field field n let set_bitfield cc field b n = - let old = N.get_field field n in + let old = Class.get_field field n in if old <> b then ( - on_backtrack cc (fun () -> N.set_field field old n); - N.set_field field b n + on_backtrack cc (fun () -> Class.set_field field old n); + Class.set_field field b n ) (* check if [t] is in the congruence closure. @@ -402,24 +401,26 @@ module Make (A : CC_ARG) : (* print full state *) let pp_full out (cc : t) : unit = - let pp_next out n = Fmt.fprintf out "@ :next %a" N.pp n.n_next in + let pp_next out n = Fmt.fprintf out "@ :next %a" Class.pp n.n_next in let pp_root out n = - if N.is_root n then + if Class.is_root n then Fmt.string out " :is-root" else - Fmt.fprintf out "@ :root %a" N.pp n.n_root + Fmt.fprintf out "@ :root %a" Class.pp n.n_root in let pp_expl out n = match n.n_expl with | FL_none -> () | FL_some e -> - Fmt.fprintf out " (@[:forest %a :expl %a@])" N.pp e.next Expl.pp e.expl + Fmt.fprintf out " (@[:forest %a :expl %a@])" Class.pp e.next Expl.pp + e.expl in let pp_n out n = Fmt.fprintf out "(@[%a%a%a%a@])" Term.pp n.n_term pp_root n pp_next n pp_expl n and pp_sig_e out (s, n) = - Fmt.fprintf out "(@[<1>%a@ ~~> %a%a@])" Signature.pp s N.pp n pp_root n + Fmt.fprintf out "(@[<1>%a@ ~~> %a%a@])" Signature.pp s Class.pp n pp_root + n in Fmt.fprintf out "(@[@{cc.state@}@ (@[:nodes@ %a@])@ (@[:sig-tbl@ %a@])@])" @@ -441,19 +442,19 @@ module Make (A : CC_ARG) : let add_signature cc (s : signature) (n : node) : unit = assert (not @@ Sig_tbl.mem cc.signatures_tbl s); Log.debugf 50 (fun k -> - k "(@[cc.add-sig@ %a@ ~~> %a@])" Signature.pp s N.pp n); + k "(@[cc.add-sig@ %a@ ~~> %a@])" Signature.pp s Class.pp n); on_backtrack cc (fun () -> Sig_tbl.remove cc.signatures_tbl s); Sig_tbl.add cc.signatures_tbl s n let push_pending cc t : unit = - Log.debugf 50 (fun k -> k "(@[cc.push-pending@ %a@])" N.pp t); + Log.debugf 50 (fun k -> k "(@[cc.push-pending@ %a@])" Class.pp t); Vec.push cc.pending t let merge_classes cc t u e : unit = if t != u && not (same_class t u) then ( Log.debugf 50 (fun k -> - k "(@[cc.push-combine@ %a ~@ %a@ :expl %a@])" N.pp t N.pp u - Expl.pp e); + k "(@[cc.push-combine@ %a ~@ %a@ :expl %a@])" Class.pp t Class.pp + u Expl.pp e); Vec.push cc.combine @@ CT_merge (t, u, e) ) @@ -477,10 +478,11 @@ module Make (A : CC_ARG) : Vec.clear cc.combine; List.iter (fun f -> f cc ~th e) cc.on_conflict; Stat.incr cc.count_conflict; - Actions.raise_conflict acts e p + let (module A) = acts in + A.raise_conflict e p let[@inline] all_classes cc : repr Iter.t = - T_tbl.values cc.tbl |> Iter.filter N.is_root + T_tbl.values cc.tbl |> Iter.filter Class.is_root (* find the closest common ancestor of [a] and [b] in the proof forest. @@ -494,7 +496,7 @@ module Make (A : CC_ARG) : let find_common_ancestor cc (a : node) (b : node) : node = (* catch up to the other node *) let rec find1 a = - if N.get_field cc.field_marked_explain a then + if Class.get_field cc.field_marked_explain a then a else ( match a.n_expl with @@ -503,15 +505,15 @@ module Make (A : CC_ARG) : ) in let rec find2 a b = - if N.equal a b then + if Class.equal a b then a - else if N.get_field cc.field_marked_explain a then + else if Class.get_field cc.field_marked_explain a then a - else if N.get_field cc.field_marked_explain b then + else if Class.get_field cc.field_marked_explain b then b else ( - N.set_field cc.field_marked_explain true a; - N.set_field cc.field_marked_explain true b; + Class.set_field cc.field_marked_explain true a; + Class.set_field cc.field_marked_explain true b; match a.n_expl, b.n_expl with | FL_some r1, FL_some r2 -> find2 r1.next r2.next | FL_some r, FL_none -> find1 r.next @@ -523,8 +525,8 @@ module Make (A : CC_ARG) : (* cleanup tags on nodes traversed in [find2] *) let rec cleanup_ n = - if N.get_field cc.field_marked_explain n then ( - N.set_field cc.field_marked_explain false n; + if Class.get_field cc.field_marked_explain n then ( + Class.set_field cc.field_marked_explain false n; match n.n_expl with | FL_none -> () | FL_some { next; _ } -> cleanup_ next @@ -538,7 +540,7 @@ module Make (A : CC_ARG) : module Expl_state = struct type t = { mutable lits: Lit.t list; - mutable same_val: (N.t * N.t) list; + mutable same_val: (Class.t * Class.t) list; mutable th_lemmas: (Lit.t * (Lit.t * Lit.t list) list * proof_step) list; } @@ -572,7 +574,9 @@ module Make (A : CC_ARG) : Iter.of_list self.th_lemmas |> Iter.map (fun (lit_t_u, _, _) -> Lit.neg lit_t_u) in - let p_cc = P.lemma_cc (Iter.append p_lits1 p_lits2) proof in + let p_cc = + P.add_step proof @@ Rules_.lemma_cc (Iter.append p_lits1 p_lits2) + in let resolve_with_th_proof pr (lit_t_u, sub_proofs, pr_th) = (* pr_th: [sub_proofs |- t=u]. now resolve away [sub_proofs] to get literals that were @@ -582,15 +586,16 @@ module Make (A : CC_ARG) : (fun pr_th (lit_i, hyps_i) -> (* [hyps_i |- lit_i] *) let lemma_i = - P.lemma_cc - Iter.(cons lit_i (of_list hyps_i |> map Lit.neg)) - proof + P.add_step proof + @@ Rules_.lemma_cc + Iter.(cons lit_i (of_list hyps_i |> map Lit.neg)) in (* resolve [lit_i] away. *) - P.proof_res ~pivot:(Lit.term lit_i) lemma_i pr_th proof) + P.add_step proof + @@ Rules_.proof_res ~pivot:(Lit.term lit_i) lemma_i pr_th) pr_th sub_proofs in - P.proof_res ~pivot:(Lit.term lit_t_u) pr_th pr proof + P.add_step proof @@ Rules_.proof_res ~pivot:(Lit.term lit_t_u) pr_th pr in (* resolve with theory proofs responsible for some merges, if any. *) List.fold_left resolve_with_th_proof p_cc self.th_lemmas @@ -629,14 +634,14 @@ module Make (A : CC_ARG) : let sub_proofs = List.map (fun (t_i, u_i, expls_i) -> - let lit_i = A.mk_lit_eq cc.tst t_i u_i in + let lit_i = A.CC.mk_lit_eq cc.tst t_i u_i in (* use a separate call to [explain_expls] for each set *) let sub = explain_expls cc expls_i in Expl_state.merge st sub; lit_i, sub.lits) expl_sets in - let lit_t_u = A.mk_lit_eq cc.tst t u in + let lit_t_u = A.CC.mk_lit_eq cc.tst t u in Expl_state.add_th st lit_t_u sub_proofs pr | E_merge (a, b) -> explain_equal_rec_ cc st a b | E_merge_t (a, b) -> @@ -657,8 +662,8 @@ module Make (A : CC_ARG) : and explain_equal_rec_ (cc : t) (st : Expl_state.t) (a : node) (b : node) : unit = Log.debugf 5 (fun k -> - k "(@[cc.explain_loop.at@ %a@ =?= %a@])" N.pp a N.pp b); - assert (N.equal (find_ a) (find_ b)); + k "(@[cc.explain_loop.at@ %a@ =?= %a@])" Class.pp a Class.pp b); + assert (Class.equal (find_ a) (find_ b)); let ancestor = find_common_ancestor cc a b in explain_along_path cc st a ancestor; explain_along_path cc st b ancestor @@ -689,7 +694,7 @@ module Make (A : CC_ARG) : and add_new_term_ cc (t : term) : node = assert (not @@ mem cc t); Log.debugf 15 (fun k -> k "(@[cc.add-term@ %a@])" Term.pp t); - let n = N.make t in + let n = Class.make t in (* register sub-terms, add [t] to their parent list, and return the corresponding initial signature *) let sig0 = compute_sig0 cc n in @@ -724,7 +729,7 @@ module Make (A : CC_ARG) : sub in let[@inline] return x = Some x in - match A.cc_view n.n_term with + match A.CC.view n.n_term with | Bool _ | Opaque _ -> None | Eq (a, b) -> let a = deref_sub a in @@ -750,13 +755,14 @@ module Make (A : CC_ARG) : match n.n_as_lit with | Some _ -> () | None -> - Log.debugf 15 (fun k -> k "(@[cc.set-as-lit@ %a@ %a@])" N.pp n Lit.pp lit); + Log.debugf 15 (fun k -> + k "(@[cc.set-as-lit@ %a@ %a@])" Class.pp n Lit.pp lit); on_backtrack cc (fun () -> n.n_as_lit <- None); n.n_as_lit <- Some lit (* is [n] true or false? *) let n_is_bool_value (self : t) n : bool = - N.equal n (n_true self) || N.equal n (n_false self) + Class.equal n (n_true self) || Class.equal n (n_false self) (* gather a pair [lits, pr], where [lits] is the set of asserted literals needed in the explanation (which is useful for @@ -790,16 +796,17 @@ module Make (A : CC_ARG) : if same_class a b then ( let expl = Expl.mk_merge a b in Log.debugf 5 (fun k -> - k "(@[cc.pending.eq@ %a@ :r1 %a@ :r2 %a@])" N.pp n N.pp a N.pp b); + k "(@[cc.pending.eq@ %a@ :r1 %a@ :r2 %a@])" Class.pp n Class.pp a + Class.pp b); 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 (n_true cc) then ( + if Class.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 ( + ) else if Class.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 ) @@ -810,7 +817,7 @@ module Make (A : CC_ARG) : | None -> (* add to the signature table [sig(n) --> n] *) add_signature cc s n - | Some u when N.equal n u -> () + | Some u when Class.equal n u -> () | Some u -> (* [t1] and [t2] must be applications of the same symbol to arguments that are pairwise equal *) @@ -841,10 +848,11 @@ module Make (A : CC_ARG) : k "(@[cc.semantic-conflict.set-val@ (@[set-val %a@ := %a@])@ \ (@[existing-val %a@ := %a@])@])" - N.pp n Term.pp v N.pp n' Term.pp v'); + Class.pp n Term.pp v Class.pp n' Term.pp v'); Stat.incr cc.count_semantic_conflict; - Actions.raise_semantic_conflict acts lits tuples + let (module A) = acts in + A.raise_semantic_conflict lits tuples | Some _ -> () | None -> T_b_tbl.add cc.t_to_val repr_n.n_term (n, v)); (* now for the reverse map, look in self.val_to_t for [v]. @@ -861,20 +869,20 @@ module Make (A : CC_ARG) : and task_merge_ cc acts a b e_ab : unit = let ra = find_ a in let rb = find_ b in - if not @@ N.equal ra rb then ( - assert (N.is_root ra); - assert (N.is_root rb); + if not @@ Class.equal ra rb then ( + assert (Class.is_root ra); + assert (Class.is_root rb); Stat.incr cc.count_merge; (* check we're not merging [true] and [false] *) 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)) + (Class.equal ra (n_true cc) && Class.equal rb (n_false cc)) + || (Class.equal rb (n_true cc) && Class.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@])" - N.pp ra N.pp a N.pp rb N.pp b Expl.pp e_ab); + Class.pp ra Class.pp a Class.pp rb Class.pp b Expl.pp e_ab); let th = ref false in (* TODO: C1: P.true_neq_false @@ -891,11 +899,12 @@ module Make (A : CC_ARG) : let lits = expl_st.lits in let same_val = expl_st.same_val - |> List.rev_map (fun (t, u) -> true, N.term t, N.term u) + |> List.rev_map (fun (t, u) -> true, Class.term t, Class.term u) in assert (same_val <> []); Stat.incr cc.count_semantic_conflict; - Actions.raise_semantic_conflict acts lits same_val + let (module A) = acts in + A.raise_semantic_conflict lits same_val ) else ( (* regular conflict *) let lits, pr = lits_and_proof_of_expl cc expl_st in @@ -917,9 +926,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 (n_true cc) then + if Class.equal r1 (n_true cc) then propagate_bools cc acts r2 t2 r1 t1 e_ab true - else if N.equal r1 (n_false cc) then + else if Class.equal r1 (n_false cc) then propagate_bools cc acts r2 t2 r1 t1 e_ab false in @@ -930,7 +939,7 @@ module Make (A : CC_ARG) : (* perform [union r_from r_into] *) Log.debugf 15 (fun k -> - k "(@[cc.merge@ :from %a@ :into %a@])" N.pp r_from N.pp r_into); + k "(@[cc.merge@ :from %a@ :into %a@])" Class.pp r_from Class.pp r_into); (* call [on_pre_merge] functions, and merge theory data items *) if not cc.model_mode then ( @@ -942,9 +951,9 @@ module Make (A : CC_ARG) : ); ((* parents might have a different signature, check for collisions *) - N.iter_parents r_from (fun parent -> push_pending cc parent); + Class.iter_parents r_from (fun parent -> push_pending cc parent); (* for each node in [r_from]'s class, make it point to [r_into] *) - N.iter_class r_from (fun u -> + Class.iter_class r_from (fun u -> assert (u.n_root == r_from); u.n_root <- r_into); (* capture current state *) @@ -961,15 +970,15 @@ module Make (A : CC_ARG) : (* on backtrack, unmerge classes and restore the pointers to [r_from] *) on_backtrack cc (fun () -> Log.debugf 30 (fun k -> - k "(@[cc.undo_merge@ :from %a@ :into %a@])" N.pp r_from N.pp - r_into); + k "(@[cc.undo_merge@ :from %a@ :into %a@])" Class.pp r_from + Class.pp r_into); r_into.n_bits <- r_into_old_bits; r_into.n_next <- r_into_old_next; r_from.n_next <- r_from_old_next; r_into.n_parents <- 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_ r_from (fun u -> u.n_root <- r_from); + Class.iter_class_ r_from (fun u -> u.n_root <- r_from); r_into.n_size <- r_into.n_size - r_from.n_size)); (* check for semantic values, update the one of [r_into] @@ -997,10 +1006,11 @@ module Make (A : CC_ARG) : k "(@[cc.semantic-conflict.post-merge@ (@[n-from %a@ := %a@])@ \ (@[n-into %a@ := %a@])@])" - N.pp n_from Term.pp v_from N.pp n_into Term.pp v_into); + Class.pp n_from Term.pp v_from Class.pp n_into Term.pp v_into); Stat.incr cc.count_semantic_conflict; - Actions.raise_semantic_conflict acts lits tuples + let (module A) = acts in + A.raise_semantic_conflict lits tuples | Some _ -> ())); (* update explanations (a -> b), arbitrarily. @@ -1012,8 +1022,8 @@ module Make (A : CC_ARG) : that bridges between [a] and [b] *) on_backtrack cc (fun () -> match a.n_expl, b.n_expl with - | FL_some e, _ when N.equal e.next b -> a.n_expl <- FL_none - | _, FL_some e when N.equal e.next a -> b.n_expl <- FL_none + | FL_some e, _ when Class.equal e.next b -> a.n_expl <- FL_none + | _, FL_some e when Class.equal e.next a -> b.n_expl <- FL_none | _ -> assert false); a.n_expl <- FL_some { next = b; expl = e_ab }; (* call [on_post_merge] *) @@ -1036,14 +1046,14 @@ module Make (A : CC_ARG) : in (* TODO: flag per class, `or`-ed on merge, to indicate if the class contains at least one lit *) - N.iter_class r1 (fun u1 -> + Class.iter_class r1 (fun u1 -> (* propagate if: - [u1] is a proper literal - [t2 != r2], because that can only happen after an explicit merge (no way to obtain that by propagation) *) - match N.as_lit u1 with - | Some lit when not (N.equal r2 t2) -> + match Class.as_lit u1 with + | Some lit when not (Class.equal r2 t2) -> let lit = if sign then lit @@ -1070,7 +1080,8 @@ module Make (A : CC_ARG) : in List.iter (fun f -> f cc lit reason) cc.on_propagate; Stat.incr cc.count_props; - Actions.propagate acts lit ~reason + let (module A) = acts in + A.propagate lit ~reason ) | _ -> ()) @@ -1078,9 +1089,7 @@ module Make (A : CC_ARG) : let pp out _ = Fmt.string out "cc" end - let add_seq cc seq = - seq (fun t -> ignore @@ add_term_rec_ cc t); - () + let add_iter cc it : unit = it (fun t -> ignore @@ add_term_rec_ cc t) let[@inline] push_level (self : t) : unit = Backtrack_stack.push_level self.undo; @@ -1112,7 +1121,7 @@ module Make (A : CC_ARG) : all_classes self |> Iter.filter_map (fun repr -> match T_b_tbl.get self.t_to_val repr.n_term with - | Some (_, v) -> Some (repr, N.iter_class repr, v) + | Some (_, v) -> Some (repr, Class.iter_class repr, v) | None -> None) (* assert that this boolean literal holds. @@ -1122,7 +1131,7 @@ module Make (A : CC_ARG) : let t = Lit.term lit in Log.debugf 15 (fun k -> k "(@[cc.assert-lit@ %a@])" Lit.pp lit); let sign = Lit.sign lit in - match A.cc_view t with + match A.CC.view t with | Eq (a, b) when sign -> let a = add_term cc a in let b = add_term cc b in @@ -1159,8 +1168,8 @@ module Make (A : CC_ARG) : let merge cc n1 n2 expl = Log.debugf 5 (fun k -> - k "(@[cc.theory.merge@ :n1 %a@ :n2 %a@ :expl %a@])" N.pp n1 N.pp n2 - Expl.pp expl); + k "(@[cc.theory.merge@ :n1 %a@ :n2 %a@ :expl %a@])" Class.pp n1 Class.pp + n2 Expl.pp expl); assert (T.Ty.equal (T.Term.ty n1.n_term) (T.Term.ty n2.n_term)); merge_classes cc n1 n2 expl @@ -1245,7 +1254,8 @@ module Make (A : CC_ARG) : let check_inv_ (self : t) : unit = if check_inv_enabled_ then ( Log.debug 2 "(cc.check-invariants)"; - all_classes self |> Iter.flat_map N.iter_class + all_classes self + |> Iter.flat_map Class.iter_class |> Iter.iter (fun n -> match n.n_sig0 with | None -> () @@ -1254,16 +1264,143 @@ module Make (A : CC_ARG) : let ok = match find_signature self s' with | None -> false - | Some r -> N.equal r n.n_root + | Some r -> Class.equal r n.n_root in if not ok then Log.debugf 0 (fun k -> k "(@[cc.check.fail@ :n %a@ :sig %a@ :actual-sig %a@])" - N.pp n Signature.pp s Signature.pp s')) + Class.pp n Signature.pp s Signature.pp s')) ) (* model: return all the classes *) let get_model (cc : t) : repr Iter.t Iter.t = check_inv_ cc; - all_classes cc |> Iter.map N.iter_class + all_classes cc |> Iter.map Class.iter_class +end + +module Make_plugin (M : MONOID_ARG) : PLUGIN_BUILDER with module M = M = struct + module M = M + module CC = M.CC + module Class = CC.Class + module N_tbl = Backtrackable_tbl.Make (Class) + module Expl = CC.Expl + + type term = CC.term + + module type PL = PLUGIN with module CC = M.CC and module M = M + + type plugin = (module PL) + + module Make (A : sig + val size : int option + val cc : CC.t + end) : PL = struct + module M = M + module CC = CC + open A + + (* repr -> value for the class *) + let values : M.t N_tbl.t = N_tbl.create ?size () + + (* bit in CC to filter out quickly classes without value *) + let field_has_value : Class.bitfield = + CC.allocate_bitfield ~descr:("monoid." ^ M.name ^ ".has-value") cc + + let push_level () = N_tbl.push_level values + let pop_levels n = N_tbl.pop_levels values n + let n_levels () = N_tbl.n_levels values + + let mem n = + let res = CC.get_bitfield cc field_has_value n in + assert ( + if res then + N_tbl.mem values n + else + true); + res + + let get n = + if CC.get_bitfield cc field_has_value n then + N_tbl.get values n + else + None + + let on_new_term cc n (t : term) : unit = + (*Log.debugf 50 (fun k->k "(@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);*) + let maybe_m, l = M.of_term cc n t in + (match maybe_m with + | Some v -> + Log.debugf 20 (fun k -> + k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])" M.name Class.pp n + M.pp v); + CC.set_bitfield cc field_has_value true n; + N_tbl.add values n v + | None -> ()); + List.iter + (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 Class.pp n Class.pp n_u M.pp m_u); + let n_u = CC.find cc n_u in + if CC.get_bitfield cc field_has_value n_u then ( + let m_u' = + try N_tbl.find values n_u + with Not_found -> + Error.errorf "node %a has bitfield but no value" Class.pp n_u + in + match M.merge cc n_u m_u n_u m_u' (Expl.mk_list []) with + | Error expl -> + Error.errorf + "when merging@ @[for node %a@],@ values %a and %a:@ conflict %a" + Class.pp n_u M.pp m_u M.pp m_u' CC.Expl.pp 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 Class.pp n Class.pp n_u M.pp m_u_merged); + N_tbl.add values n_u m_u_merged + ) else ( + (* just add to [n_u] *) + CC.set_bitfield cc field_has_value true n_u; + N_tbl.add values n_u m_u + )) + l; + () + + let iter_all : _ Iter.t = N_tbl.to_iter values + + let on_pre_merge cc acts n1 n2 e_n1_n2 : unit = + match get n1, get n2 with + | Some v1, Some v2 -> + Log.debugf 5 (fun k -> + k + "(@[monoid[%s].on_pre_merge@ (@[:n1 %a@ :val1 %a@])@ (@[:n2 %a@ \ + :val2 %a@])@])" + M.name Class.pp n1 M.pp v1 Class.pp n2 M.pp v2); + (match M.merge cc n1 v1 n2 v2 e_n1_n2 with + | Ok v' -> + N_tbl.remove values n2; + (* only keep repr *) + N_tbl.add values n1 v' + | Error expl -> CC.raise_conflict_from_expl cc acts expl) + | None, Some cr -> + CC.set_bitfield cc field_has_value true n1; + N_tbl.add values n1 cr; + N_tbl.remove values n2 (* only keep reprs *) + | Some _, None -> () (* already there on the left *) + | None, None -> () + + (* setup *) + let () = + CC.on_new_term cc on_new_term; + CC.on_pre_merge cc on_pre_merge; + () + end + + let create_and_setup ?size (cc : CC.t) : plugin = + (module Make (struct + let size = size + let cc = cc + end)) end diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli index 48760ec2..ade46641 100644 --- a/src/cc/Sidekick_cc.mli +++ b/src/cc/Sidekick_cc.mli @@ -1,13 +1,20 @@ -(** {2 Congruence Closure} *) +(** Congruence Closure Implementation *) -open Sidekick_core +module View = Sidekick_sigs_cc.View -module type S = Sidekick_core.CC_S +module type TERM = Sidekick_sigs_cc.TERM +module type LIT = Sidekick_sigs_cc.LIT +module type ARG = Sidekick_sigs_cc.ARG +module type S = Sidekick_sigs_cc.S +module type MONOID_ARG = Sidekick_sigs_cc.MONOID_ARG +module type PLUGIN = Sidekick_sigs_cc.PLUGIN +module type PLUGIN_BUILDER = Sidekick_sigs_cc.PLUGIN_BUILDER -module Make (A : CC_ARG) : +module Make (A : ARG) : S with module T = A.T and module Lit = A.Lit - and type proof = A.proof - and type proof_step = A.proof_step - and module Actions = A.Actions + and module Proof_trace = A.Proof_trace + +(** Create a plugin builder from the given per-class monoid *) +module Make_plugin (M : MONOID_ARG) : PLUGIN_BUILDER with module M = M diff --git a/src/cc/dune b/src/cc/dune index a7ca76ab..b33f850d 100644 --- a/src/cc/dune +++ b/src/cc/dune @@ -1,5 +1,5 @@ (library (name Sidekick_cc) (public_name sidekick.cc) - (libraries containers iter sidekick.core sidekick.util) + (libraries containers iter sidekick.sigs sidekick.sigs.cc sidekick.util) (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util)) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index ce108e2b..213ba2fc 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -1,4 +1,4 @@ -(** {1 Main Signatures} +(** Main Signatures. Theories and concrete solvers rely on an environment that defines several important types: @@ -14,777 +14,15 @@ module Fmt = CCFormat -(** View terms through the lens of the Congruence Closure *) -module CC_view = struct - (** A view of a term fron the point of view of the congruence closure. - - - ['f] is the type of function symbols - - ['t] is the type of terms - - ['ts] is the type of sequences of terms (arguments of function application) - *) - type ('f, 't, 'ts) t = - | Bool of bool - | App_fun of 'f * 'ts - | App_ho of 't * 't - | If of 't * 't * 't - | Eq of 't * 't - | Not of 't - | Opaque of 't - (* do not enter *) - - (** Map function over a view, one level deep. - Each function maps over a different type, e.g. [f_t] maps over terms *) - let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t = - match v with - | Bool b -> Bool b - | App_fun (f, args) -> App_fun (f_f f, f_ts args) - | App_ho (f, a) -> App_ho (f_t f, f_t a) - | Not t -> Not (f_t t) - | If (a, b, c) -> If (f_t a, f_t b, f_t c) - | Eq (a, b) -> Eq (f_t a, f_t b) - | Opaque t -> Opaque (f_t t) - - (** Iterate over a view, one level deep. *) - let iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit = - match v with - | Bool _ -> () - | App_fun (f, args) -> - f_f f; - f_ts args - | App_ho (f, a) -> - f_t f; - f_t a - | Not t -> f_t t - | If (a, b, c) -> - f_t a; - f_t b; - f_t c - | Eq (a, b) -> - f_t a; - f_t b - | Opaque t -> f_t t -end - -(** Main representation of Terms and Types *) -module type TERM = sig - (** A function symbol, like "f" or "plus" or "is_human" or "socrates" *) - module Fun : sig - type t - - val equal : t -> t -> bool - val hash : t -> int - val pp : t Fmt.printer - end - - (** Types - - Types should be comparable (ideally, in O(1)), and have - at least a boolean type available. *) - module Ty : sig - type t - - val equal : t -> t -> bool - val hash : t -> int - val pp : t Fmt.printer - - type store - - val bool : store -> t - val is_bool : t -> bool - end - - (** Term structure. - - Terms should be {b hashconsed}, with perfect sharing. - This allows, for example, {!Term.Tbl} and {!Term.iter_dag} to be efficient. - *) - module Term : sig - type t - - val equal : t -> t -> bool - val compare : t -> t -> int - val hash : t -> int - val pp : t Fmt.printer - - type store - (** A store used to create new terms. It is where the hashconsing - table should live, along with other all-terms related store. *) - - val ty : t -> Ty.t - - val bool : store -> bool -> t - (** build true/false *) - - val as_bool : t -> bool option - (** [as_bool t] is [Some true] if [t] is the term [true], and similarly - for [false]. For other terms it is [None]. *) - - val abs : store -> t -> t * bool - (** [abs t] returns an "absolute value" for the term, along with the - sign of [t]. - - The idea is that we want to turn [not a] into [(a, false)], - or [(a != b)] into [(a=b, false)]. For terms without a negation this - should return [(t, true)]. - - The store is passed in case a new term needs to be created. *) - - val map_shallow : store -> (t -> t) -> t -> t - (** Map function on immediate subterms. This should not be recursive. *) - - val iter_shallow : store -> (t -> unit) -> t -> unit - (** Iterate function on immediate subterms. This should not be recursive. *) - - val iter_dag : t -> (t -> unit) -> unit - (** [iter_dag t f] calls [f] once on each subterm of [t], [t] included. - It must {b not} traverse [t] as a tree, but rather as a - perfectly shared DAG. - - For example, in: - {[ - let x = 2 in - let y = f x x in - let z = g y x in - z = z - ]} - - the DAG has the following nodes: - - {[ n1: 2 - n2: f n1 n1 - n3: g n2 n1 - n4: = n3 n3 - ]} - *) - - module Tbl : CCHashtbl.S with type key = t - end -end +module type TERM = Sidekick_sigs_term.S +module type LIT = Sidekick_sigs_lit.S +module type PROOF_TRACE = Sidekick_sigs_proof_trace.S +module type SAT_PROOF = Sidekick_sigs_proof_sat.S (** Signature for SAT-solver proof emission. *) -module type SAT_PROOF = sig - type t - (** The stored proof (possibly nil, possibly on disk, possibly in memory) *) - - type proof_step - (** identifier for a proof *) - - module Step_vec : Vec_sig.BASE with type elt = proof_step - (** A vector of steps *) - - type lit - (** A boolean literal for the proof trace *) - - type proof_rule = t -> proof_step - (** A proof proof_rule constructor, used to obtain proofs from theories *) - - val enabled : t -> bool - (** Returns true if proof production is enabled *) - - val emit_input_clause : lit Iter.t -> proof_rule - (** Emit an input clause. *) - - val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule - (** Emit a clause deduced by the SAT solver, redundant wrt previous clauses. - The clause must be RUP wrt [hyps]. *) - - val emit_unsat_core : lit Iter.t -> proof_rule - (** Produce a proof of the empty clause given this subset of the assumptions. - FIXME: probably needs the list of proof_step that disprove the lits? *) - - val emit_unsat : proof_step -> t -> unit - (** Signal "unsat" result at the given proof *) - - val del_clause : proof_step -> lit Iter.t -> t -> unit - (** Forget a clause. Only useful for performance considerations. *) -end +module type PROOF = Sidekick_sigs_proof_core.S (** Proofs of unsatisfiability. *) -module type PROOF = sig - type t - (** The abstract representation of a proof. A proof always proves - a clause to be {b valid} (true in every possible interpretation - of the problem's assertions, and the theories) *) - - type proof_step - (** Identifier for a proof proof_rule (like a unique ID for a clause previously - added/proved) *) - - type term - type lit - type proof_rule = t -> proof_step - - include - SAT_PROOF - with type t := t - and type lit := lit - and type proof_step := proof_step - and type proof_rule := proof_rule - - val lemma_cc : lit Iter.t -> proof_rule - (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory - of uninterpreted functions. *) - - val define_term : term -> term -> proof_rule - (** [define_term cst u proof] defines the new constant [cst] as being equal - to [u]. - The result is a proof of the clause [cst = u] *) - - val proof_p1 : proof_step -> proof_step -> proof_rule - (** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool) - and [p2] proves [C \/ t], is the rule that produces [C \/ u], - i.e unit paramodulation. *) - - val proof_r1 : proof_step -> proof_step -> proof_rule - (** [proof_r1 p1 p2], where [p1] proves the unit clause [|- t] (t:bool) - and [p2] proves [C \/ ¬t], is the rule that produces [C \/ u], - i.e unit resolution. *) - - val proof_res : pivot:term -> proof_step -> proof_step -> proof_rule - (** [proof_res ~pivot p1 p2], where [p1] proves the clause [|- C \/ l] - and [p2] proves [D \/ ¬l], where [l] is either [pivot] or [¬pivot], - is the rule that produces [C \/ D], i.e boolean resolution. *) - - val with_defs : proof_step -> proof_step Iter.t -> proof_rule - (** [with_defs pr defs] specifies that [pr] is valid only in - a context where the definitions [defs] are present. *) - - val lemma_true : term -> proof_rule - (** [lemma_true (true) p] asserts the clause [(true)] *) - - val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule - (** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology - and that [t] has been preprocessed into [u]. - - The theorem [/\_{eqn in using} eqn |- t=u] is proved using congruence - closure, and then resolved against the clauses [using] to obtain - a unit equality. - - From now on, [t] and [u] will be used interchangeably. - @return a proof_rule ID for the clause [(t=u)]. *) - - val lemma_rw_clause : - proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule - (** [lemma_rw_clause prc ~res ~using], where [prc] is the proof of [|- c], - uses the equations [|- p_i = q_i] from [using] - to rewrite some literals of [c] into [res]. This is used to preprocess - literals of a clause (using {!lemma_preprocess} individually). *) -end - -(** Literals - - Literals are a pair of a boolean-sorted term, and a sign. - Positive literals are the same as their term, and negative literals - are the negation of their term. - - The SAT solver deals only in literals and clauses (sets of literals). - Everything else belongs in the SMT solver. *) -module type LIT = sig - module T : TERM - (** Literals depend on terms *) - - type t - (** A literal *) - - val term : t -> T.Term.t - (** Get the (positive) term *) - - val sign : t -> bool - (** Get the sign. A negated literal has sign [false]. *) - - val neg : t -> t - (** Take negation of literal. [sign (neg lit) = not (sign lit)]. *) - - val abs : t -> t - (** [abs lit] is like [lit] but always positive, i.e. [sign (abs lit) = true] *) - - val signed_term : t -> T.Term.t * bool - (** Return the atom and the sign *) - - val atom : ?sign:bool -> T.Term.store -> T.Term.t -> t - (** [atom store t] makes a literal out of a term, possibly normalizing - its sign in the process. - @param sign if provided, and [sign=false], negate the resulting lit. *) - - val norm_sign : t -> t * bool - (** [norm_sign (+t)] is [+t, true], - and [norm_sign (-t)] is [+t, false]. - In both cases the term is positive, and the boolean reflects the initial sign. *) - - val equal : t -> t -> bool - val hash : t -> int - val pp : t Fmt.printer -end - -(** Actions provided to the congruence closure. - - The congruence closure must be able to propagate literals when - it detects that they are true or false; it must also - be able to create conflicts when the set of (dis)equalities - is inconsistent *) -module type CC_ACTIONS = sig - module T : TERM - module Lit : LIT with module T = T - - type proof - type proof_step - - module P : - PROOF - with type lit = Lit.t - and type t = proof - and type term = T.Term.t - and type proof_step = proof_step - - type t - (** An action handle. It is used by the congruence closure - to perform the actions below. How it performs the actions - is not specified and is solver-specific. *) - - val proof : t -> proof - - val raise_conflict : t -> Lit.t list -> proof_step -> 'a - (** [raise_conflict acts c pr] declares that [c] is a tautology of - the theory of congruence. This does not return (it should raise an - exception). - @param pr the proof of [c] being a tautology *) - - val raise_semantic_conflict : - t -> Lit.t list -> (bool * T.Term.t * T.Term.t) list -> 'a - (** [raise_semantic_conflict acts lits same_val] declares that - the conjunction of all [lits] (literals true in current trail) and tuples - [{=,≠}, t_i, u_i] implies false. - - The [{=,≠}, t_i, u_i] are pairs of terms with the same value (if [=] / true) - or distinct value (if [≠] / false)) in the current model. - - This does not return. It should raise an exception. - *) - - val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * proof_step) -> unit - (** [propagate acts lit ~reason pr] declares that [reason() => lit] - is a tautology. - - - [reason()] should return a list of literals that are currently true. - - [lit] should be a literal of interest (see {!CC_S.set_as_lit}). - - This function might never be called, a congruence closure has the right - to not propagate and only trigger conflicts. *) -end - -(** Arguments to a congruence closure's implementation *) -module type CC_ARG = sig - module T : TERM - module Lit : LIT with module T = T - - type proof - type proof_step - - module P : - PROOF - with type lit = Lit.t - and type t = proof - and type term = T.Term.t - and type proof_step = proof_step - - module Actions : - CC_ACTIONS - with module T = T - and module Lit = Lit - and type proof = proof - and type proof_step = proof_step - - val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t - (** View the term through the lens of the congruence closure *) - - val mk_lit_eq : ?sign:bool -> T.Term.store -> T.Term.t -> T.Term.t -> Lit.t - (** [mk_lit_eq store t u] makes the literal [t=u] *) -end - -(** Main congruence closure signature. - - The congruence closure handles the theory QF_UF (uninterpreted - function symbols). - It is also responsible for {i theory combination}, and provides - a general framework for equality reasoning that other - theories piggyback on. - - For example, the theory of datatypes relies on the congruence closure - to do most of the work, and "only" adds injectivity/disjointness/acyclicity - lemmas when needed. - - Similarly, a theory of arrays would hook into the congruence closure and - assert (dis)equalities as needed. -*) -module type CC_S = sig - (** first, some aliases. *) - - module T : TERM - module Lit : LIT with module T = T - - type proof - type proof_step - - module P : - PROOF - with type lit = Lit.t - and type t = proof - and type proof_step = proof_step - - module Actions : - CC_ACTIONS - with module T = T - and module Lit = Lit - and type proof = proof - and type proof_step = proof_step - - type term_store = T.Term.store - type term = T.Term.t - type value = term - type fun_ = T.Fun.t - type lit = Lit.t - type actions = Actions.t - - type t - (** The congruence closure object. - It contains a fair amount of state and is mutable - and backtrackable. *) - - (** Equivalence classes. - - An equivalence class is a set of terms that are currently equal - in the partial model built by the solver. - The class is represented by a collection of nodes, one of which is - distinguished and is called the "representative". - - All information pertaining to the whole equivalence class is stored - in this representative's node. - - When two classes become equal (are "merged"), one of the two - representatives is picked as the representative of the new class. - The new class contains the union of the two old classes' nodes. - - We also allow theories to store additional information in the - representative. This information can be used when two classes are - merged, to detect conflicts and solve equations à la Shostak. - *) - module N : sig - type t - (** An equivalent class, containing terms that are proved - to be equal. - - A value of type [t] points to a particular term, but see - {!find} to get the representative of the class. *) - - val term : t -> term - (** Term contained in this equivalence class. - If [is_root n], then [term n] is the class' representative term. *) - - val equal : t -> t -> bool - (** Are two classes {b physically} equal? To check for - logical equality, use [CC.N.equal (CC.find cc n1) (CC.find cc n2)] - which checks for equality of representatives. *) - - val hash : t -> int - (** An opaque hash of this node. *) - - val pp : t Fmt.printer - (** Unspecified printing of the node, for example its term, - a unique ID, etc. *) - - val is_root : t -> bool - (** Is the node a root (ie the representative of its class)? - See {!find} to get the root. *) - - val iter_class : t -> t Iter.t - (** Traverse the congruence class. - Precondition: [is_root n] (see {!find} below) *) - - val iter_parents : t -> t Iter.t - (** Traverse the parents of the class. - Precondition: [is_root n] (see {!find} below) *) - - type bitfield - (** A field in the bitfield of this node. This should only be - allocated when a theory is initialized. - - Bitfields are accessed using preallocated keys. - See {!CC_S.allocate_bitfield}. - - All fields are initially 0, are backtracked automatically, - and are merged automatically when classes are merged. *) - end - - (** Explanations - - Explanations are specialized proofs, created by the congruence closure - when asked to justify why 2 terms are equal. *) - module Expl : sig - type t - - val pp : t Fmt.printer - - val mk_merge : N.t -> N.t -> t - (** Explanation: the nodes were explicitly merged *) - - val mk_merge_t : term -> term -> t - (** Explanation: the terms were explicitly merged *) - - val mk_lit : lit -> t - (** Explanation: we merged [t] and [u] because of literal [t=u], - or we merged [t] and [true] because of literal [t], - or [t] and [false] because of literal [¬t] *) - - val mk_same_value : N.t -> N.t -> t - - val mk_list : t list -> t - (** Conjunction of explanations *) - - val mk_theory : - term -> term -> (term * term * t list) list -> proof_step -> t - (** [mk_theory t u expl_sets pr] builds a theory explanation for - why [|- t=u]. It depends on sub-explanations [expl_sets] which - are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are - explanations that justify [t_i = u_i] in the current congruence closure. - - The proof [pr] is the theory lemma, of the form - [ (t_i = u_i)_i |- t=u ]. - It is resolved against each [expls_i |- t_i=u_i] obtained from - [expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u] - where [Gamma] is a subset of the literals asserted into the congruence - closure. - - For example for the lemma [a=b] deduced by injectivity - from [Some a=Some b] in the theory of datatypes, - the arguments would be - [a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr] - where [pr] is the injectivity lemma [Some a=Some b |- a=b]. - *) - end - - (** Resolved explanations. - - The congruence closure keeps explanations for why terms are in the same - class. However these are represented in a compact, cheap form. - To use these explanations we need to {b resolve} them into a - resolved explanation, typically a list of - literals that are true in the current trail and are responsible for - merges. - - However, we can also have merged classes because they have the same value - in the current model. *) - module Resolved_expl : sig - type t = { - lits: lit list; - same_value: (N.t * N.t) list; - pr: proof -> proof_step; - } - - val is_semantic : t -> bool - (** [is_semantic expl] is [true] if there's at least one - pair in [expl.same_value]. *) - - val pp : t Fmt.printer - end - - type node = N.t - (** A node of the congruence closure *) - - type repr = N.t - (** Node that is currently a representative *) - - type explanation = Expl.t - - (** {3 Accessors} *) - - val term_store : t -> term_store - val proof : t -> proof - - val find : t -> node -> repr - (** Current representative *) - - val add_term : t -> term -> node - (** Add the term to the congruence closure, if not present already. - Will be backtracked. *) - - val mem_term : t -> term -> bool - (** Returns [true] if the term is explicitly present in the congruence closure *) - - (** {3 Events} - - Events triggered by the congruence closure, to which - other plugins can subscribe. *) - - type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unit - (** [ev_on_pre_merge cc acts n1 n2 expl] is called right before [n1] - and [n2] are merged with explanation [expl]. *) - - type ev_on_post_merge = t -> actions -> N.t -> N.t -> unit - (** [ev_on_post_merge cc acts n1 n2] is called right after [n1] - and [n2] were merged. [find cc n1] and [find cc n2] will return - the same node. *) - - type ev_on_new_term = t -> N.t -> term -> unit - (** [ev_on_new_term cc n t] is called whenever a new term [t] - is added to the congruence closure. Its node is [n]. *) - - type ev_on_conflict = t -> th:bool -> lit list -> unit - (** [ev_on_conflict acts ~th c] is called when the congruence - closure triggers a conflict by asserting the tautology [c]. - - @param th true if the explanation for this conflict involves - at least one "theory" explanation; i.e. some of the equations - participating in the conflict are purely syntactic theories - like injectivity of constructors. *) - - type ev_on_propagate = t -> lit -> (unit -> lit list * proof_step) -> unit - (** [ev_on_propagate cc lit reason] is called whenever [reason() => lit] - is a propagated lemma. See {!CC_ACTIONS.propagate}. *) - - type ev_on_is_subterm = N.t -> term -> unit - (** [ev_on_is_subterm n t] is called when [n] is a subterm of - another node for the first time. [t] is the term corresponding to - the node [n]. This can be useful for theory combination. *) - - val create : - ?stat:Stat.t -> - ?on_pre_merge:ev_on_pre_merge list -> - ?on_post_merge:ev_on_post_merge list -> - ?on_new_term:ev_on_new_term list -> - ?on_conflict:ev_on_conflict list -> - ?on_propagate:ev_on_propagate list -> - ?on_is_subterm:ev_on_is_subterm list -> - ?size:[ `Small | `Big ] -> - term_store -> - proof -> - t - (** Create a new congruence closure. - - @param term_store used to be able to create new terms. All terms - interacting with this congruence closure must belong in this term state - as well. *) - - val allocate_bitfield : descr:string -> t -> N.bitfield - (** Allocate a new node field (see {!N.bitfield}). - - This field descriptor is henceforth reserved for all nodes - in this congruence closure, and can be set using {!set_bitfield} - for each node individually. - This can be used to efficiently store some metadata on nodes - (e.g. "is there a numeric value in the class" - or "is there a constructor term in the class"). - - There may be restrictions on how many distinct fields are allocated - for a given congruence closure (e.g. at most {!Sys.int_size} fields). - *) - - val get_bitfield : t -> N.bitfield -> N.t -> bool - (** Access the bit field of the given node *) - - val set_bitfield : t -> N.bitfield -> bool -> N.t -> unit - (** Set the bitfield for the node. This will be backtracked. - See {!N.bitfield}. *) - - (* TODO: remove? this is managed by the solver anyway? *) - val on_pre_merge : t -> ev_on_pre_merge -> unit - (** Add a function to be called when two classes are merged *) - - val on_post_merge : t -> ev_on_post_merge -> unit - (** Add a function to be called when two classes are merged *) - - val on_new_term : t -> ev_on_new_term -> unit - (** Add a function to be called when a new node is created *) - - val on_conflict : t -> ev_on_conflict -> unit - (** Called when the congruence closure finds a conflict *) - - val on_propagate : t -> ev_on_propagate -> unit - (** Called when the congruence closure propagates a literal *) - - val on_is_subterm : t -> ev_on_is_subterm -> unit - (** Called on terms that are subterms of function symbols *) - - val set_as_lit : t -> N.t -> lit -> unit - (** map the given node to a literal. *) - - val find_t : t -> term -> repr - (** Current representative of the term. - @raise Not_found if the term is not already {!add}-ed. *) - - val add_seq : t -> term Iter.t -> unit - (** Add a sequence of terms to the congruence closure *) - - val all_classes : t -> repr Iter.t - (** All current classes. This is costly, only use if there is no other solution *) - - val assert_lit : t -> lit -> unit - (** Given a literal, assume it in the congruence closure and propagate - its consequences. Will be backtracked. - - Useful for the theory combination or the SAT solver's functor *) - - val assert_lits : t -> lit Iter.t -> unit - (** Addition of many literals *) - - val explain_eq : t -> N.t -> N.t -> Resolved_expl.t - (** Explain why the two nodes are equal. - Fails if they are not, in an unspecified way. *) - - val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a - (** Raise a conflict with the given explanation. - It must be a theory tautology that [expl ==> absurd]. - To be used in theories. - - This fails in an unspecified way if the explanation, once resolved, - satisfies {!Resolved_expl.is_semantic}. *) - - val n_true : t -> N.t - (** Node for [true] *) - - val n_false : t -> N.t - (** Node for [false] *) - - val n_bool : t -> bool -> N.t - (** Node for either true or false *) - - 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]. - To be used in theories. *) - - val merge_t : t -> term -> term -> Expl.t -> unit - (** Shortcut for adding + merging *) - - val set_model_value : t -> term -> value -> unit - (** Set the value of a term in the model. *) - - val with_model_mode : t -> (unit -> 'a) -> 'a - (** Enter model combination mode. *) - - val get_model_for_each_class : t -> (repr * N.t Iter.t * value) Iter.t - (** In model combination mode, obtain classes with their values. *) - - val check : t -> actions -> unit - (** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc. - Will use the {!actions} to propagate literals, declare conflicts, etc. *) - - val push_level : t -> unit - (** Push backtracking level *) - - val pop_levels : t -> int -> unit - (** Restore to state [n] calls to [push_level] earlier. Used during backtracking. *) - - val get_model : t -> N.t Iter.t Iter.t - (** get all the equivalence classes so they can be merged in the model *) - - (**/**) - - module Debug_ : sig - val pp : t Fmt.printer - end - - (**/**) -end (** Registry to extract values *) module type REGISTRY = sig @@ -807,6 +45,7 @@ end module type SOLVER_INTERNAL = sig module T : TERM module Lit : LIT with module T = T + module Proof_trace : PROOF_TRACE type ty = T.Ty.t type term = T.Term.t @@ -814,16 +53,8 @@ module type SOLVER_INTERNAL = sig type term_store = T.Term.store type ty_store = T.Ty.store type clause_pool - type proof - type proof_step - - (** {3 Proofs} *) - module P : - PROOF - with type lit = Lit.t - and type term = term - and type t = proof - and type proof_step = proof_step + type proof = Proof_trace.t + type proof_step = Proof_trace.step_id type t (** {3 Main type for a solver} *) @@ -855,14 +86,10 @@ module type SOLVER_INTERNAL = sig (** Congruence closure instance *) module CC : - CC_S + Sidekick_sigs_cc.S with module T = T and module Lit = Lit - and type proof = proof - and type proof_step = proof_step - and type P.t = proof - and type P.lit = lit - and type Actions.t = theory_actions + and module Proof_trace = Proof_trace val cc : t -> CC.t (** Congruence closure for this solver *) @@ -1000,13 +227,14 @@ module type SOLVER_INTERNAL = sig it must be a theory tautology that [expl ==> absurd]. To be used in theories. *) - val cc_find : t -> CC.N.t -> CC.N.t + val cc_find : t -> CC.Class.t -> CC.Class.t (** Find representative of the node *) val cc_are_equal : t -> term -> term -> bool (** Are these two terms equal in the congruence closure? *) - val cc_merge : t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit + val cc_merge : + t -> theory_actions -> CC.Class.t -> CC.Class.t -> CC.Expl.t -> unit (** Merge these two nodes in the congruence closure, given this explanation. It must be a theory tautology that [expl ==> n1 = n2]. To be used in theories. *) @@ -1015,7 +243,7 @@ module type SOLVER_INTERNAL = sig (** Merge these two terms in the congruence closure, given this explanation. See {!cc_merge} *) - val cc_add_term : t -> term -> CC.N.t + val cc_add_term : t -> term -> CC.Class.t (** Add/retrieve congruence closure node for this term. To be used in theories *) @@ -1025,19 +253,19 @@ module type SOLVER_INTERNAL = sig val on_cc_pre_merge : t -> - (CC.t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> + (CC.t -> theory_actions -> CC.Class.t -> CC.Class.t -> CC.Expl.t -> unit) -> unit (** Callback for when two classes containing data for this key are merged (called before) *) val on_cc_post_merge : - t -> (CC.t -> theory_actions -> CC.N.t -> CC.N.t -> unit) -> unit + t -> (CC.t -> theory_actions -> CC.Class.t -> CC.Class.t -> unit) -> unit (** Callback for when two classes containing data for this key are merged (called after)*) - val on_cc_new_term : t -> (CC.t -> CC.N.t -> term -> unit) -> unit + val on_cc_new_term : t -> (CC.t -> CC.Class.t -> term -> unit) -> unit (** Callback to add data on terms when they are added to the congruence closure *) - val on_cc_is_subterm : t -> (CC.N.t -> term -> unit) -> unit + val on_cc_is_subterm : t -> (CC.Class.t -> term -> unit) -> unit (** Callback for when a term is a subterm of another term in the congruence closure *) @@ -1083,7 +311,7 @@ module type SOLVER_INTERNAL = sig (** {3 Model production} *) type model_ask_hook = - recurse:(t -> CC.N.t -> term) -> t -> CC.N.t -> term option + recurse:(t -> CC.Class.t -> term) -> t -> CC.Class.t -> term option (** A model-production hook to query values from a theory. It takes the solver, a class, and returns @@ -1113,25 +341,14 @@ end module type SOLVER = sig module T : TERM module Lit : LIT with module T = T - - type proof - type proof_step - - module P : - PROOF - with type lit = Lit.t - and type t = proof - and type proof_step = proof_step - and type term = T.Term.t + module Proof_trace : PROOF_TRACE (** Internal solver, available to theories. *) module Solver_internal : SOLVER_INTERNAL with module T = T and module Lit = Lit - and type proof = proof - and type proof_step = proof_step - and module P = P + and module Proof_trace = Proof_trace type t (** The solver's state. *) @@ -1140,6 +357,8 @@ module type SOLVER = sig type term = T.Term.t type ty = T.Ty.t type lit = Lit.t + type proof = Proof_trace.t + type proof_step = Proof_trace.step_id (** {3 Value registry} *) @@ -1368,195 +587,3 @@ module type SOLVER = sig val pp_stats : t CCFormat.printer (** Print some statistics. What it prints exactly is unspecified. *) end - -(** Helper for the congruence closure - - This helps theories keeping track of some state for each class. - The state of a class is the monoidal combination of the state for each - term in the class (for example, the set of terms in the - class whose head symbol is a datatype constructor). *) -module type MONOID_ARG = sig - module SI : SOLVER_INTERNAL - - type t - (** Some type with a monoid structure *) - - val pp : t Fmt.printer - - val name : string - (** name of the monoid structure (short) *) - - val of_term : - SI.CC.t -> SI.CC.N.t -> SI.T.Term.t -> t option * (SI.CC.N.t * t) list - (** [of_term n t], where [t] is the term annotating node [n], - must return [maybe_m, l], where: - - [maybe_m = Some m] if [t] has monoid value [m]; - otherwise [maybe_m=None] - - [l] is a list of [(u, m_u)] where each [u]'s term - is a direct subterm of [t] - and [m_u] is the monoid value attached to [u]. - *) - - val merge : - SI.CC.t -> - SI.CC.N.t -> - t -> - SI.CC.N.t -> - t -> - SI.CC.Expl.t -> - (t, SI.CC.Expl.t) result - (** Monoidal combination of two values. - - [merge cc n1 mon1 n2 mon2 expl] returns the result of merging - monoid values [mon1] (for class [n1]) and [mon2] (for class [n2]) - when [n1] and [n2] are merged with explanation [expl]. - - @return [Ok mon] if the merge is acceptable, annotating the class of [n1 ∪ n2]; - or [Error expl'] if the merge is unsatisfiable. [expl'] can then be - used to trigger a conflict and undo the merge. - *) -end - -(** State for a per-equivalence-class monoid. - - Helps keep track of monoid state per equivalence class. - A theory might use one or more instance(s) of this to - aggregate some theory-specific state over all terms, with - the information of what terms are already known to be equal - potentially saving work for the theory. *) -module Monoid_of_repr (M : MONOID_ARG) : sig - type t - - val create_and_setup : ?size:int -> M.SI.t -> t - (** Create a new monoid state *) - - val push_level : t -> unit - (** Push backtracking point *) - - val pop_levels : t -> int -> unit - (** Pop [n] backtracking points *) - - val n_levels : t -> int - - val mem : t -> M.SI.CC.N.t -> bool - (** Does the CC node have a monoid value? *) - - val get : t -> M.SI.CC.N.t -> M.t option - (** Get monoid value for this CC node, if any *) - - val iter_all : t -> (M.SI.CC.repr * M.t) Iter.t - val pp : t Fmt.printer -end = struct - module SI = M.SI - module T = SI.T.Term - module N = SI.CC.N - module CC = SI.CC - module N_tbl = Backtrackable_tbl.Make (N) - module Expl = SI.CC.Expl - - type t = { - cc: CC.t; - values: M.t N_tbl.t; (* repr -> value for the class *) - field_has_value: N.bitfield; - (* bit in CC to filter out quickly classes without value *) - } - - let push_level self = N_tbl.push_level self.values - let pop_levels self n = N_tbl.pop_levels self.values n - let n_levels self = N_tbl.n_levels self.values - - let mem self n = - let res = CC.get_bitfield self.cc self.field_has_value n in - assert ( - if res then - N_tbl.mem self.values n - else - true); - res - - let get self n = - if CC.get_bitfield self.cc 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 = - (*Log.debugf 50 (fun k->k "(@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);*) - let maybe_m, l = M.of_term cc n t in - (match maybe_m with - | Some v -> - Log.debugf 20 (fun k -> - k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])" M.name N.pp n M.pp - v); - SI.CC.set_bitfield cc self.field_has_value true n; - N_tbl.add self.values n v - | None -> ()); - List.iter - (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 n N.pp n_u M.pp 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' = - try N_tbl.find self.values n_u - with Not_found -> - Error.errorf "node %a has bitfield but no value" N.pp n_u - in - match M.merge cc n_u m_u n_u m_u' (Expl.mk_list []) with - | Error expl -> - Error.errorf - "when merging@ @[for node %a@],@ values %a and %a:@ conflict %a" - N.pp n_u M.pp m_u M.pp m_u' CC.Expl.pp 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 n N.pp n_u M.pp m_u_merged); - N_tbl.add self.values n_u m_u_merged - ) else ( - (* just add to [n_u] *) - SI.CC.set_bitfield cc self.field_has_value true n_u; - N_tbl.add self.values n_u m_u - )) - l; - () - - let iter_all (self : t) : _ Iter.t = N_tbl.to_iter self.values - - let on_pre_merge (self : t) cc acts n1 n2 e_n1_n2 : unit = - match get self n1, get self n2 with - | Some v1, Some v2 -> - Log.debugf 5 (fun k -> - k - "(@[monoid[%s].on_pre_merge@ (@[:n1 %a@ :val1 %a@])@ (@[:n2 %a@ \ - :val2 %a@])@])" - M.name N.pp n1 M.pp v1 N.pp n2 M.pp v2); - (match M.merge cc n1 v1 n2 v2 e_n1_n2 with - | Ok v' -> - N_tbl.remove self.values n2; - (* only keep repr *) - N_tbl.add self.values n1 v' - | Error expl -> SI.CC.raise_conflict_from_expl cc acts expl) - | None, Some cr -> - SI.CC.set_bitfield cc self.field_has_value true n1; - N_tbl.add self.values n1 cr; - N_tbl.remove self.values n2 (* only keep reprs *) - | Some _, None -> () (* already there on the left *) - | None, None -> () - - let pp out (self : t) : unit = - let pp_e out (t, v) = Fmt.fprintf out "(@[%a@ :has %a@])" N.pp t M.pp v in - Fmt.fprintf out "(@[%a@])" (Fmt.iter pp_e) (iter_all self) - - let create_and_setup ?size (solver : SI.t) : t = - let cc = SI.cc solver in - let field_has_value = - SI.CC.allocate_bitfield ~descr:("monoid." ^ M.name ^ ".has-value") cc - in - let self = { cc; values = N_tbl.create ?size (); field_has_value } in - SI.on_cc_new_term solver (on_new_term self); - SI.on_cc_pre_merge solver (on_pre_merge self); - self -end diff --git a/src/core/dune b/src/core/dune index 946d7159..b95bfa59 100644 --- a/src/core/dune +++ b/src/core/dune @@ -2,4 +2,6 @@ (name Sidekick_core) (public_name sidekick.core) (flags :standard -open Sidekick_util) - (libraries containers iter sidekick.util)) + (libraries containers iter sidekick.util sidekick.sigs.proof-trace + sidekick.sigs.term sidekick.sigs.lit sidekick.sigs.proof.sat + sidekick.sigs.proof.core sidekick.sigs.cc)) diff --git a/src/mini-cc/Sidekick_mini_cc.ml b/src/mini-cc/Sidekick_mini_cc.ml index 996e7ac1..444c0f2f 100644 --- a/src/mini-cc/Sidekick_mini_cc.ml +++ b/src/mini-cc/Sidekick_mini_cc.ml @@ -1,7 +1,9 @@ -module CC_view = Sidekick_core.CC_view +module CC_view = Sidekick_sigs_cc.View + +module type TERM = Sidekick_sigs_term.S module type ARG = sig - module T : Sidekick_core.TERM + module T : TERM val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t end diff --git a/src/mini-cc/Sidekick_mini_cc.mli b/src/mini-cc/Sidekick_mini_cc.mli index 8097c446..85d5b588 100644 --- a/src/mini-cc/Sidekick_mini_cc.mli +++ b/src/mini-cc/Sidekick_mini_cc.mli @@ -1,17 +1,19 @@ -(** {1 Mini congruence closure} +(** Mini congruence closure This implementation is as simple as possible, and doesn't provide backtracking, theories, or explanations. It just decides the satisfiability of a set of (dis)equations. *) -module CC_view = Sidekick_core.CC_view +module CC_view = Sidekick_sigs_cc.View + +module type TERM = Sidekick_sigs_term.S (** Argument for the functor {!Make} It only requires a term structure, and a congruence-oriented view. *) module type ARG = sig - module T : Sidekick_core.TERM + module T : TERM val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t end diff --git a/src/mini-cc/dune b/src/mini-cc/dune index e20dc525..bbcbb9ad 100644 --- a/src/mini-cc/dune +++ b/src/mini-cc/dune @@ -1,5 +1,5 @@ (library (name Sidekick_mini_cc) (public_name sidekick.mini-cc) - (libraries containers iter sidekick.core sidekick.util) + (libraries containers iter sidekick.sigs.cc sidekick.sigs.term sidekick.util) (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util))