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

fix: restore the module type coercion

Browse source
This commit is contained in:
Simon Cruanes 2019-06-07 17:55:22 -05:00
parent c9d8fd2f51
commit d1aec70cbe
1 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -12,7 +12,7 @@ end
module type S = Sidekick_core.SOLVER
module Make(A : ARG)
(* : S with module A = A *)
: S with module A = A
= struct
module A = A
module T = A.Term
@ -21,7 +21,7 @@ module Make(A : ARG)
type ty = Ty.t
type lemma = A.Proof.t
module Lit = struct
module Lit_ = struct
type t = {
lit_term: term;
lit_sign : bool
@ -61,15 +61,15 @@ module Make(A : ARG)
let norm l = let l, sign = norm_sign l in l, if sign then Msat.Same_sign else Msat.Negated
end
type lit = Lit.t
type lit = Lit_.t
(* actions from msat *)
type msat_acts = (Msat.void, Lit.t, Msat.void, A.Proof.t) Msat.acts
type msat_acts = (Msat.void, lit, Msat.void, A.Proof.t) Msat.acts
(* the full argument to the congruence closure *)
module CC_A = struct
module A = A
module Lit = Lit
module Lit = Lit_
let cc_view = A.cc_view
module Actions = struct
@ -90,7 +90,7 @@ module Make(A : ARG)
module Solver_internal = struct
module A = A
module CC_A = CC_A
module Lit = Lit
module Lit = Lit_
module CC = CC
module N = CC.N
type term = T.t
@ -360,6 +360,7 @@ module Make(A : ARG)
ignore (Lazy.force @@ self.cc : CC.t);
self
end
module Lit = Solver_internal.Lit
(** the parametrized SAT Solver *)
module Sat_solver = Msat.Make_cdcl_t(Solver_internal)