simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 12:15:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: theories

Browse source
This commit is contained in:
Simon Cruanes 2019-06-01 16:56:05 -05:00
parent 44259ec5fc
commit fc80d8c6e9
3 changed files with 19 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/th-cstor/Sidekick_th_cstor.ml
View file

@ -38,9 +38,9 @@ module Make(A : ARG) : S with module A = A = struct
let merge x _ = x
end
type t = {
k: data SI.Key.t;
}
let k = SI.Key.create (module Data)
type t = unit
let on_merge (solver:SI.t) n1 tc1 n2 tc2 e_n1_n2 : unit =
Log.debugf 5
@ -69,10 +69,9 @@ module Make(A : ARG) : S with module A = A = struct
| _ -> None
let create_and_setup (solver:SI.t) : t =
let k = SI.Key.create solver (module Data) in
SI.on_cc_merge solver ~k on_merge;
SI.on_cc_new_term solver ~k on_new_term;
{k}
()
let theory = A.S.mk_theory ~name ~create_and_setup ()
end

9
src/th-distinct/Sidekick_th_distinct.ml
View file

@ -62,9 +62,11 @@ module Make(A : ARG) : S with module A = A = struct
m1 m2
in ()
let k = SI.Key.create (module Data)
module T_tbl = CCHashtbl.Make(T)
type t = {
k: Data.t SI.Key.t;
expanded: unit T_tbl.t; (* negative "distinct" that have been case-split on *)
}
@ -79,7 +81,7 @@ module Make(A : ARG) : S with module A = A = struct
subs
(fun sub ->
let n = SI.cc_add_term solver sub in
SI.cc_add_data solver n ~k:self.k (IM.singleton lit sub));
SI.cc_add_data solver n ~k (IM.singleton lit sub));
) else if not @@ T_tbl.mem self.expanded lit_t then (
(* add clause [distinct t1…tn ∨ ∨_{i,j>i} t_i=j] *)
T_tbl.add self.expanded lit_t ();
@ -104,8 +106,7 @@ module Make(A : ARG) : S with module A = A = struct
| Some subs -> process_lit st solver lit t subs)
let create_and_setup (solver:SI.t) : t =
let k = SI.Key.create solver (module Data) in
let self = { expanded=T_tbl.create 8; k; } in
let self = { expanded=T_tbl.create 8; } in
SI.on_cc_merge solver ~k on_merge;
SI.on_final_check solver (partial_check self);
self

22
src/th-ite/Sidekick_th_ite.ml
View file

@ -42,16 +42,16 @@ module Make(A : ARG)
let merge = A.T_set.union
end
type t = {
k: Data.t Solver.Key.t;
}
let k = Solver.Key.create (module Data)
let on_merge (self:t) (solver:Solver.t) n1 n2 e_n1_n2 : unit =
type t = unit
let on_merge (solver:Solver.t) n1 n2 e_n1_n2 : unit =
Log.debugf 5
(fun k->k "(@[th-ite.on_merge@ :c1 %a@ :c2 %a@])" N.pp n1 N.pp n2);
(* check if [n1] has some [ite] parents, and if [n2] is true/false *)
let check_ n1 n2 =
match Solver.cc_data solver ~k:self.k n1, A.view_as_ite (N.term n2) with
match Solver.cc_data solver ~k n1, A.view_as_ite (N.term n2) with
| Some set, T_bool n2_true ->
assert (not @@ A.T_set.is_empty set);
A.T_set.iter
@ -77,21 +77,19 @@ module Make(A : ARG)
check_ n2 n1;
()
let on_new_term (self:t) (solver:Solver.t) _n (t:T.t) =
let on_new_term (solver:Solver.t) _n (t:T.t) =
match A.view_as_ite t with
| T_ite (a,_,_) ->
(* add [t] to parents of [a] *)
let n_a = Solver.cc_find solver @@ Solver.cc_add_term solver a in
Solver.cc_add_data solver n_a ~k:self.k (A.T_set.singleton t);
Solver.cc_add_data solver n_a ~k (A.T_set.singleton t);
None
| _ -> None
let create_and_setup (solver:Solver.t) : t =
let k = Solver.Key.create solver (module Data) in
let self = {k} in
Solver.on_cc_merge_all solver (on_merge self);
Solver.on_cc_new_term solver ~k (on_new_term self);
self
Solver.on_cc_merge_all solver on_merge;
Solver.on_cc_new_term solver ~k on_new_term;
()
let theory = A.S.mk_theory ~name:"ite" ~create_and_setup ()
end