diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml index c9234d9e..0d7ef5b5 100644 --- a/src/smt/Congruence_closure.ml +++ b/src/smt/Congruence_closure.ml @@ -253,15 +253,9 @@ let rec decompose_explain cc (e:explanation): unit = | E_reduction -> () | E_lit lit -> ps_add_lit cc lit | E_lits l -> List.iter (ps_add_lit cc) l - | E_custom {args;_} -> - (* decompose sub-expls *) - List.iter (decompose_explain cc) args - | E_reduce_eq (a, b) -> - ps_add_obligation cc a b; - | E_injectivity (t1,t2) -> - (* arguments of [t1], [t2] are equal by injectivity, so we - just need to explain why [t1=t2] *) - ps_add_obligation cc t1 t2 + | E_merges l -> + (* need to explain each merge in [l] *) + List.iter (fun (t,u) -> ps_add_obligation cc t u) l | E_congruence (t1,t2) -> (* [t1] and [t2] must be applications of the same symbol to arguments that are pairwise equal *) @@ -366,7 +360,7 @@ let rec update_pending (cc:t): unit = add_signature cc n.n_term (find cc n) | Some u -> (* must combine [t] with [r] *) - push_combine cc n u(E_congruence (n,u)) + push_combine cc n u (Explanation.mk_congruence n u) end; (* FIXME: when to actually evaluate? eval_pending cc; @@ -490,15 +484,6 @@ and notify_merge cc (ra:repr) ~into:(rb:repr) (e:explanation): unit = let (module A) = cc.acts in A.on_merge ra rb e - -(* FIXME: callback? -(* evaluation rules: if, case... *) -and eval_pending (t:term): unit = - List.iter - (fun ((module Theory):repr theory) -> Theory.eval t) - theories - *) - (* add [t] to [cc] when not present already *) and add_new_term cc (t:term) : node = assert (not @@ mem cc t); @@ -625,7 +610,7 @@ let create ?(size=2048) ~actions (tst:Term.state) : t = tbl = Term.Tbl.create size; signatures_tbl = Sig_tbl.create size; pending=Vec.make_empty Equiv_class.dummy; - combine= Vec.make_empty (nd,nd,E_reduce_eq(nd,nd)); + combine= Vec.make_empty (nd,nd,E_reduction); ps_lits=Lit.Set.empty; ps_queue=Vec.make_empty (nd,nd); true_ = lazy (add cc (Term.true_ tst)); diff --git a/src/smt/Explanation.ml b/src/smt/Explanation.ml index 91a2c649..19b866ff 100644 --- a/src/smt/Explanation.ml +++ b/src/smt/Explanation.ml @@ -2,22 +2,23 @@ open Solver_types type t = explanation = - | E_reduction - | E_lit of lit - | E_lits of lit list - | E_congruence of cc_node * cc_node - | E_injectivity of cc_node * cc_node - | E_reduce_eq of cc_node * cc_node - | E_custom of { - name : ID.t; args : explanation list; - pp : (ID.t * explanation list) Fmt.printer; - } + | E_reduction (* by pure reduction, tautologically equal *) + | E_merges of (cc_node * cc_node) list (* caused by these merges *) + | E_lit of lit (* because of this literal *) + | E_lits of lit list (* because of this (true) conjunction *) + | E_congruence of cc_node * cc_node (* these terms are congruent *) let compare = cmp_exp let equal a b = cmp_exp a b = 0 let pp = pp_explanation +let mk_merges l : t = E_merges l +let mk_lit l : t = E_lit l +let mk_lits = function [x] -> mk_lit x | l -> E_lits l +let mk_reduction : t = E_reduction +let mk_congruence t u = E_congruence (t,u) + let[@inline] lit l : t = E_lit l module Set = CCSet.Make(struct diff --git a/src/smt/Solver_types.ml b/src/smt/Solver_types.ml index 29fd2298..ac0cb093 100644 --- a/src/smt/Solver_types.ml +++ b/src/smt/Solver_types.ml @@ -104,16 +104,10 @@ and explanation_forest_link = (* atomic explanation in the congruence closure *) and explanation = | E_reduction (* by pure reduction, tautologically equal *) + | E_merges of (cc_node * cc_node) list (* caused by these merges *) | E_lit of lit (* because of this literal *) | E_lits of lit list (* because of this (true) conjunction *) | E_congruence of cc_node * cc_node (* these terms are congruent *) - | E_injectivity of cc_node * cc_node (* injective function *) - | E_reduce_eq of cc_node * cc_node (* reduce because those are equal by reduction *) - | E_custom of { - name: ID.t; (* name of the rule *) - args: explanation list; (* sub-explanations *) - pp: (ID.t * explanation list) Fmt.printer; - } (** Custom explanation, typically for theories *) (* boolean literal *) and lit = { @@ -229,26 +223,20 @@ let cmp_cc_node a b = term_cmp_ a.n_term b.n_term let rec cmp_exp a b = let toint = function - | E_congruence _ -> 0 | E_lit _ -> 1 - | E_reduction -> 2 | E_injectivity _ -> 3 - | E_reduce_eq _ -> 5 - | E_custom _ -> 6 - | E_lits _ -> 7 + | E_merges _ -> 0 | E_lit _ -> 1 + | E_reduction -> 2 | E_lits _ -> 3 + | E_congruence _ -> 4 in begin match a, b with | E_congruence (t1,t2), E_congruence (u1,u2) -> CCOrd.(cmp_cc_node t1 u1 (cmp_cc_node, t2, u2)) + | E_merges l1, E_merges l2 -> + CCList.compare (CCOrd.pair cmp_cc_node cmp_cc_node) l1 l2 | E_reduction, E_reduction -> 0 | E_lit l1, E_lit l2 -> cmp_lit l1 l2 | E_lits l1, E_lits l2 -> CCList.compare cmp_lit l1 l2 - | E_injectivity (t1,t2), E_injectivity (u1,u2) -> - CCOrd.(cmp_cc_node t1 u1 (cmp_cc_node, t2, u2)) - | E_reduce_eq (t1, u1), E_reduce_eq (t2,u2) -> - CCOrd.(cmp_cc_node t1 t2 (cmp_cc_node, u1, u2)) - | E_custom r1, E_custom r2 -> - CCOrd.(ID.compare r1.name r2.name (list cmp_exp, r1.args, r2.args)) - | E_congruence _, _ | E_lit _, _ | E_reduction, _ | E_lits _, _ - | E_injectivity _, _ | E_reduce_eq _, _ | E_custom _, _ + | E_merges _, _ | E_lit _, _ | E_lits _, _ + | E_reduction, _ | E_congruence _, _ -> CCInt.compare (toint a)(toint b) end @@ -323,8 +311,8 @@ let pp_explanation out (e:explanation) = match e with | E_lits l -> CCFormat.Dump.list pp_lit out l | E_congruence (a,b) -> Format.fprintf out "(@[congruence@ %a@ %a@])" pp_cc_node a pp_cc_node b - | E_injectivity (a,b) -> - Format.fprintf out "(@[injectivity@ %a@ %a@])" pp_cc_node a pp_cc_node b - | E_reduce_eq (t, u) -> - Format.fprintf out "(@[reduce_eq@ %a@ %a@])" pp_cc_node t pp_cc_node u - | E_custom {name; args; pp} -> pp out (name,args) + | E_merges l -> + Format.fprintf out "(@[merges@ %a@])" + Fmt.(list ~sep:(return "@ ") @@ within "[" "]" @@ hvbox @@ + pair ~sep:(return "@ <-> ") pp_cc_node pp_cc_node) + l