From 11d8f8e879573890b72b52205e91d05af0f2345b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 15 Feb 2020 14:33:44 -0600 Subject: [PATCH] remove dead code, some printing info --- src/core/Sidekick_core.ml | 8 ++++- src/msat-solver/Sidekick_msat_solver.ml | 4 ++- src/th-data/Sidekick_th_data.ml | 39 +++++-------------------- 3 files changed, 18 insertions(+), 33 deletions(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 55c4d657..7baf5fa6 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -465,7 +465,8 @@ module type SOLVER_INTERNAL = sig Must be complete (i.e. must raise a conflict if the set of literals is not satisfiable) and can be expensive. The function - is given the whole trail. *) + is given the whole trail. + *) (** {3 Preprocessors} These preprocessors turn mixed, raw literals (possibly simplified) into @@ -702,6 +703,7 @@ module Monoid_of_repr(M : MONOID_ARG) : sig val mem : t -> M.SI.CC.N.t -> bool val get : t -> M.SI.CC.N.t -> M.t option 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 @@ -799,6 +801,10 @@ end = struct | None, None -> () end + 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.seq pp_e) (iter_all self) + let create_and_setup ?size (solver:SI.t) : t = let field_has_value = SI.CC.allocate_bitfield ~descr:("monoid."^M.name^".has-value") diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index be1a4be8..a574d0ba 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -312,8 +312,10 @@ module Make(A : ARG) (* transmit to theories. *) CC.check cc acts; if final then ( + for _i = 0 to 1 do List.iter (fun f -> f self acts lits) self.on_final_check; CC.check cc acts; + done; (* FIXME *) (* TODO: theory combination until fixpoint *) ) else ( List.iter (fun f -> f self acts lits) self.on_partial_check; @@ -598,7 +600,7 @@ module Make(A : ARG) Stat.incr self.count_solve; match r with | Sat_solver.Sat st -> - Log.debugf 1 (fun k->k "SAT"); + Log.debug 1 "sidekick.msat-solver: SAT"; let _lits f = st.iter_trail f (fun _ -> ()) in (* TODO: theory combination *) let m = mk_model self _lits in diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index b8465bbd..983db001 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -165,7 +165,7 @@ module Make(A : ARG) : S with module A = A = struct let merge cc n1 c1 n2 c2 e_n1_n2 : _ result = 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 n1 pp c1 N.pp n2 pp 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 = @@ -242,7 +242,7 @@ module Make(A : ARG) : S with module A = A = struct let merge cc n1 v1 n2 v2 _e : _ result = 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 n1 pp v1 N.pp n2 pp 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;} @@ -274,33 +274,6 @@ module Make(A : ARG) : S with module A = A = struct N_tbl.pop_levels self.to_decide n; () - (* TODO: select/is-a *) - - (* TODO: remove - (* attach data to constructor terms *) - let on_new_term_look_at_shape self n (t:T.t) = - match A.view_as_data t with - | T_cstor (cstor,args) -> - Log.debugf 20 - (fun k->k "(@[%s.on-new-term@ %a@ :cstor %a@ @[:args@ (@[%a@])@]@]@])" - name T.pp t A.Cstor.pp cstor (Util.pp_iarray T.pp) args); - N_tbl.add self.cstors n {n; t; cstor; args}; - | T_select (cstor,i,u) -> - Log.debugf 20 - (fun k->k "(@[%s.on-new-term.select[%d]@ %a@ :cstor %a@ :in %a@])" - name i T.pp t A.Cstor.pp cstor T.pp u); - (* TODO: remember that [u] must be decided *) - () - (* N_tbl.add self.cstors n {n; t; cstor; args}; *) - | T_is_a (cstor,u) -> - Log.debugf 20 - (fun k->k "(@[%s.on-new-term.is-a@ %a@ :cstor %a@ :in %a@])" - name T.pp t A.Cstor.pp cstor T.pp u); - () - (* N_tbl.add self.cstors n {n; t; cstor; args}; *) - | T_other _ -> () - *) - (* remember terms of a datatype *) let on_new_term_look_at_ty (self:t) n (t:T.t) : unit = let ty = T.ty t in @@ -497,7 +470,11 @@ module Make(A : ARG) : S with module A = A = struct |> Iter.to_rev_list in begin match remaining_to_decide with - | [] -> () + | [] -> + Log.debugf 10 + (fun k->k "(@[%s.final-check.all-decided@ :cstors %a@ :parents %a@])" + name ST_cstors.pp self.cstors ST_parents.pp self.parents); + () | l -> Log.debugf 10 (fun k->k "(@[%s.final-check.must-decide@ %a@])" name (Util.pp_list N.pp) l); @@ -509,7 +486,7 @@ module Make(A : ARG) : S with module A = A = struct if not @@ T.Tbl.mem self.case_split_done t then ( T.Tbl.add self.case_split_done t (); let c = - cstors_of_ty (T.ty t) + cstors_of_ty (T.ty t) |> Iter.map (fun c -> A.mk_is_a self.tst c t) |> Iter.map (fun t ->