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

cleanup

Browse source
This commit is contained in:
Simon Cruanes 2022-08-21 13:53:48 -04:00
parent 007fbad243
commit e34f5a5c3c
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 2 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/solver.ml
View file

@ -212,7 +212,8 @@ let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
Log.debugf 5 (fun k ->
let ppc out n =
Fmt.fprintf out "{@[<hv>class@ %a@]}" (Util.pp_iter E_node.pp)
Fmt.fprintf out "{@[<hv1>class@ %a@]}"
(Util.pp_iter ~sep:";" E_node.pp)
(E_node.iter_class n)
in
k "(@[sidekick.smt-solver.classes@ (@[%a@])@])" (Util.pp_iter ppc)

12
src/smt/solver_internal.ml
View file

@ -312,18 +312,6 @@ let cc_resolve_expl self e : lit list * _ =
let r = CC.explain_expl (cc self) e in
r.lits, r.pr self.proof
(*
let cc_merge self _acts n1 n2 e = CC.merge (cc self) n1 n2 e
let cc_merge_t self acts t1 t2 e =
let cc_acts = mk_cc_acts_ self.proof acts in
cc_merge self cc_acts (cc_add_term self t1) (cc_add_term self t2) e
let cc_raise_conflict_expl self acts e =
let cc_acts = mk_cc_acts_ self.proof acts in
CC.raise_conflict_from_expl (cc self) cc_acts e
*)
(** {2 Interface with the SAT solver} *)
let rec push_lvl_ = function