remove dead code, some printing info

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")

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

src/th-data/Sidekick_th_data.ml

@@ -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);