wip: move Value into the arguments to the Solver

src/base-term/Sidekick_base_term.ml

@@ -10,8 +10,6 @@ module Value = Value
 module Term_cell = Term_cell
 module Ty = Ty
 module Lit = Lit
-module Value = Value
-
 
 module Arg
   : Sidekick_core.TERM_LIT

src/cc/Sidekick_cc.ml

@@ -26,15 +26,16 @@ let field_usr2 = Bits.mk_field()
 
 let () = Bits.freeze()
 
-module Make(A: ARG) = struct
-  module A = A
+module Make(CC_A: ARG) = struct
+  module A = CC_A.A
+  module CC_A = CC_A
   type term = A.Term.t
   type term_state = A.Term.state
   type lit = A.Lit.t
   type fun_ = A.Fun.t
   type proof = A.Proof.t
-  type th_data = A.Data.t
-  type actions = A.Actions.t
+  type th_data = CC_A.Data.t
+  type actions = CC_A.Actions.t
 
   module T = A.Term
   module Fun = A.Fun
@@ -97,7 +98,7 @@ module Make(A: ARG) = struct
         n_expl=FL_none;
         n_next=n;
         n_size=1;
-        n_th_data=A.Data.empty;
+        n_th_data=CC_A.Data.empty;
       } in
       n
 
@@ -357,7 +358,7 @@ module Make(A: ARG) = struct
     Vec.clear cc.pending;
     Vec.clear cc.combine;
     Stat.incr cc.count_conflict;
-    A.Actions.raise_conflict acts e A.Proof.default
+    CC_A.Actions.raise_conflict acts e A.Proof.default
 
   let[@inline] all_classes cc : repr Iter.t =
     T_tbl.values cc.tbl
@@ -507,8 +508,8 @@ module Make(A: ARG) = struct
         (fun data f ->
            match f cc n t with
            | None -> data
-           | Some d -> A.Data.merge data d)
-      A.Data.empty cc.on_new_term
+           | Some d -> CC_A.Data.merge data d)
+      CC_A.Data.empty cc.on_new_term
     in
     n.n_th_data <- th_data;
     n
@@ -527,7 +528,7 @@ module Make(A: ARG) = struct
       sub
     in
     let[@inline] return x = Some x in
-    match A.cc_view n.n_term with
+    match CC_A.cc_view n.n_term with
     | Bool _ | Opaque _ -> None
     | Eq (a,b) ->
       let a = deref_sub a in
@@ -655,7 +656,7 @@ module Make(A: ARG) = struct
       begin
         let th_into = r_into.n_th_data in
         let th_from = r_from.n_th_data in
-        let new_data = A.Data.merge th_into th_from in
+        let new_data = CC_A.Data.merge th_into th_from in
         (* restore old data, if it changed *)
         if new_data != th_into then (
           on_backtrack cc (fun () -> r_into.n_th_data <- th_into);
@@ -739,7 +740,7 @@ module Make(A: ARG) = struct
              let e = explain_eq_n ~init:(Lazy.force half_expl) cc u1 t1 in
              List.iter yield e
            in
-           A.Actions.propagate acts lit ~reason A.Proof.default
+           CC_A.Actions.propagate acts lit ~reason A.Proof.default
          | _ -> ())
 
   module Theory = struct
@@ -820,7 +821,7 @@ module Make(A: ARG) = struct
     let t = A.Lit.term lit in
     Log.debugf 5 (fun k->k "(@[cc.assert_lit@ %a@])" A.Lit.pp lit);
     let sign = A.Lit.sign lit in
-    begin match A.cc_view t with
+    begin match CC_A.cc_view t with
       | Eq (a,b) when sign ->
         let a = add_term cc a in
         let b = add_term cc b in

src/cc/Sidekick_cc.mli

@@ -3,4 +3,5 @@
 module type ARG = Sidekick_core.CC_ARG
 module type S = Sidekick_core.CC_S
 
-module Make(A: ARG) : S with module A = A
+module Make(CC_A: ARG)
+  : S with module A=CC_A.A and module CC_A = CC_A

src/core/Sidekick_core.ml

@@ -56,23 +56,29 @@ module type TERM = sig
     val pp : t Fmt.printer
   end
 
-  module Term : sig
-    type t
-    val equal : t -> t -> bool
-    val hash : t -> int
-    val pp : t Fmt.printer
-
-    type state
-
-    val bool : state -> bool -> t
-  end
-
   module Ty : sig
     type t
 
     val equal : t -> t -> bool
     val hash : t -> int
     val pp : t Fmt.printer
