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

feat: function to add a theory and retain its state

Browse source
This commit is contained in:
Simon Cruanes 2019-06-10 14:16:09 -05:00
parent 128e7dceb8
commit b2f6a30cc8
2 changed files with 16 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/core/Sidekick_core.ml
View file

@ -502,6 +502,10 @@ module type SOLVER = sig
type theory = (module THEORY)
(** A theory that can be used for this particular solver. *)
type 'a theory_p = (module THEORY with type t = 'a)
(** A theory that can be used for this particular solver, with state
of type ['a]. *)
val mk_theory :
name:string ->
create_and_setup:(Solver_internal.t -> 'th) ->
@ -584,6 +588,11 @@ module type SOLVER = sig
any call to {!solve} or to {!add_clause} and the likes (otherwise
the theory will have a partial view of the problem). *)
val add_theory_p : t -> 'a theory_p -> 'a
(** Add the given theory and obtain its state *)
val add_theory_l : t -> theory list -> unit
val mk_atom_lit : t -> lit -> Atom.t
val mk_atom_t : t -> ?sign:bool -> term -> Atom.t

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

@ -388,10 +388,11 @@ module Make(A : ARG)
end
type theory = (module THEORY)
type 'a theory_p = (module THEORY with type t = 'a)
(** {2 Main} *)
let add_theory (self:t) (th:theory) : unit =
let add_theory_p (type a) (self:t) (th:a theory_p) : a =
let (module Th) = th in
Log.debugf 2
(fun k-> k "(@[msat-solver.add-theory@ :name %S@])" Th.name);
@ -406,7 +407,11 @@ module Make(A : ARG)
next=self.si.th_states;
};
end;
()
st
let add_theory (self:t) (th:theory) : unit =
let (module Th) = th in
ignore (add_theory_p self (module Th))
let add_theory_l self = List.iter (add_theory self)