simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-29 04:44:52 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: missing type equality

Browse source
This commit is contained in:
Simon Cruanes 2019-11-01 15:10:43 -05:00
parent d4c3d3e443
commit 5b3cadf1e1
1 changed files with 7 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/core/Sidekick_core.ml
View file

@ -10,12 +10,6 @@
module Fmt = CCFormat module Fmt = CCFormat
module type MERGE_PP = sig
type t
val merge : t -> t -> t
val pp : t Fmt.printer
end
module CC_view = struct module CC_view = struct
type ('f, 't, 'ts) t = type ('f, 't, 'ts) t =
| Bool of bool | Bool of bool
@ -330,6 +324,10 @@ module type SOLVER_INTERNAL = sig
val tst : t -> term_state val tst : t -> term_state
val stats : t -> Stat.t val stats : t -> Stat.t
(** {3 Actions for the theories} *)
type actions
(** {3 Literals} (** {3 Literals}
A literal is a (preprocessed) term along with its sign. A literal is a (preprocessed) term along with its sign.
@ -345,6 +343,7 @@ module type SOLVER_INTERNAL = sig
with module T = T with module T = T
and module P = P and module P = P
and module Lit = Lit and module Lit = Lit
and type Actions.t = actions
val cc : t -> CC.t val cc : t -> CC.t
(** Congruence closure for this solver *) (** Congruence closure for this solver *)
@ -377,8 +376,6 @@ module type SOLVER_INTERNAL = sig
(** {3 hooks for the theory} *) (** {3 hooks for the theory} *)
type actions
val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> proof -> unit val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> proof -> unit
val raise_conflict : t -> actions -> lit list -> proof -> 'a val raise_conflict : t -> actions -> lit list -> proof -> 'a
@ -505,7 +502,8 @@ module type SOLVER = sig
so they can work with any implementation. so they can work with any implementation.
Typically a theory should be a functor taking an argument containing Typically a theory should be a functor taking an argument containing
a [SOLVER_INTERNAL] and some additional views on terms, literals, etc. a [SOLVER_INTERNAL] or even a full [SOLVER],
and some additional views on terms, literals, etc.
that are specific to the theory (e.g. to map terms to linear that are specific to the theory (e.g. to map terms to linear
expressions). expressions).
The theory can then be instantiated on any kind of solver for any The theory can then be instantiated on any kind of solver for any