+
+    val is_bool : t -> bool
+  end
+
+  module Term : sig
+    type t
+    val equal : t -> t -> bool
+    val hash : t -> int
+    val pp : t Fmt.printer
+    val ty : t -> Ty.t
+
+    val iter_dag : t -> t Iter.t
+    (** Iterate over the subterms, using sharing *)
+
+    type state
+
+    val bool : state -> bool -> t
   end
 end
 
@@ -94,14 +100,23 @@ module type TERM_LIT = sig
     val norm_sign : t -> t * bool
     (** Invariant: if [u, sign = norm_sign t] then [apply_sign u sign = t] *)
 
-
     val atom : Term.state -> ?sign:bool -> Term.t -> t
   end
 end
 
-module type TERM_LIT_PROOF = sig
+module type CORE_TYPES = sig
   include TERM_LIT
 
+  (** {3 Semantic values} *)
+  module Value : sig
+    type t
+
+    val equal : t -> t -> bool
+    val hash : t -> int
+    val ty : t -> Ty.t
+    val pp : t Fmt.printer
+  end
+
   module Proof : sig
     type t
     val pp : t Fmt.printer
@@ -115,7 +130,8 @@ module type TERM_LIT_PROOF = sig
 end
 
 module type CC_ARG = sig
-  include TERM_LIT_PROOF
+  module A : CORE_TYPES
+  open A
 
   val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) CC_view.t
   (** View the term through the lens of the congruence closure *)
@@ -138,14 +154,15 @@ module type CC_ARG = sig
 end
 
 module type CC_S = sig
-  module A : CC_ARG
+  module A : CORE_TYPES
+  module CC_A : CC_ARG with module A=A
   type term_state = A.Term.state
   type term = A.Term.t
   type fun_ = A.Fun.t
   type lit = A.Lit.t
   type proof = A.Proof.t
-  type th_data = A.Data.t
-  type actions = A.Actions.t
+  type th_data = CC_A.Data.t
+  type actions = CC_A.Actions.t
 
   type t
   (** Global state of the congruence closure *)
@@ -326,8 +343,9 @@ type ('model, 'proof, 'ucore, 'unknown) solver_res =
 
 (** A view of the solver from a theory's point of view *)
 module type SOLVER_INTERNAL = sig
-  module A : CC_ARG
-  module CC : CC_S with module A = A
+  module A : CORE_TYPES
+  module CC : CC_S with module A=A
+  module CC_A = CC.CC_A
 
   type ty = A.Ty.t
   type lit = A.Lit.t
@@ -367,7 +385,7 @@ module type SOLVER_INTERNAL = sig
 
     type 'a data = (module MERGE_PP with type t = 'a)
 
-    val create : solver -> 'a data -> 'a t
+    val create : 'a data -> 'a t
     (** Create a key for storing and accessing data of type ['a].
         Values have to be mergeable. *)
   end
@@ -473,16 +491,17 @@ end
 
 (** Public view of the solver *)
 module type SOLVER = sig
-  module Solver_internal : SOLVER_INTERNAL
+  module A : CORE_TYPES
+  module Solver_internal : SOLVER_INTERNAL with module A = A
   (** Internal solver, available to theories.  *)
 
-  module A = Solver_internal.A
   type t
   type solver = t
   type term = A.Term.t
   type ty = A.Ty.t
   type lit = A.Lit.t
   type proof = A.Proof.t
+  type value = A.Value.t
 
   (** {3 A theory}
 
@@ -520,12 +539,6 @@ module type SOLVER = sig
   type theory = (module THEORY)
   (** A theory that can be used for this particular solver. *)
 
-  type theory_with_st = Tst : {
-      m: (module THEORY with type t = 'th);
-      st: 'th;
-    } -> theory_with_st
-  (** An instantiated theory *)
-
   val mk_theory :
     name:string ->
     create_and_setup:(Solver_internal.t -> 'th) ->
@@ -544,16 +557,6 @@ module type SOLVER = sig
     val pp : t CCFormat.printer
   end
 
-  (** {3 Semantic values} *)
-  module Value : sig
-    type t
-
-    val equal : t -> t -> bool
-    val hash : t -> int
-    val ty : t -> ty
-    val pp : t Fmt.printer
-  end
-
   module Model : sig
     type t
 
@@ -561,9 +564,9 @@ module type SOLVER = sig
 
     val mem : term -> t -> bool
 
-    val find : term -> t -> Value.t option
+    val find : term -> t -> value option
 
-    val eval : t -> term -> Value.t option
+    val eval : t -> term -> value option
 
     val pp : t Fmt.printer
   end