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

cleanup: remove a few functions

Browse source
This commit is contained in:
Simon Cruanes 2019-11-01 14:17:28 -05:00
parent 4875b07d0b
commit d4c3d3e443
2 changed files with 0 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/core/Sidekick_core.ml
View file

@ -658,6 +658,5 @@ module type SOLVER = sig
if any, will be a subset of [assumptions]. if any, will be a subset of [assumptions].
@param on_exit functions to be run before this returns *) @param on_exit functions to be run before this returns *)
val pp_term_graph: t CCFormat.printer
val pp_stats : t CCFormat.printer val pp_stats : t CCFormat.printer
end end

18
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -1,8 +1,6 @@
(** {1 Implementation of a Solver using Msat} *) (** {1 Implementation of a Solver using Msat} *)
module Vec = Msat.Vec
module Log = Msat.Log module Log = Msat.Log
module IM = Util.Int_map
module type ARG = sig module type ARG = sig
open Sidekick_core open Sidekick_core
@ -553,10 +551,6 @@ module Make(A : ARG)
(** {2 Main} *) (** {2 Main} *)
(* print all terms reachable from watched literals *)
let pp_term_graph _out (_:t) =
() (* TODO *)
let pp_stats out (self:t) : unit = let pp_stats out (self:t) : unit =
Stat.pp_all out (Stat.all @@ stats self) Stat.pp_all out (Stat.all @@ stats self)
@ -566,11 +560,6 @@ module Make(A : ARG)
let add_clause_l self c = add_clause self (IArray.of_list c) let add_clause_l self c = add_clause self (IArray.of_list c)
(* TODO: remove? use a special constant + micro theory instead?
let[@inline] assume_distinct self l ~neq lit : unit =
CC.assert_distinct (cc self) l lit ~neq
*)
let mk_model (self:t) (lits:lit Iter.t) : Model.t = let mk_model (self:t) (lits:lit Iter.t) : Model.t =
Log.debug 1 "(smt.solver.mk-model)"; Log.debug 1 "(smt.solver.mk-model)";
let module M = Term.Tbl in let module M = Term.Tbl in
@ -592,13 +581,6 @@ module Make(A : ARG)
(* TODO: theory combination *) (* TODO: theory combination *)
Model.Map m Model.Map m
let check_model (_s:t) : unit =
Log.debug 1 "(smt.solver.check-model)";
(* TODO
Sat_solver.check_model s.solver
*)
()
let solve ?(on_exit=[]) ?(check=true) ?(on_progress=fun _ -> ()) let solve ?(on_exit=[]) ?(check=true) ?(on_progress=fun _ -> ())
~assumptions (self:t) : res = ~assumptions (self:t) : res =
let do_on_exit () = let do_on_exit () =