mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-12 05:58:46 -05:00
wip: continue refactor
This commit is contained in:
Simon Cruanes
parent
4d312ad1aa
commit
4fd291b117
9 changed files with 135 additions and 93 deletions
|
|
@ -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 "(@[<hv1>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;
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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 =
|
||||
|
|
|
|||
2
src/dune
2
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)))
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
)));
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
()
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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 "(@[<hv>%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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue