From 5b3cadf1e17be99396ef0018189856087a5abd30 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 1 Nov 2019 15:10:43 -0500 Subject: [PATCH] fix: missing type equality --- src/core/Sidekick_core.ml | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 9ed15426..6be110ba 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -10,12 +10,6 @@ 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 type ('f, 't, 'ts) t = | Bool of bool @@ -330,6 +324,10 @@ module type SOLVER_INTERNAL = sig val tst : t -> term_state val stats : t -> Stat.t + (** {3 Actions for the theories} *) + + type actions + (** {3 Literals} A literal is a (preprocessed) term along with its sign. @@ -345,6 +343,7 @@ module type SOLVER_INTERNAL = sig with module T = T and module P = P and module Lit = Lit + and type Actions.t = actions val cc : t -> CC.t (** Congruence closure for this solver *) @@ -377,8 +376,6 @@ module type SOLVER_INTERNAL = sig (** {3 hooks for the theory} *) - type actions - val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> proof -> unit val raise_conflict : t -> actions -> lit list -> proof -> 'a @@ -505,7 +502,8 @@ module type SOLVER = sig so they can work with any implementation. 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 expressions). The theory can then be instantiated on any kind of solver for any