From d527b2b9459ec34b94d8bac44c5cd516121466ef Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 31 Jul 2019 03:25:04 -0500 Subject: [PATCH] fix: remove some module aliases for 4.08 --- src/cc/Sidekick_cc.ml | 21 +++++----- src/cc/Sidekick_cc.mli | 2 +- src/core/Sidekick_core.ml | 38 ++++++++----------- src/smtlib/Process.ml | 2 +- src/th-bool-static/Sidekick_th_bool_static.ml | 10 ++--- 5 files changed, 32 insertions(+), 41 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index bd48ca08..9f48086b 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -13,17 +13,16 @@ module type ARG = Sidekick_core.CC_ARG module type S = Sidekick_core.CC_S module Make(CC_A: ARG) = struct - module CC_A = CC_A - module A = CC_A.A - type term = A.Term.t - type term_state = A.Term.state - type lit = CC_A.Lit.t - type fun_ = A.Fun.t - type proof = A.Proof.t - type actions = CC_A.Actions.t + module A = CC_A + type term = A.A.Term.t + type term_state = A.A.Term.state + type lit = A.Lit.t + type fun_ = A.A.Fun.t + type proof = A.A.Proof.t + type actions = A.Actions.t - module T = A.Term - module Fun = A.Fun + module T = A.A.Term + module Fun = A.A.Fun module Lit = CC_A.Lit module Bits : sig @@ -353,7 +352,7 @@ module Make(CC_A: ARG) = struct Vec.clear cc.combine; List.iter (fun f -> f cc e) cc.on_conflict; Stat.incr cc.count_conflict; - CC_A.Actions.raise_conflict acts e A.Proof.default + CC_A.Actions.raise_conflict acts e A.A.Proof.default let[@inline] all_classes cc : repr Iter.t = T_tbl.values cc.tbl diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli index 298146aa..07259b23 100644 --- a/src/cc/Sidekick_cc.mli +++ b/src/cc/Sidekick_cc.mli @@ -3,4 +3,4 @@ module type ARG = Sidekick_core.CC_ARG module type S = Sidekick_core.CC_S -module Make(CC_A: ARG) : S with module CC_A = CC_A +module Make(A: ARG) : S with module A = A diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 845ef121..a4febe7a 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -124,14 +124,13 @@ module type CC_ARG = sig end module type CC_S = sig - module CC_A : CC_ARG - module A = CC_A.A - type term_state = A.Term.state - type term = A.Term.t - type fun_ = A.Fun.t - type lit = CC_A.Lit.t - type proof = A.Proof.t - type actions = CC_A.Actions.t + module A : CC_ARG + type term_state = A.A.Term.state + type term = A.A.Term.t + type fun_ = A.A.Fun.t + type lit = A.Lit.t + type proof = A.A.Proof.t + type actions = A.Actions.t type t (** Global state of the congruence closure *) @@ -303,7 +302,7 @@ end module type SOLVER_INTERNAL = sig module A : TERM_PROOF module CC_A : CC_ARG with module A = A - module CC : CC_S with module CC_A = CC_A + module CC : CC_S with module A = CC_A type ty = A.Ty.t type term = A.Term.t @@ -314,9 +313,6 @@ module type SOLVER_INTERNAL = sig type t type solver = t - module Expl = CC.Expl - module N = CC.N - val tst : t -> term_state val cc : t -> CC.t @@ -401,31 +397,31 @@ module type SOLVER_INTERNAL = sig (** Add the given (signed) bool term to the SAT solver, so it gets assigned a boolean value *) - val cc_raise_conflict_expl : t -> actions -> Expl.t -> 'a + val cc_raise_conflict_expl : t -> actions -> CC.Expl.t -> 'a (** Raise a conflict with the given congruence closure explanation. it must be a theory tautology that [expl ==> absurd]. To be used in theories. *) - val cc_find : t -> N.t -> N.t + val cc_find : t -> CC.N.t -> CC.N.t (** Find representative of the node *) - val cc_merge : t -> actions -> N.t -> N.t -> Expl.t -> unit + val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit (** Merge these two nodes in the congruence closure, given this explanation. It must be a theory tautology that [expl ==> n1 = n2]. To be used in theories. *) - val cc_merge_t : t -> actions -> term -> term -> Expl.t -> unit + val cc_merge_t : t -> actions -> term -> term -> CC.Expl.t -> unit (** Merge these two terms in the congruence closure, given this explanation. See {!cc_merge} *) - val cc_add_term : t -> term -> N.t + val cc_add_term : t -> term -> CC.N.t (** Add/retrieve congruence closure node for this term. To be used in theories *) - val on_cc_merge : t -> (CC.t -> actions -> N.t -> N.t -> Expl.t -> unit) -> unit + val on_cc_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> unit (** Callback for when two classes containing data for this key are merged *) - val on_cc_new_term : t -> (CC.t -> N.t -> term -> unit) -> unit + val on_cc_new_term : t -> (CC.t -> CC.N.t -> term -> unit) -> unit (** Callback to add data on terms when they are added to the congruence closure *) @@ -473,8 +469,6 @@ module type SOLVER = sig module Solver_internal : SOLVER_INTERNAL with module A = A and module CC_A = CC_A (** Internal solver, available to theories. *) - module Lit = Solver_internal.Lit - type t type solver = t type term = A.Term.t @@ -539,7 +533,7 @@ module type SOLVER = sig val hash : t -> int val pp : t CCFormat.printer - val formula : t -> Lit.t + val formula : t -> lit val sign : t -> bool end diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 1287d5a0..b9c7e7df 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -406,7 +406,7 @@ end module Solver = Sidekick_msat_solver.Make(Solver_arg) module Check_cc = struct - module Lit = Solver.Lit + module Lit = Solver.Solver_internal.Lit module SI = Solver.Solver_internal module CC = Solver.Solver_internal.CC module MCC = Sidekick_mini_cc.Make(Solver_arg) diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index e5ce0711..c6f692af 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -34,17 +34,15 @@ end module type S = sig module A : ARG - module T = A.S.A.Term - module SI = A.S.Solver_internal type state - val create : T.state -> state + val create : A.S.A.Term.state -> state - val simplify : state -> SI.simplify_hook + val simplify : state -> A.S.Solver_internal.simplify_hook (** Simplify given term *) - val cnf : state -> SI.preprocess_hook + val cnf : state -> A.S.Solver_internal.preprocess_hook (** add clauses for the booleans within the term. *) val theory : A.S.theory @@ -54,7 +52,7 @@ module Make(A : ARG) : S with module A = A = struct module A = A module Ty = A.S.A.Ty module T = A.S.A.Term - module Lit = A.S.Lit + module Lit = A.S.Solver_internal.Lit module SI = A.S.Solver_internal type state = {