From 080a20480fddf72ae9fb27938c0f823f021cdf86 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 27 May 2019 19:55:21 -0500
Subject: [PATCH] refactor: continue functorization of sidekick

---
 src/base-term/Sidekick_base_term.ml     |  27 ++
 src/base-term/dune                      |   2 +-
 src/cc/Sidekick_cc.ml                   |  13 +-
 src/core/Sidekick_core.ml               | 111 ++---
 src/main/dune                           |   3 +-
 src/mini-cc/Mini_cc.ml                  |  16 +-
 src/mini-cc/Mini_cc.mli                 |   9 +-
 src/msat-solver/CC.ml                   |  18 -
 src/msat-solver/CC.mli                  |  16 -
 src/msat-solver/Sidekick_msat_solver.ml | 547 ++++++++++++++++++++++++
 src/msat-solver/Sidekick_smt.ml         |  25 --
 src/msat-solver/Solver.ml               | 279 ------------
 src/msat-solver/Solver.mli              |  77 ----
 src/msat-solver/Solver_types.ml         | 182 --------
 src/msat-solver/Theory.ml               | 132 ------
 src/msat-solver/Theory_combine.ml       | 162 -------
 src/msat-solver/Theory_combine.mli      |  29 --
 src/smtlib/Sidekick_smtlib.ml           | 239 ++++++++++-
 src/smtlib/dune                         |   2 +-
 19 files changed, 886 insertions(+), 1003 deletions(-)
 create mode 100644 src/base-term/Sidekick_base_term.ml
 delete mode 100644 src/msat-solver/CC.ml
 delete mode 100644 src/msat-solver/CC.mli
 create mode 100644 src/msat-solver/Sidekick_msat_solver.ml
 delete mode 100644 src/msat-solver/Sidekick_smt.ml
 delete mode 100644 src/msat-solver/Solver.ml
 delete mode 100644 src/msat-solver/Solver.mli
 delete mode 100644 src/msat-solver/Solver_types.ml
 delete mode 100644 src/msat-solver/Theory.ml
 delete mode 100644 src/msat-solver/Theory_combine.ml
 delete mode 100644 src/msat-solver/Theory_combine.mli

diff --git a/src/base-term/Sidekick_base_term.ml b/src/base-term/Sidekick_base_term.ml
new file mode 100644
index 00000000..ea9150d5
--- /dev/null
+++ b/src/base-term/Sidekick_base_term.ml
@@ -0,0 +1,27 @@
+
+module ID = ID
+module Ty_card = Ty_card
+module Cst = Cst
+module Stat = Stat
+module Model = Model
+module Ast = Ast
+module Term = Term
+module Value = Value
+module Term_cell = Term_cell
+module Ty = Ty
+module Lit = Lit
+module Value = Value
+
+
+module Arg
+  : Sidekick_core.TERM_LIT
+    with type Term.t = Term.t
+     and type Lit.t = Lit.t
+     and type Fun.t = Cst.t
+     and type Ty.t = Ty.t
+= struct
+  module Term = Term
+  module Lit = Lit
+  module Fun = Cst
+  module Ty = Ty
+end
diff --git a/src/base-term/dune b/src/base-term/dune
index 2c19bc8b..463ad6c0 100644
--- a/src/base-term/dune
+++ b/src/base-term/dune
@@ -4,4 +4,4 @@
   (synopsis "Basic term definitions for the standalone SMT solver")
   (libraries containers containers.data
              sidekick.core sidekick.util zarith)
-  (flags :standard -open Sidekick_util))
+  (flags :standard -w -32 -open Sidekick_util))
diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 25178ede..8451dd23 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -245,7 +245,7 @@ module Make(A: ARG) = struct
      See "fast congruence closure and extensions", Nieuwenhis&al, page 14 *)
 
   and ev_on_merge = t -> N.t -> th_data -> N.t -> th_data -> Expl.t -> unit
-  and ev_on_new_term = t -> N.t -> term -> th_data -> th_data option
+  and ev_on_new_term = t -> N.t -> term -> th_data option
 
   let[@inline] size_ (r:repr) = r.n_size
   let[@inline] true_ cc = Lazy.force cc.true_
@@ -505,9 +505,9 @@ module Make(A: ARG) = struct
     let th_data =
       List.fold_left
         (fun data f ->
-           match f cc n t data with
+           match f cc n t with
            | None -> data
-           | Some d -> d)
+           | Some d -> A.Data.merge data d)
       A.Data.empty cc.on_new_term
     in
     n.n_th_data <- th_data;
@@ -527,7 +527,7 @@ module Make(A: ARG) = struct
       sub
     in
     let[@inline] return x = Some x in
-    match T.cc_view n.n_term with
+    match A.cc_view n.n_term with
     | Bool _ | Opaque _ -> None
     | Eq (a,b) ->
       let a = deref_sub a in
@@ -820,7 +820,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 T.cc_view t with
+    begin match A.cc_view t with
       | Eq (a,b) when sign ->
         let a = add_term cc a in
         let b = add_term cc b in
@@ -850,7 +850,8 @@ module Make(A: ARG) = struct
   let on_new_term cc f = cc.on_new_term <- f :: cc.on_new_term
 
   let create ?(stat=Stat.global)
-      ?(on_merge=[]) ?(on_new_term=[]) ?(size=`Big) (tst:term_state) : t =
+      ?(on_merge=[]) ?(on_new_term=[]) ?(size=`Big)
+      (tst:term_state) : t =
     let size = match size with `Small -> 128 | `Big -> 2048 in
     let rec cc = {
       tst;
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index d31bd365..e72d6f29 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -93,6 +93,9 @@ module type TERM_LIT = sig
     val apply_sign : t -> bool -> t
     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
 
@@ -111,7 +114,6 @@ module type TERM_LIT_PROOF = sig
   end
 end
 
-
 module type CC_ARG = sig
   include TERM_LIT_PROOF
 
@@ -120,7 +122,9 @@ module type CC_ARG = sig
 
   (** Monoid embedded in every node *)
   module Data : sig
-    include MERGE_PP
+    type t
+    val merge : t -> t -> t
+    val pp : t Fmt.printer
     val empty : t
   end
 
@@ -335,9 +339,6 @@ module type SOLVER_INTERNAL = sig
   type t
   type solver = t
 
-  (** {3 Utils} *)
-  val tst : t -> term_state
-
   (**/**)
   module Debug_ : sig
     val on_check_invariants : t -> (unit -> unit) -> unit
@@ -364,19 +365,17 @@ module type SOLVER_INTERNAL = sig
   module Key : sig
     type 'a t
 
-    type 'a ev_on_merge = solver -> CC.N.t -> 'a -> CC.N.t -> 'a -> CC.Expl.t -> unit
     type 'a data = (module MERGE_PP with type t = 'a)
 
-    val create :
-      solver ->
-      'a data ->
-      on_merge:'a ev_on_merge ->
-      'a t
+    val create : solver -> 'a data -> 'a t
     (** Create a key for storing and accessing data of type ['a].
-        Values have to be mergeable (but only if [on_merge] does not
-        raise a conflict) *)
+        Values have to be mergeable. *)
   end
 
+  (** {3 Actions available to theories} *)
+
+  val tst : t -> term_state
+
   val cc : t -> CC.t
   (** Congruence closure for this solver *)
 
@@ -410,11 +409,14 @@ module type SOLVER_INTERNAL = sig
   (** Add toplevel clause to the SAT solver. This clause will
       not be backtracked. *)
 
-  val raise_conflict : t -> Expl.t -> unit
+  val raise_conflict : t -> Expl.t -> 'a
   (** Raise a conflict with the given explanation
       it must be a theory tautology that [expl ==> absurd].
       To be used in theories. *)
 
+  val cc_find : t -> N.t -> N.t
+  (** Find representative of the node *)
+
   val cc_merge : t -> N.t -> N.t -> Expl.t -> unit
   (** Merge these two nodes in the congruence closure, given this explanation.
       It must be a theory tautology that [expl ==> n1 = n2].
@@ -424,6 +426,13 @@ module type SOLVER_INTERNAL = sig
   (** Add/retrieve congruence closure node for this term.
       To be used in theories *)
 
+  val cc_data : t -> k:'a Key.t -> N.t -> 'a option
+  (** Theory specific data for the given node *)
+
+  val cc_add_data : t -> k:'a Key.t -> N.t -> 'a -> unit
+  (** Add data for this node. This might trigger a conflict if the class
+      already contains data that is not compatible. *)
+
   val cc_merge_t : t -> term -> term -> Expl.t -> unit
   (** Merge these two terms in the congruence closure, given this explanation.
       See {!cc_merge} *)
@@ -435,6 +444,9 @@ module type SOLVER_INTERNAL = sig
     unit
   (** Callback for when two classes containing data for this key are merged *)
 
+  val on_cc_merge_all : t -> (t -> N.t -> N.t -> Expl.t -> unit) -> unit
+  (** Callback for when any two classes are merged *)
+
   val on_cc_new_term :
     t ->
     k:'a Key.t ->
@@ -444,26 +456,28 @@ module type SOLVER_INTERNAL = sig
       closure *)
 
   val on_partial_check : t -> (t -> lit Iter.t -> unit) -> unit
-  (** Called with the slice of literals newly added on the trail *)
+  (** Register callbacked to be called with the slice of literals
+      newly added on the trail.
+
+      This is called very often and should be efficient. It doesn't have
+      to be complete, only correct. It's given only the slice of
+      the trail consisting in new literals. *)
 
   val on_final_check: t -> (t -> lit Iter.t -> unit) -> unit
-  (** Final check, must be complete (i.e. must raise a conflict
-      if the set of literals is not satisfiable) *)
+  (** Register callback to be called during the final check.
 
-  (* TODO?
-  val on_mk_model : t -> (lit Iter.t -> Model.t -> Model.t) -> unit
-  (** Update the given model *)
-    *)
+      Must be complete (i.e. must raise a conflict if the set of literals is
+      not satisfiable) and can be expensive. The function
+      is given the whole trail. *)
 end
 
 (** Public view of the solver *)
 module type SOLVER = sig
-  module Internal : SOLVER_INTERNAL
-  (** Extensive view of the solver. This should mostly be used
-      by the theories *)
+  module Solver_internal : SOLVER_INTERNAL
+  (** Internal solver, available to theories.  *)
 
-  module A = Internal.A
-  type t = Internal.t
+  module A = Solver_internal.A
+  type t
   type solver = t
   type term = A.Term.t
   type ty = A.Ty.t
@@ -492,8 +506,8 @@ module type SOLVER = sig
     val name : string
     (** Name of the theory *)
 
-    val create_and_setup : solver -> t
-    (** Instantiate the theory's state for the given solver,
+    val create_and_setup : Solver_internal.t -> t
+    (** Instantiate the theory's state for the given (internal) solver,
         register callbacks, create keys, etc. *)
 
     val push_level : t -> unit
@@ -514,45 +528,13 @@ module type SOLVER = sig
 
   val mk_theory :
     name:string ->
-    create_and_setup:(t -> 'th) ->
+    create_and_setup:(Solver_internal.t -> 'th) ->
     ?push_level:('th -> unit) ->
     ?pop_levels:('th -> int -> unit) ->
     unit ->
     theory
   (** Helper to create a theory *)
 
-  (* TODO: remove?
-  let make
-    (type st)
-      ?(check_invariants=fun _ -> ())
-      ?(on_new_term=fun _ _ _ -> ())
-      ?(on_merge=fun _ _ _ _ _ -> ())
-      ?(partial_check=fun _ _ _ -> ())
-      ?(mk_model=fun _ _ m -> m)
-      ?(push_level=fun _ -> ())
-      ?(pop_levels=fun _ _ -> ())
-      ?(cc_th=fun _->[])
-      ~name
-      ~final_check
-      ~create
-      () : t =
-    let module A = struct
-      type nonrec t = st
-      let name = name
-      let create = create
-      let on_new_term = on_new_term
-      let on_merge = on_merge
-      let partial_check = partial_check
-      let final_check = final_check
-      let mk_model = mk_model
-      let check_invariants = check_invariants
-      let push_level = push_level
-      let pop_levels = pop_levels
-      let cc_th = cc_th
-    end in
-    (module A : S)
-  *)
-
   (** {3 Boolean Atoms} *)
   module Atom : sig
     type t
@@ -591,9 +573,9 @@ module type SOLVER = sig
     val pp : t CCFormat.printer
 
     (*
-  type unknown =
-    | U_timeout
-    | U_incomplete
+    type unknown =
+      | U_timeout
+      | U_incomplete
        *)
   end
 
@@ -607,6 +589,7 @@ module type SOLVER = sig
     (* TODO? ?config:Config.t -> *)
     ?store_proof:bool ->
     theories:theory list ->
+    A.Term.state ->
     unit ->
     t
   (** Create a new solver.
diff --git a/src/main/dune b/src/main/dune
index 6d74cb43..3dbe68e6 100644
--- a/src/main/dune
+++ b/src/main/dune
@@ -5,8 +5,7 @@
   (public_name sidekick)
   (package sidekick)
   (libraries containers iter result msat sidekick.core
-   sidekick.base-term sidekick.msat-solver sidekick.smtlib
-   sidekick.smt.th-ite sidekick.dimacs)
+   sidekick.base-term sidekick.msat-solver sidekick.smtlib sidekick.dimacs)
   (flags :standard -w +a-4-42-44-48-50-58-32-60@8
          -safe-string -color always -open Sidekick_util)
   (ocamlopt_flags :standard -O3 -color always
diff --git a/src/mini-cc/Mini_cc.ml b/src/mini-cc/Mini_cc.ml
index 66a000a5..0b89e069 100644
--- a/src/mini-cc/Mini_cc.ml
+++ b/src/mini-cc/Mini_cc.ml
@@ -4,7 +4,12 @@ type res =
   | Unsat
 
 module CC_view = Sidekick_core.CC_view
-module type TERM = Sidekick_core.TERM
+
+module type ARG = sig
+  include Sidekick_core.TERM
+
+  val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) CC_view.t
+end
 
 module type S = sig
   type term
@@ -23,8 +28,7 @@ module type S = sig
   val classes : t -> term Iter.t Iter.t
 end
 
-
-module Make(A: TERM) = struct
+module Make(A: ARG) = struct
   open CC_view
 
   module Fun = A.Fun
@@ -150,7 +154,7 @@ module Make(A: TERM) = struct
     self
 
   let sub_ t k : unit =
-    match T.cc_view t with
+    match A.cc_view t with
     | Bool _ | Opaque _ -> ()
     | App_fun (_, args) -> args k
     | App_ho (f, args) -> k f; args k
@@ -202,7 +206,7 @@ module Make(A: TERM) = struct
 
   let compute_sig (self:t) (n:node) : Signature.t option =
     let[@inline] return x = Some x in
-    match T.cc_view n.n_t with
+    match A.cc_view n.n_t with
     | Bool _ | Opaque _ -> None
     | Eq (a,b) ->
       let a = find_t_ self a in
@@ -293,7 +297,7 @@ module Make(A: TERM) = struct
   (* API *)
 
   let add_lit (self:t) (p:T.t) (sign:bool) : unit =
-    match T.cc_view p with
+    match A.cc_view p with
     | Eq (t1,t2) when sign ->
       let n1 = add_t self t1 in
       let n2 = add_t self t2 in
diff --git a/src/mini-cc/Mini_cc.mli b/src/mini-cc/Mini_cc.mli
index 10afc715..53cf6781 100644
--- a/src/mini-cc/Mini_cc.mli
+++ b/src/mini-cc/Mini_cc.mli
@@ -11,7 +11,12 @@ type res =
   | Unsat
 
 module CC_view = Sidekick_core.CC_view
-module type TERM = Sidekick_core.TERM
+
+module type ARG = sig
+  include Sidekick_core.TERM
+
+  val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) CC_view.t
+end
 
 module type S = sig
   type term
@@ -35,7 +40,7 @@ module type S = sig
       This should be called only if {!check} returned [Sat]. *)
 end
 
-module Make(A: TERM)
+module Make(A: ARG)
   : S with type term = A.Term.t
        and type fun_ = A.Fun.t
        and type term_state = A.Term.state
diff --git a/src/msat-solver/CC.ml b/src/msat-solver/CC.ml
deleted file mode 100644
index 10297c22..00000000
--- a/src/msat-solver/CC.ml
+++ /dev/null
@@ -1,18 +0,0 @@
-
-module Arg = struct
-  module Fun = Cst
-  module Term = Term
-  module Lit = Lit
-  module Value = Value
-  module Ty = Ty
-  module Model = Model
-  module Proof = struct
-    type t = Solver_types.proof
-    let pp = Solver_types.pp_proof
-    let default = Solver_types.Proof_default
-  end
-end
-
-(* include Sidekick_cc.Make(Arg) *)
-
-module Mini_cc = Sidekick_cc.Mini_cc.Make(Arg)
diff --git a/src/msat-solver/CC.mli b/src/msat-solver/CC.mli
deleted file mode 100644
index 4eaa4996..00000000
--- a/src/msat-solver/CC.mli
+++ /dev/null
@@ -1,16 +0,0 @@
-(*
-
-include Sidekick_cc.S
-  with type term = Term.t
-   and type model = Model.t
-   and type lit = Lit.t
-   and type fun_ = Cst.t
-   and type term_state = Term.state
-   and type proof = Solver_types.proof
-   and module Key = Sidekick_cc.Key
-
-*)
-module Mini_cc : Sidekick_cc.Mini_cc.S
-  with type term = Term.t
-   and type fun_ = Cst.t
-   and type term_state = Term.state
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
new file mode 100644
index 00000000..59f26dee
--- /dev/null
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -0,0 +1,547 @@
+
+
+(** {1 Implementation of a Solver using Msat} *)
+
+module Vec = Msat.Vec
+module Log = Msat.Log
+module IM = Util.Int_map
+
+module type ARG = sig
+  include Sidekick_core.TERM_LIT_PROOF
+  val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) Sidekick_core.CC_view.t
+end
+
+module type S = Sidekick_core.SOLVER
+
+module Make(A : ARG)
+(*   : S with type A.Term.t = A.Term.t *)
+= struct
+  module T = A.Term
+  module Lit = A.Lit
+  type lit = Lit.t
+
+  (** Custom keys for theory data.
+      This imitates the classic tricks for heterogeneous maps
+      https://blog.janestreet.com/a-universal-type/
+
+      It needs to form a commutative monoid where values are persistent so
+      they can be restored during backtracking.
+  *)
+  module CC_key = struct
+    type 'a data = (module Sidekick_core.MERGE_PP with type t = 'a)
+    module type KEY_IMPL = sig
+      include Sidekick_core.MERGE_PP
+      val id : int
+      exception Store of t
+    end
+
+    type 'a t = (module KEY_IMPL with type t = 'a)
+
+    let n_ = ref 0
+
+    let create (type d) (x:d data) : d t =
+      let (module D) = x in
+      let module K = struct
+        include D
+        let id = !n_
+        exception Store of t
+      end in
+      incr n_;
+      (module K)
+
+    let[@inline] id : type a. a t -> int = fun (module K) -> K.id
+
+    let[@inline] equal
+      : type a b. a t -> b t -> bool
+      = fun (module K1) (module K2) -> K1.id = K2.id
+
+    let pp
+      : type a. a t -> a Fmt.printer
+      = fun (module K) out x -> K.pp out x
+  end
+
+  (** Map for theory data associated with representatives, given
+      to the congruence closure. *)
+  module Key_set = struct
+    type 'a key = 'a CC_key.t
+    type k1 =
+      | K1 : {
+          k: 'a key;
+          e: exn;
+        } -> k1
+
+    type t = k1 IM.t
+
+    let empty = IM.empty
+
+    let[@inline] mem k t = IM.mem (CC_key.id k) t
+
+    let find (type a) (k : a key) (self:t) : a option =
+      let (module K) = k in
+      match IM.find K.id self with
+      | K1 {e=K.Store v;_} -> Some v
+      | _ -> None
+      | exception Not_found -> None
+
+    let add (type a) (k : a key) (v:a) (self:t) : t =
+      let (module K) = k in
+      IM.add K.id (K1 {k; e=K.Store v}) self
+      
+    let remove (type a) (k: a key) self : t =
+      let (module K) = k in
+      IM.remove K.id self
+
+    let merge (m1:t) (m2:t) : t =
+      IM.merge
+        (fun _ p1 p2 ->
+           match p1, p2 with
+           | None, None -> None
+           | Some v, None
+           | None, Some v -> Some v
+           | Some (K1 {k=(module K1) as key1; e=pair1; }), Some (K1{e=pair2;_}) ->
+             match pair1, pair2 with
+             | K1.Store v1, K1.Store v2 ->
+               let v12 = K1.merge v1 v2 in (* merge content *)
+               Some (K1 {k=key1; e=K1.Store v12; })
+             | _ -> assert false)
+        m1 m2
+
+    let pp_pair out (K1 {k=(module K);e=x; _}) =
+      match x with
+      | K.Store x -> K.pp out x
+      | _ -> assert false
+
+    let pp out (self:t) =
+      if IM.is_empty self then Fmt.string out "{}"
+      else Fmt.fprintf out "{@[%a@]}" (Util.pp_seq pp_pair) (IM.values self)
+  end
+
+  (* the full argument to the congruence closure *)
+  module A = struct
+    include A
+
+    module Data = Key_set
+    module Actions = struct
+      type t = {
+        raise_conflict : 'a. Lit.t list -> Proof.t -> 'a;
+        propagate : Lit.t -> reason:Lit.t Iter.t -> Proof.t -> unit;
+      }
+      let[@inline] raise_conflict a lits p = a.raise_conflict lits p
+      let[@inline] propagate a lit ~reason p = a.propagate lit ~reason p
+    end
+  end
+
+  module CC = Sidekick_cc.Make(A)
+  module Expl = CC.Expl
+  module N = CC.N
+
+  (** Internal solver, given to theories and to Msat *)
+  module Solver_internal = struct
+    module A = A
+
+    type th_states = 
+      | Ths_nil
+      | Ths_cons : {
+          st: 'a;
+          push_level: 'a -> unit;
+          pop_levels: 'a -> int -> unit;
+          next: th_states;
+        } -> th_states
+
+    (* actions from msat *)
+    type msat_acts = (Msat.void, Lit.t, Msat.void, A.Proof.t) Msat.acts
+
+    type t = {
+      tst: T.state; (** state for managing terms *)
+      cc: CC.t lazy_t; (** congruence closure *)
+      stat: Stat.t;
+      count_axiom: int Stat.counter;
+      count_conflict: int Stat.counter;
+      count_propagate: int Stat.counter;
+      cc_acts: CC.actions lazy_t;
+      mutable th_states : th_states; (** Set of theories *)
+      mutable msat_acts: msat_acts option;
+      mutable on_partial_check: (t -> lit Iter.t -> unit) list;
+      mutable on_final_check: (t -> lit Iter.t -> unit) list;
+      mutable on_cc_merge: on_cc_merge list IM.t;
+      mutable on_cc_new_term : on_cc_new_term IM.t;
+    }
+
+    and on_cc_merge = On_cc_merge : {
+        k: 'a CC_key.t;
+        f: t -> CC.N.t -> 'a -> CC.N.t -> 'a -> CC.Expl.t -> unit;
+      } -> on_cc_merge
+
+    and on_cc_new_term = On_cc_new_term : {
+        k: 'a CC_key.t;
+        f: t -> N.t -> T.t -> 'a option;
+      } -> on_cc_new_term
+
+    module Formula = struct
+      include Lit
+      let norm lit =
+        let lit', sign = norm_sign lit in
+        lit', if sign then Msat.Same_sign else Msat.Negated
+    end
+    module Eq_class = CC.N
+    module Expl = CC.Expl
+
+    type formula = Lit.t
+    type proof = A.Proof.t
+    type conflict = lit list
+
+    let[@inline] cc (t:t) = Lazy.force t.cc
+    let[@inline] tst t = t.tst
+
+    let[@inline] raise_conflict self c : 'a =
+      Stat.incr self.count_conflict;
+      match self.msat_acts with
+      | None -> assert false
+      | Some acts ->
+        acts.Msat.acts_raise_conflict c A.Proof.default
+
+    let[@inline] propagate self p cs : unit =
+      Stat.incr self.count_propagate;
+      match self.msat_acts with
+      | None -> assert false
+      | Some acts ->
+        acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), A.Proof.default))
+
+    let[@inline] propagate_l self p cs : unit = propagate self p (fun()->cs)
+
+    let add_axiom_ self ~keep lits : unit =
+      Stat.incr self.count_axiom;
+      match self.msat_acts with
+      | None -> assert false
+      | Some acts ->
+        acts.Msat.acts_add_clause ~keep lits A.Proof.default
+
+    let[@inline] mk_lit self ?sign t = Lit.atom self.tst ?sign t
+
+    let[@inline] add_local_axiom self lits : unit =
+      add_axiom_ self ~keep:false lits
+
+    let[@inline] add_persistent_axiom self lits : unit =
+      add_axiom_ self ~keep:true lits
+
+    let[@inline] add_lit self lit : unit =
+      match self.msat_acts with
+      | None -> assert false
+      | Some acts -> acts.Msat.acts_mk_lit lit
+
+    let add_lit_t self ?sign t = add_lit self (mk_lit self ?sign t)
+
+    (** {2 Interface with the SAT solver} *)
+
+    let rec push_lvl_ = function
+      | Ths_nil -> ()
+      | Ths_cons r -> r.push_level r.st; push_lvl_ r.next
+
+    let rec pop_lvls_ n = function
+      | Ths_nil -> ()
+      | Ths_cons r -> r.pop_levels r.st n; pop_lvls_ n r.next
+
+    let push_level (self:t) : unit =
+      CC.push_level (cc self);
+      push_lvl_ self.th_states
+
+    let pop_levels (self:t) n : unit =
+      CC.pop_levels (cc self) n;
+      pop_lvls_ n self.th_states
+
+    (* handle a literal assumed by the SAT solver *)
+    let assert_lits_ ~final (self:t) (lits:Lit.t Iter.t) : unit =
+      Msat.Log.debugf 2
+        (fun k->k "(@[<hv1>@{<green>th_combine.assume_lits@}%s@ %a@])"
+            (if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits);
+      (* transmit to CC *)
+      let cc = cc self in
+      if not final then (
+        CC.assert_lits cc lits;
+      );
+      (* transmit to theories. *)
+      CC.check cc (Lazy.force self.cc_acts);
+      if final then (
+        List.iter (fun f -> f self lits) self.on_final_check;
+      ) else (
+        List.iter (fun f -> f self lits) self.on_partial_check;
+      );
+      ()
+
+    let[@inline] iter_atoms_ acts : _ Iter.t =
+      fun f ->
+      acts.Msat.acts_iter_assumptions
+        (function
+          | Msat.Lit a -> f a
+          | Msat.Assign _ -> assert false)
+
+    (* propagation from the bool solver *)
+    let check_ ~final (self:t) (acts: msat_acts) =
+      let old_acts = self.msat_acts in
+      self.msat_acts <- Some acts;
+      try
+        let iter = iter_atoms_ acts in
+        (* TODO if Config.progress then print_progress(); *)
+        Msat.Log.debugf 5 (fun k->k "(th_combine.assume :len %d)" (Iter.length iter));
+        assert_lits_ ~final self iter;
+        self.msat_acts <- old_acts;
+        ()
+      with e ->
+        self.msat_acts <- old_acts;
+        raise e
+
+    let add_formula (self:t) (lit:Lit.t) =
+      let t = Lit.term lit in
+      let lazy cc = self.cc in
+      let n = CC.add_term cc t in
+      CC.set_as_lit cc n (Lit.abs lit);
+      ()
+
+    (* propagation from the bool solver *)
+    let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
+      check_ ~final:false self acts
+
+    (* perform final check of the model *)
+    let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit =
+      check_ ~final:true self acts
+
+    (* TODO
+    let mk_model (self:t) lits : Model.t =
+      let m =
+        Iter.fold
+          (fun m (Th_state ((module Th),st)) -> Th.mk_model st lits m)
+          Model.empty (theories self)
+      in
+      (* now complete model using CC *)
+      CC.mk_model (cc self) m
+       *)
+
+    let cc_raise_conflict self lits _p =
+      raise_conflict self lits
+
+    let cc_propagate self p ~reason _p =
+      let reason() = Iter.to_list reason in
+      propagate self p reason
+
+    let create ~stat (tst:A.Term.state) () : t =
+      let rec self = {
+        tst;
+        cc = lazy (
+          (* lazily tie the knot *)
+          CC.create ~size:`Big self.tst;
+        );
+        cc_acts=lazy {
+          raise_conflict=cc_raise_conflict self;
+          propagate=cc_propagate self;
+        };
+        th_states=Ths_nil;
+        stat;
+        count_axiom = Stat.mk_int stat "th-axioms";
+        count_propagate = Stat.mk_int stat "th-propagations";
+        count_conflict = Stat.mk_int stat "th-conflicts";
+        msat_acts=None;
+        on_partial_check=[];
+        on_final_check=[];
+        on_cc_merge=IM.empty;
+        on_cc_new_term=IM.empty;
+      } in
+      ignore (Lazy.force @@ self.cc : CC.t);
+      self
+
+  end
+
+  type conflict = lit list
+
+  (** the Main Solver *)
+  module Sat_solver = Msat.Make_cdcl_t(Solver_internal)
+
+  let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
+    Sat_solver.Clause.atoms c |> Array.map Sat_solver.Atom.formula |> IArray.of_array_unsafe
+
+  module Atom = Sat_solver.Atom
+  module Proof = Sat_solver.Proof
+
+  (* main solver state *)
+  type t = {
+    si: Solver_internal.t;
+    solver: Sat_solver.t;
+    stat: Stat.t;
+    (* config: Config.t *)
+  }
+  type solver = t
+
+  module type THEORY = sig
+    type t
+    val name : string
+    val create_and_setup : Solver_internal.t -> t
+    val push_level : t -> unit
+    val pop_levels : t -> int -> unit
+  end
+
+  type theory = (module THEORY)
+
+  (** {2 Main} *)
+
+  let add_theory (self:t) (th:theory) : unit =
+    let (module Th) = th in
+    Log.debugf 2
+      (fun k-> k "(@[th_combine.add_th@ :name %S@])" Th.name);
+    let st = Th.create_and_setup self.si in
+    (* add push/pop to the internal solver *)
+    begin
+      let open Solver_internal in
+      self.si.th_states <- Ths_cons {
+          st;
+          push_level=Th.push_level;
+          pop_levels=Th.pop_levels;
+          next=self.si.th_states;
+        };
+    end;
+    ()
+
+  let add_theory_l self = List.iter (add_theory self)
+
+  (* create a new solver *)
+  let create ?(stat=Stat.global) ?size ?store_proof ~theories tst () : t =
+    Log.debug 5 "th_combine.create";
+    let si = Solver_internal.create ~stat tst () in
+    let self = {
+      si;
+      solver=Sat_solver.create ?store_proof ?size si;
+      stat;
+    } in
+    add_theory_l self theories;
+    (* assert [true] and [not false] *)
+    begin
+      let tst = Solver_internal.tst self.si in
+      Sat_solver.assume self.solver [
+        [Lit.atom tst @@ T.bool tst true];
+      ] A.Proof.default;
+    end;
+    self
+
+  let check_invariants (self:t) =
+    if Util._CHECK_INVARIANTS then (
+      CC.Debug_.check_invariants (Solver_internal.cc self.si);
+    )
+
+  let[@inline] solver self = self.solver
+  let[@inline] cc self = Solver_internal.cc self.si
+  let stats self = self.stat
+  let[@inline] tst self = Solver_internal.tst self.si
+
+  let[@inline] mk_atom_lit self lit : Atom.t = Sat_solver.make_atom self.solver lit
+  let[@inline] mk_atom_t self ?sign t : Atom.t =
+    let lit = Lit.atom (tst self) ?sign t in
+    mk_atom_lit self lit
+
+  (** {2 Result} *)
+
+  module Unknown = struct
+    type t =
+      | U_timeout
+      | U_max_depth
+      | U_incomplete
+
+    let pp out = function
+      | U_timeout -> Fmt.string out "timeout"
+      | U_max_depth -> Fmt.string out "max depth reached"
+      | U_incomplete -> Fmt.string out "incomplete fragment"
+  end
+
+  (* TODO *)
+  module Model = struct
+    type t = unit
+    let empty = ()
+    let mem _ _ = false
+    let find _ _ = None
+    let eval _ _ = None
+    let pp out _ = Fmt.string out "<model>"
+  end
+
+  (* TODO
+  type model = A.Model.t
+  let pp_model = Model.pp
+     *)
+
+  type res = (Model.t, Proof.t, lit IArray.t, Unknown.t) Sidekick_core.solver_res
+
+  (** {2 Main} *)
+
+  (* convert unsat-core *)
+  let clauses_of_unsat_core (core:Sat_solver.clause list): Lit.t IArray.t Iter.t =
+    Iter.of_list core
+    |> Iter.map clause_of_mclause
+
+  (* print all terms reachable from watched literals *)
+  let pp_term_graph _out (_:t) =
+    ()
+
+  let pp_stats out (self:t) : unit =
+    Stat.pp_all out (Stat.all @@ stats self)
+
+  (* map boolean subterms to literals *)
+  let add_bool_subterms_ (self:t) (t:T.t) : unit =
+    Term.iter_dag t
+    |> Iter.filter (fun t -> Ty.is_prop @@ Term.ty t)
+    |> Iter.filter
+      (fun t -> match Term.view t with
+         | Term.Not _ -> false (* will process the subterm just later *)
+         | _ -> true)
+    |> Iter.iter
+      (fun sub ->
+         Log.debugf 5 (fun k->k  "(@[solver.map-to-lit@ :subterm %a@])" Term.pp sub);
+         ignore (mk_atom_t self sub : Sat_solver.atom))
+
+  let assume (self:t) (c:Lit.t IArray.t) : unit =
+    let sat = solver self in
+    IArray.iter (fun lit -> add_bool_subterms_ self @@ Lit.term lit) c;
+    let c = IArray.to_array_map (Sat_solver.make_atom sat) c in
+    Stat.incr self.count_clause;
+    Sat_solver.add_clause_a sat c Proof_default
+
+  (* TODO: remove? use a special constant + micro theory instead?
+  let[@inline] assume_distinct self l ~neq lit : unit =
+    CC.assert_distinct (cc self) l lit ~neq
+     *)
+
+  let check_model (_s:t) : unit =
+    Log.debug 1 "(smt.solver.check-model)";
+    (* TODO
+    Sat_solver.check_model s.solver
+    *)
+    ()
+
+  (* TODO: main loop with iterative deepening of the unrolling  limit
+     (not the value depth limit) *)
+  let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
+    let do_on_exit () =
+      List.iter (fun f->f()) on_exit;
+    in
+    let r = Sat_solver.solve ~assumptions (solver self) in
+    Stat.incr self.count_solve;
+    match r with
+    | Sat_solver.Sat st ->
+      Log.debugf 1 (fun k->k "SAT");
+      let lits f = st.iter_trail f (fun _ -> ()) in
+      let m = Theory_combine.mk_model (th_combine self) lits in
+      do_on_exit ();
+      Sat m
+      (*
+      let env = Ast.env_empty in
+      let m = Model.make ~env in
+         …
+      Unknown U_incomplete (* TODO *)
+      *)
+    | Sat_solver.Unsat us ->
+      let pr =
+        try
+          let pr = us.get_proof () in
+          if check then Sat_solver.Proof.check pr;
+          Some pr
+        with Msat.Solver_intf.No_proof -> None
+      in
+      do_on_exit ();
+      Unsat pr
+
+end
diff --git a/src/msat-solver/Sidekick_smt.ml b/src/msat-solver/Sidekick_smt.ml
deleted file mode 100644
index cdd6cc37..00000000
--- a/src/msat-solver/Sidekick_smt.ml
+++ /dev/null
@@ -1,25 +0,0 @@
-
-module ID = ID
-module Ty_card = Ty_card
-module Cst = Cst
-module Stat = Stat
-module Model = Model
-module Ast = Ast
-module Term = Term
-module Value = Value
-module Term_cell = Term_cell
-module Ty = Ty
-module Lit = Lit
-module Theory_combine = Theory_combine
-module Theory = Theory
-module Solver = Solver
-module CC = CC
-
-module Solver_types = Solver_types
-
-type theory = Theory.t
-
-(**/**)
-module Vec = Msat.Vec
-module Log = Msat.Log
-(**/**)
diff --git a/src/msat-solver/Solver.ml b/src/msat-solver/Solver.ml
deleted file mode 100644
index 76b5dad0..00000000
--- a/src/msat-solver/Solver.ml
+++ /dev/null
@@ -1,279 +0,0 @@
-
-(* This file is free software. See file "license" for more details. *)
-
-(** {1 Main Solver} *)
-
-[@@@warning "-32"]
-
-open Solver_types
-
-let get_time : unit -> float = Sys.time
-
-(** {2 The Main Solver} *)
-
-module Sat_solver = Msat.Make_cdcl_t(Theory_combine)
-
-let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
-  Sat_solver.Clause.atoms c |> Array.map Sat_solver.Atom.formula |> IArray.of_array_unsafe
-
-module Atom = Sat_solver.Atom
-module Proof = Sat_solver.Proof
-
-(* main solver state *)
-type t = {
-  solver: Sat_solver.t;
-  stat: Stat.t;
-  count_clause: int Stat.counter;
-  count_solve: int Stat.counter;
-  config: Config.t
-}
-
-let[@inline] solver self = self.solver
-let[@inline] th_combine (self:t) : Theory_combine.t = Sat_solver.theory self.solver
-let[@inline] add_theory self th = Theory_combine.add_theory (th_combine self) th
-let[@inline] cc self = Theory_combine.cc (th_combine self)
-let stats self = self.stat
-let[@inline] tst self = Theory_combine.tst (th_combine self)
-
-let[@inline] mk_atom_lit self lit : Atom.t = Sat_solver.make_atom self.solver lit
-let[@inline] mk_atom_t self ?sign t : Atom.t =
-  let lit = Lit.atom (tst self) ?sign t in
-  mk_atom_lit self lit
-
-let create ?(stat=Stat.global) ?size ?(config=Config.empty) ?store_proof ~theories () : t =
-  let th_combine = Theory_combine.create ~stat () in
-  let self = {
-    solver=Sat_solver.create ?store_proof ?size th_combine;
-    stat;
-    count_clause=Stat.mk_int stat "input-clauses";
-    count_solve=Stat.mk_int stat "solve";
-    config;
-  } in
-  (* now add the theories *)
-  Theory_combine.add_theory_l th_combine theories;
-  (* assert [true] and [not false] *)
-  let tst = tst self in
-  Sat_solver.assume self.solver [
-    [Lit.atom tst @@ Term.true_ tst];
-  ] Proof_default;
-  self
-
-(** {2 Toplevel Goals}
-
-    List of toplevel goals to satisfy. Mainly used for checking purpose
-*)
-
-module Top_goals: sig
-  val push : term -> unit
-  val to_seq : term Iter.t
-  val check: unit -> unit
-end = struct
-  (* list of terms to fully evaluate *)
-  let toplevel_goals_ : term list ref = ref []
-
-  (* add [t] to the set of terms that must be evaluated *)
-  let push (t:term): unit =
-    toplevel_goals_ := t :: !toplevel_goals_;
-    ()
-
-  let to_seq k = List.iter k !toplevel_goals_
-
-  (* FIXME
-  (* check that this term fully evaluates to [true] *)
-  let is_true_ (t:term): bool = match CC.normal_form t with
-    | None -> false
-    | Some (NF_bool b) -> b
-    | Some (NF_cstor _) -> assert false (* not a bool *)
-
-  let check () =
-    if not (List.for_all is_true_ !toplevel_goals_)
-    then (
-      if Config.progress then flush_progress();
-      Log.debugf 1
-        (fun k->
-           let pp_lit out t =
-             let nf = CC.normal_form t in
-             Format.fprintf out "(@[term: %a@ nf: %a@])"
-               Term.pp t (Fmt.opt pp_term_nf) nf
-           in
-           k "(@[<hv1>Top_goals.check@ (@[<v>%a@])@])"
-             (Util.pp_list pp_lit) !toplevel_goals_);
-      assert false;
-    )
-  *)
-
-  let check () : unit = ()
-end
-
-(** {2 Conversion} *)
-
-(* list of constants we are interested in *)
-let model_support_ : Cst.t list ref = ref []
-
-let model_env_ : Ast.env ref = ref Ast.env_empty
-
-let add_cst_support_ (c:cst): unit =
-  CCList.Ref.push model_support_ c
-
-let add_ty_support_ (_ty:Ty.t): unit = ()
-
-(** {2 Result} *)
-
-type unknown =
-  | U_timeout
-  | U_max_depth
-  | U_incomplete
-
-let pp_unknown out = function
-  | U_timeout -> Fmt.string out "timeout"
-  | U_max_depth -> Fmt.string out "max depth reached"
-  | U_incomplete -> Fmt.string out "incomplete fragment"
-
-type model = Model.t
-let pp_model = Model.pp
-
-type res =
-  | Sat of model
-  | Unsat of Proof.t option
-  | Unknown of unknown
-
-(** {2 Main} *)
-
-(* convert unsat-core *)
-let clauses_of_unsat_core (core:Sat_solver.clause list): Lit.t IArray.t Iter.t =
-  Iter.of_list core
-  |> Iter.map clause_of_mclause
-
-(* print all terms reachable from watched literals *)
-let pp_term_graph _out (_:t) =
-  ()
-
-let pp_stats out (self:t) : unit =
-  Stat.pp_all out (Stat.all @@ stats self)
-
-let do_on_exit ~on_exit =
-  List.iter (fun f->f()) on_exit;
-  ()
-
-(* map boolean subterms to literals *)
-let add_bool_subterms_ (self:t) (t:Term.t) : unit =
-  Term.iter_dag t
-  |> Iter.filter (fun t -> Ty.is_prop @@ Term.ty t)
-  |> Iter.filter
-    (fun t -> match Term.view t with
-       | Term.Not _ -> false (* will process the subterm just later *)
-       | _ -> true)
-  |> Iter.iter
-    (fun sub ->
-       Log.debugf 5 (fun k->k  "(@[solver.map-to-lit@ :subterm %a@])" Term.pp sub);
-       ignore (mk_atom_t self sub : Sat_solver.atom))
-
-let assume (self:t) (c:Lit.t IArray.t) : unit =
-  let sat = solver self in
-  IArray.iter (fun lit -> add_bool_subterms_ self @@ Lit.term lit) c;
-  let c = IArray.to_array_map (Sat_solver.make_atom sat) c in
-  Stat.incr self.count_clause;
-  Sat_solver.add_clause_a sat c Proof_default
-
-(* TODO: remove? use a special constant + micro theory instead?
-let[@inline] assume_distinct self l ~neq lit : unit =
-  CC.assert_distinct (cc self) l lit ~neq
-   *)
-
-let check_model (_s:t) : unit =
-  Log.debug 1 "(smt.solver.check-model)";
-  (* TODO
-  Sat_solver.check_model s.solver
-  *)
-  ()
-
-(* TODO: main loop with iterative deepening of the unrolling  limit
-   (not the value depth limit) *)
-let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
-  let r = Sat_solver.solve ~assumptions (solver self) in
-  Stat.incr self.count_solve;
-  match r with
-  | Sat_solver.Sat st ->
-    Log.debugf 1 (fun k->k "SAT");
-    let lits f = st.iter_trail f (fun _ -> ()) in
-    let m = Theory_combine.mk_model (th_combine self) lits in
-    do_on_exit ~on_exit;
-    Sat m
-    (*
-    let env = Ast.env_empty in
-    let m = Model.make ~env in
-       …
-    Unknown U_incomplete (* TODO *)
-    *)
-  | Sat_solver.Unsat us ->
-    let pr =
-      try
-        let pr = us.get_proof () in
-        if check then Sat_solver.Proof.check pr;
-        Some pr
-      with Msat.Solver_intf.No_proof -> None
-    in
-    do_on_exit ~on_exit;
-    Unsat pr
-
-(* FIXME:
-(* TODO: max_depth should actually correspond to the maximum depth
-   of un-expanded terms (expand in body of t --> depth = depth(t)+1),
-   so it corresponds to unfolding call graph to some depth *)
-
-let solve ?(on_exit=[]) ?(check=true) () =
-  let n_iter = ref 0 in
-  let rec check_cc (): res =
-    assert (Backtrack.at_level_0 ());
-    if !n_iter > Config.max_depth then Unknown U_max_depth (* exceeded limit *)
-    else begin match CC.check () with
-      | CC.Unsat _ -> Unsat (* TODO proof *)
-      | CC.Sat lemmas  ->
-        add_cc_lemmas lemmas;
-        check_solver()
-    end
-
-  and check_solver (): res =
-    (* assume all literals [expanded t] are false *)
-    let assumptions =
-      Terms_to_expand.to_seq
-      |> Iter.map (fun {Terms_to_expand.lit; _} -> Lit.neg lit)
-      |> Iter.to_rev_list
-    in
-    incr n_iter;
-    Log.debugf 2
-      (fun k->k
-          "(@[<1>@{<Yellow>solve@}@ @[:with-assumptions@ (@[%a@])@ n_iter: %d]@])"
-          (Util.pp_list Lit.pp) assumptions !n_iter);
-    begin match M.solve ~assumptions() with
-      | M.Sat _ ->
-        Log.debugf 1 (fun k->k "@{<Yellow>** found SAT@}");
-        do_on_exit ~on_exit;
-        let m = Model_build.make () in
-        if check then Model_build.check m;
-        Sat m
-      | M.Unsat us ->
-        let p = us.SI.get_proof () in
-        Log.debugf 4 (fun k->k "proof: @[%a@]@." pp_proof p);
-        let core = p |> M.unsat_core in
-        (* check if unsat because of assumptions *)
-        expand_next core
-    end
-
-  (* pick a term to expand, or UNSAT *)
-  and expand_next (core:unsat_core) =
-    begin match find_to_expand core with
-      | None -> Unsat (* TODO proof *)
-      | Some to_expand ->
-        let t = to_expand.Terms_to_expand.term in
-        Log.debugf 2 (fun k->k "(@[<1>@{<green>expand_next@}@ :term %a@])" Term.pp t);
-        CC.expand_term t;
-        Terms_to_expand.remove t;
-        Clause.push_new (Clause.make [to_expand.Terms_to_expand.lit]);
-        Backtrack.backtrack_to_level_0 ();
-        check_cc () (* recurse *)
-    end
-  in
-  check_cc()
-
-   *)
diff --git a/src/msat-solver/Solver.mli b/src/msat-solver/Solver.mli
deleted file mode 100644
index fea5cdd5..00000000
--- a/src/msat-solver/Solver.mli
+++ /dev/null
@@ -1,77 +0,0 @@
-
-(* This file is free software. See file "license" for more details. *)
-
-(** {1 Solver}
-
-    The solving algorithm, based on MCSat *)
-
-module Sat_solver : Msat.S
-      with type Formula.t = Lit.t
-       and type theory = Theory_combine.t
-       and type lemma = Theory_combine.proof
-
-(** {2 Result} *)
-
-type model = Model.t
-
-module Atom = Sat_solver.Atom
-
-module Proof : sig
-  type t = Sat_solver.Proof.t
-  val check : t -> unit
-end
-
-type unknown =
-  | U_timeout
-  | U_max_depth
-  | U_incomplete
-
-type res =
-  | Sat of Model.t
-  | Unsat of Proof.t option
-  | Unknown of unknown
-
-(** {2 Main} *)
-
-type t
-(** Solver state *)
-
-val create :
-  ?stat:Stat.t ->
-  ?size:[`Big | `Tiny | `Small] ->
-  ?config:Config.t ->
-  ?store_proof:bool ->
-  theories:Theory.t list ->
-  unit -> t
-
-val solver : t -> Sat_solver.t
-val th_combine : t -> Theory_combine.t
-val add_theory : t -> Theory.t -> unit
-val cc : t -> CC.t
-val stats : t -> Stat.t
-val tst : t -> Term.state
-
-val mk_atom_lit : t -> Lit.t -> Atom.t
-val mk_atom_t : t -> ?sign:bool -> Term.t -> Atom.t
-
-val assume : t -> Lit.t IArray.t -> unit
-
-(* TODO: use the theory instead
-val assume_distinct : t -> Term.t list -> neq:Term.t -> Lit.t -> unit
-   *)
-
-val solve :
-  ?on_exit:(unit -> unit) list ->
-  ?check:bool ->
-  assumptions:Atom.t list ->
-  t ->
-  res
-(** [solve s] checks the satisfiability of the statement added so far to [s]
-    @param check if true, the model is checked before returning
-    @param on_exit functions to be run before this returns *)
-
-val check_model : t -> unit
-
-val pp_term_graph: t CCFormat.printer
-val pp_stats : t CCFormat.printer
-val pp_unknown : unknown CCFormat.printer
diff --git a/src/msat-solver/Solver_types.ml b/src/msat-solver/Solver_types.ml
deleted file mode 100644
index 3c95c320..00000000
--- a/src/msat-solver/Solver_types.ml
+++ /dev/null
@@ -1,182 +0,0 @@
-
-module Vec = Msat.Vec
-module Log = Msat.Log
-
-module Fmt = CCFormat
-
-(* main term cell. *)
-type term = {
-  mutable term_id: int; (* unique ID *)
-  mutable term_ty: ty;
-  term_view : term term_view;
-}
-
-(* term shallow structure *)
-and 'a term_view =
-  | Bool of bool
-  | App_cst of cst * 'a IArray.t (* full, first-order application *)
-  | Eq of 'a * 'a
-  | If of 'a * 'a * 'a
-  | Not of 'a
-
-(* boolean literal *)
-and lit = {
-  lit_term: term;
-  lit_sign: bool;
-}
-
-and cst = {
-  cst_id: ID.t;
-  cst_view: cst_view;
-}
-
-and cst_view =
-  | Cst_undef of fun_ty (* simple undefined constant *)
-  | Cst_def of {
-      pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
-      abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *)
-      do_cc: bool; (* participate in congruence closure? *)
-      relevant : 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *)
-      ty : ID.t -> term IArray.t -> ty; (* compute type *)
-      eval: value IArray.t -> value; (* evaluate term *)
-    }
-(** Methods on the custom term view whose arguments are ['a].
-    Terms must be printable, and provide some additional theory handles.
-
-    - [relevant] must return a subset of [args] (possibly the same set).
-      The terms it returns will be activated and evaluated whenever possible.
-      Terms in [args \ relevant args] are considered for
-      congruence but not for evaluation.
-*)
-
-(** Function type *)
-and fun_ty = {
-  fun_ty_args: ty list;
-  fun_ty_ret: ty;
-}
-
-(** Hashconsed type *)
-and ty = {
-  mutable ty_id: int;
-  ty_view: ty_view;
-}
-
-and ty_view =
-  | Ty_prop
-  | Ty_atomic of {
-      def: ty_def;
-      args: ty list;
-      card: ty_card lazy_t;
-    }
-
-and ty_def =
-  | Ty_uninterpreted of ID.t
-  | Ty_def of {
-      id: ID.t;
-      pp: ty Fmt.printer -> ty list Fmt.printer;
-      default_val: value list -> value; (* default value of this type *)
-      card: ty list -> ty_card;
-    }
-
-and ty_card =
-  | Finite
-  | Infinite
-
-(** Semantic values, used for models (and possibly model-constructing calculi) *)
-and value =
-  | V_bool of bool
-  | V_element of {
-      id: ID.t;
-      ty: ty;
-    } (** a named constant, distinct from any other constant *)
-  | V_custom of {
-      view: value_custom_view;
-      pp: value_custom_view Fmt.printer;
-      eq: value_custom_view -> value_custom_view -> bool;
-      hash: value_custom_view -> int;
-    } (** Custom value *)
-
-and value_custom_view = ..
-
-type proof = Proof_default
-
-type sat_actions = (Msat.void, lit, Msat.void, proof) Msat.acts
-
-let[@inline] term_equal_ (a:term) b = a==b
-let[@inline] term_hash_ a = a.term_id
-let[@inline] term_cmp_ a b = CCInt.compare a.term_id b.term_id
-
-let cmp_lit a b =
-  let c = CCBool.compare a.lit_sign b.lit_sign in
-  if c<>0 then c
-  else term_cmp_ a.lit_term b.lit_term
-
-let cst_compare a b = ID.compare a.cst_id b.cst_id
-
-let hash_lit a =
-  let sign = a.lit_sign in
-  Hash.combine3 2 (Hash.bool sign) (term_hash_ a.lit_term)
-
-let pp_cst out a = ID.pp out a.cst_id
-let id_of_cst a = a.cst_id
-
-let[@inline] eq_ty a b = a.ty_id = b.ty_id
-
-let eq_value a b = match a, b with
-  | V_bool a, V_bool b -> a=b
-  | V_element e1, V_element e2 ->
-    ID.equal e1.id e2.id && eq_ty e1.ty e2.ty
-  | V_custom x1, V_custom x2 ->
-    x1.eq x1.view x2.view
-  | V_bool _, _ | V_element _, _ | V_custom _, _
-    -> false
-
-let hash_value a = match a with
-  | V_bool a -> Hash.bool a
-  | V_element e -> ID.hash e.id
-  | V_custom x -> x.hash x.view
-
-let pp_value out = function
-  | V_bool b -> Fmt.bool out b
-  | V_element e -> ID.pp out e.id
-  | V_custom c -> c.pp out c.view
-
-let pp_db out (i,_) = Format.fprintf out "%%%d" i
-
-let rec pp_ty out t = match t.ty_view with
-  | Ty_prop -> Fmt.string out "prop"
-  | Ty_atomic {def=Ty_uninterpreted id; args=[]; _} -> ID.pp out id
-  | Ty_atomic {def=Ty_uninterpreted id; args; _} ->
-    Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp_ty) args
-  | Ty_atomic {def=Ty_def def; args; _} -> def.pp pp_ty out args
-
-let pp_term_view_gen ~pp_id ~pp_t out = function
-  | Bool true -> Fmt.string out "true"
-  | Bool false -> Fmt.string out "false"
-  | App_cst ({cst_view=Cst_def {pp=Some pp_custom;_};_},l) -> pp_custom pp_t out l
-  | App_cst (c, a) when IArray.is_empty a ->
-    pp_id out (id_of_cst c)
-  | App_cst (f,l) ->
-    Fmt.fprintf out "(@[<1>%a@ %a@])" pp_id (id_of_cst f) (Util.pp_iarray pp_t) l
-  | Eq (a,b) -> Fmt.fprintf out "(@[<hv>=@ %a@ %a@])" pp_t a pp_t b
-  | If (a, b, c) ->
-    Fmt.fprintf out "(@[if %a@ %a@ %a@])" pp_t a pp_t b pp_t c
-  | Not u -> Fmt.fprintf out "(@[not@ %a@])" pp_t u
-
-let pp_term_top ~ids out t =
-  let rec pp out t =
-    pp_rec out t;
-    (* FIXME if Config.pp_hashcons then Format.fprintf out "/%d" t.term_id; *)
-  and pp_rec out t = pp_term_view_gen ~pp_id ~pp_t:pp_rec out t.term_view
-  and pp_id = if ids then ID.pp else ID.pp_name in
-  pp out t
-
-let pp_term = pp_term_top ~ids:false
-let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term
-
-let pp_lit out l =
-  if l.lit_sign then pp_term out l.lit_term
-  else Format.fprintf out "(@[@<1>¬@ %a@])" pp_term l.lit_term
-
-let pp_proof out = function
-  | Proof_default -> Fmt.fprintf out "<default proof>"
diff --git a/src/msat-solver/Theory.ml b/src/msat-solver/Theory.ml
deleted file mode 100644
index 772e75a4..00000000
--- a/src/msat-solver/Theory.ml
+++ /dev/null
@@ -1,132 +0,0 @@
-
-(** {1 All the context for a theory} *)
-module type ENV = sig
-  include Sidekick_cc.TERM_LIT
-  module CC : Sidekick_cc.S
-                
-  (* TODO: useful?
-  module Th_clause : sig
-    type t = Lit.t IArray.t
-    val pp : t CCFormat.printer
-  end
-     = struct
-    type t = Lit.t IArray.t
-
-    let pp out c =
-      if IArray.length c = 0 then CCFormat.string out "false"
-      else if IArray.length c = 1 then Lit.pp out (IArray.get c 0)
-      else (
-        Format.fprintf out "[@[<hv>%a@]]"
-          (Util.pp_iarray ~sep:" ∨ " Lit.pp) c
-      )
-  end
-  *)
-
-  (** Unsatisfiable conjunction.
-      Its negation will become a conflict clause *)
-  type conflict = Lit.t list
-
-  (** {3 Actions available to some of the theory's callbacks} *)
-  module type ACTIONS = sig
-    val cc : CC.t
-
-    val raise_conflict: conflict -> 'a
-    (** Give a conflict clause to the solver *)
-
-    val propagate: Lit.t -> (unit -> Lit.t list) -> unit
-    (** Propagate a boolean using a unit clause.
-        [expl => lit] must be a theory lemma, that is, a T-tautology *)
-
-    val propagate_l: Lit.t -> Lit.t list -> unit
-    (** Propagate a boolean using a unit clause.
-        [expl => lit] must be a theory lemma, that is, a T-tautology *)
-
-    val add_lit : Lit.t -> unit
-    (** Add the given literal to the SAT solver, so it gets assigned
-        a boolean value *)
-
-    val add_local_axiom: Lit.t list -> unit
-    (** Add local clause to the SAT solver. This clause will be
-        removed when the solver backtracks. *)
-
-    val add_persistent_axiom: Lit.t list -> unit
-    (** Add toplevel clause to the SAT solver. This clause will
-        not be backtracked. *)
-  end
-
-  type actions = (module ACTIONS)
-
-  (** {3 Context given to a theory} *)
-  module Ctx : sig
-    type t
-
-    val cc : t -> CC.t
-
-    val on_partial_check : t -> (actions -> Lit.t Iter.t -> unit) -> unit
-    (** Called when a literal becomes true *)
-
-    val on_final_check: t -> (actions -> Lit.t Iter.t -> unit) -> unit
-    (** Final check, must be complete (i.e. must raise a conflict
-        if the set of literals is not satisfiable) *)
-
-    val on_mk_model : t -> (Lit.t Iter.t -> Model.t -> Model.t) -> unit
-    (** Update the given model *)
-
-    (**/**)
-    val on_check_invariants : t -> (unit -> unit) -> unit
-    (**/**)
-  end
-
-  (** {3 A theory's state} *)
-  module type THEORY = sig
-    type t
-
-    val name : string
-    (** Name of the theory *)
-
-    val create : Term.state -> t
-    (** Instantiate the theory's state *)
-
-    val setup : t -> Ctx.t -> unit
-    (** Setup the theory with the given context, including a
-        congruence closure *)
-
-    val push_level : t -> unit
-
-    val pop_levels : t -> int -> unit
-  end
-
-  type theory = (module THEORY)
-
-  (* TODO: remove?
-  let make
-    (type st)
-      ?(check_invariants=fun _ -> ())
-      ?(on_new_term=fun _ _ _ -> ())
-      ?(on_merge=fun _ _ _ _ _ -> ())
-      ?(partial_check=fun _ _ _ -> ())
-      ?(mk_model=fun _ _ m -> m)
-      ?(push_level=fun _ -> ())
-      ?(pop_levels=fun _ _ -> ())
-      ?(cc_th=fun _->[])
-      ~name
-      ~final_check
-      ~create
-      () : t =
-    let module A = struct
-      type nonrec t = st
-      let name = name
-      let create = create
-      let on_new_term = on_new_term
-      let on_merge = on_merge
-      let partial_check = partial_check
-      let final_check = final_check
-      let mk_model = mk_model
-      let check_invariants = check_invariants
-      let push_level = push_level
-      let pop_levels = pop_levels
-      let cc_th = cc_th
-    end in
-    (module A : S)
-  *)
-end
diff --git a/src/msat-solver/Theory_combine.ml b/src/msat-solver/Theory_combine.ml
deleted file mode 100644
index a7e741a8..00000000
--- a/src/msat-solver/Theory_combine.ml
+++ /dev/null
@@ -1,162 +0,0 @@
-
-(** {1 Main theory} *)
-
-(** Combine the congruence closure with a number of plugins *)
-
-open Solver_types
-
-module Proof = struct
-  type t = Solver_types.proof
-  let default = Proof_default
-end
-
-module Formula = Lit
-module Eq_class = CC.N
-module Expl = CC.Expl
-
-type formula = Lit.t
-type proof = Proof.t
-type conflict = Theory.conflict
-
-type theory_state =
-  | Th_state : ('a Theory.t1 * 'a) -> theory_state
-
-(* TODO: first-class module instead *)
-type t = {
-  tst: Term.state; (** state for managing terms *)
-  cc: CC.t lazy_t; (** congruence closure *)
-  stat: Stat.t;
-  count_axiom: int Stat.counter;
-  count_conflict: int Stat.counter;
-  count_propagate: int Stat.counter;
-  mutable theories : theory_state list; (** Set of theories *)
-}
-
-let[@inline] cc (t:t) = Lazy.force t.cc
-let[@inline] tst t = t.tst
-let[@inline] theories (self:t) : theory_state Iter.t =
-  fun k -> List.iter k self.theories
-
-(** {2 Interface with the SAT solver} *)
-
-(* handle a literal assumed by the SAT solver *)
-let assert_lits_ ~final (self:t) acts (lits:Lit.t Iter.t) : unit =
-  Msat.Log.debugf 2
-    (fun k->k "(@[<hv1>@{<green>th_combine.assume_lits@}%s@ %a@])"
-        (if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits);
-  (* transmit to CC *)
-  let cc = cc self in
-  if not final then (
-    CC.assert_lits cc lits;
-  );
-  (* transmit to theories. *)
-  CC.check cc acts;
-  let module A = struct
-    let cc = cc
-    let[@inline] raise_conflict c : 'a =
-      Stat.incr self.count_conflict;
-      acts.Msat.acts_raise_conflict c Proof_default
-    let[@inline] propagate p cs : unit =
-      Stat.incr self.count_propagate;
-      acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), Proof_default))
-    let[@inline] propagate_l p cs : unit = propagate p (fun()->cs)
-    let[@inline] add_local_axiom lits : unit =
-      Stat.incr self.count_axiom;
-      acts.Msat.acts_add_clause ~keep:false lits Proof_default
-    let[@inline] add_persistent_axiom lits : unit =
-      Stat.incr self.count_axiom;
-      acts.Msat.acts_add_clause ~keep:true lits Proof_default
-    let[@inline] add_lit lit : unit = acts.Msat.acts_mk_lit lit
-  end in
-  let acts = (module A : Theory.ACTIONS) in
-  theories self
-    (fun (Th_state ((module Th),st)) ->
-       (* give new merges, then call {final,partial}-check *)
-       if final then Th.final_check st acts lits else Th.partial_check st acts lits);
-  ()
-
-let[@inline] iter_atoms_ acts : _ Iter.t =
-  fun f ->
-    acts.Msat.acts_iter_assumptions
-      (function
-        | Msat.Lit a -> f a
-        | Msat.Assign _ -> assert false)
-
-(* propagation from the bool solver *)
-let check_ ~final (self:t) (acts:_ Msat.acts) =
-  let iter = iter_atoms_ acts in
-  (* TODO if Config.progress then print_progress(); *)
-  Msat.Log.debugf 5 (fun k->k "(th_combine.assume :len %d)" (Iter.length iter));
-  assert_lits_ ~final self acts iter
-
-let add_formula (self:t) (lit:Lit.t) =
-  let t = Lit.term lit in
-  let lazy cc = self.cc in
-  let n = CC.add_term cc t in
-  CC.set_as_lit cc n (Lit.abs lit);
-  ()
-
-(* propagation from the bool solver *)
-let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
-  check_ ~final:false self acts
-
-(* perform final check of the model *)
-let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit =
-  check_ ~final:true self acts
-
-let push_level (self:t) : unit =
-  CC.push_level (cc self);
-  theories self (fun (Th_state ((module Th), st)) -> Th.push_level st)
-
-let pop_levels (self:t) n : unit =
-  CC.pop_levels (cc self) n;
-  theories self (fun (Th_state ((module Th), st)) -> Th.pop_levels st n)
-
-let mk_model (self:t) lits : Model.t =
-  let m =
-    Iter.fold
-      (fun m (Th_state ((module Th),st)) -> Th.mk_model st lits m)
-      Model.empty (theories self)
-  in
-  (* now complete model using CC *)
-  CC.mk_model (cc self) m
-
-(** {2 Interface to Congruence Closure} *)
-
-(** {2 Main} *)
-
-(* create a new theory combination *)
-let create ?(stat=Stat.global) () : t =
-  Log.debug 5 "th_combine.create";
-  let rec self = {
-    tst=Term.create ~size:1024 ();
-    cc = lazy (
-      (* lazily tie the knot *)
-      (* TODO: pass theories *)
-      CC.create ~size:`Big self.tst;
-    );
-    theories = [];
-    stat;
-    count_axiom = Stat.mk_int stat "th-axioms";
-    count_propagate = Stat.mk_int stat "th-propagations";
-    count_conflict = Stat.mk_int stat "th-conflicts";
-  } in
-  ignore (Lazy.force @@ self.cc : CC.t);
-  self
-
-let check_invariants (self:t) =
-  if Util._CHECK_INVARIANTS then (
-    CC.check_invariants (cc self);
-  )
-
-let add_theory (self:t) (th:Theory.t) : unit =
-let (module Th) = th in
-  Log.debugf 2
-    (fun k-> k "(@[th_combine.add_th@ :name %S@])" Th.name);
-  let st = Th.create self.tst in
-  (* add micro theories *)
-  List.iter (CC.add_th (cc self)) (Th.cc_th st);
-  (* re-pack as a [Theory.t1] *)
-  self.theories <- (Th_state ((module Th),st)) :: self.theories
-
-let add_theory_l self = List.iter (add_theory self)
diff --git a/src/msat-solver/Theory_combine.mli b/src/msat-solver/Theory_combine.mli
deleted file mode 100644
index f470a3ce..00000000
--- a/src/msat-solver/Theory_combine.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-
-(** {1 Main theory} *)
-
-(** Combine the congruence closure with a number of plugins *)
-
-module Proof : sig
-  type t = Solver_types.proof (* dummy proofs, for now *)
-end
-
-include Msat.Solver_intf.PLUGIN_CDCL_T
-  with module Formula = Lit
-   and type proof = Proof.t
-
-val create : ?stat:Stat.t -> unit -> t
-
-val cc : t -> CC.t
-val tst : t -> Term.state
-
-type theory_state =
-  | Th_state : ('a Theory.t1 * 'a) -> theory_state
-
-val theories : t -> theory_state Iter.t
-
-val mk_model : t -> Lit.t Iter.t -> Model.t
-
-val add_theory : t -> Theory.t -> unit
-(** How to add new theories *)
-
-val add_theory_l : t -> Theory.t list -> unit
diff --git a/src/smtlib/Sidekick_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml
index 4ce7e17e..4baacebf 100644
--- a/src/smtlib/Sidekick_smtlib.ml
+++ b/src/smtlib/Sidekick_smtlib.ml
@@ -2,11 +2,16 @@
 (** {1 Process Statements} *)
 
 module Fmt = CCFormat
-module Ast = Sidekick_smt.Ast
+module Ast = Sidekick_base_term.Ast
 module E = CCResult
 module Loc = Locations
 module Process = Process
 
+module Proof = struct
+  type t = Proof_default
+  let default = Proof_default
+end
+
 type 'a or_error = ('a, string) CCResult.t
 
 module Parse = struct
@@ -45,5 +50,237 @@ module Parse = struct
     with e -> Result.Error (Printexc.to_string e)
 end
 
+module Term_bool : sig
+  open Sidekick_th_bool
+  type 'a view = 'a Bool_intf.view
+
+  type term = Sidekick_smt.Term.t
+
+  include Bool_intf.BOOL_TERM
+    with type t = term
+     and type state = Sidekick_smt.Term.state
+
+  val and_ : state -> term -> term -> term
+  val or_ : state -> term -> term -> term
+  val not_ : state -> term -> term
+  val imply : state -> term -> term -> term
+  val imply_a : state -> term IArray.t -> term -> term
+  val imply_l : state -> term list -> term -> term
+  val eq : state -> term -> term -> term
+  val neq : state -> term -> term -> term
+  val and_a : state -> term IArray.t -> term
+  val and_l : state -> term list -> term
+  val or_a : state -> term IArray.t -> term
+  val or_l : state -> term list -> term
+end = struct
+  module ID = Sidekick_smt.ID
+  module T = Sidekick_smt.Term
+  module Ty = Sidekick_smt.Ty
+  open Sidekick_smt.Solver_types
+
+  open Bool_intf
+
+  type term = T.t
+  type t = T.t
+  type state = T.state
+
+  type 'a view = 'a Bool_intf.view
+
+  exception Not_a_th_term
+
+  let id_and = ID.make "and"
+  let id_or = ID.make "or"
+  let id_imply = ID.make "=>"
+
+  let equal = T.equal
+  let hash = T.hash
+
+  let view_id cst_id args =
+    if ID.equal cst_id id_and then (
+      B_and args
+    ) else if ID.equal cst_id id_or then (
+      B_or args
+    ) else if ID.equal cst_id id_imply && IArray.length args >= 2 then (
+      (* conclusion is stored first *)
+      let len = IArray.length args in
+      B_imply (IArray.sub args 1 (len-1), IArray.get args 0)
+    ) else (
+      raise_notrace Not_a_th_term
+    )
+
+  let view_as_bool (t:T.t) : T.t view =
+    match T.view t with
+    | Not u -> B_not u
+    | App_cst ({cst_id; _}, args) ->
+      (try view_id cst_id args with Not_a_th_term -> B_atom t)
+    | _ -> B_atom t
+
+  module C = struct
+
+    let get_ty _ _ = Ty.prop
+
+    let abs ~self _a =
+      match T.view self with
+      | Not u -> u, false
+      | _ -> self, true
+
+    let eval id args =
+      let module Value = Sidekick_smt.Value in
+      match view_id id args with
+      | B_not (V_bool b) -> Value.bool (not b)
+      | B_and a when IArray.for_all Value.is_true a -> Value.true_
+      | B_and a when IArray.exists Value.is_false a -> Value.false_
+      | B_or a when IArray.exists Value.is_true a -> Value.true_
+      | B_or a when IArray.for_all Value.is_false a -> Value.false_
+      | B_imply (_, V_bool true) -> Value.true_
+      | B_imply (a,_) when IArray.exists Value.is_false a -> Value.true_
+      | B_imply (a,b) when IArray.for_all Value.is_bool a && Value.is_bool b -> Value.false_
+      | B_atom v -> v
+      | B_not _ | B_and _ | B_or _ | B_imply _
+        -> Error.errorf "non boolean value in boolean connective"
+
+    (* no congruence closure for boolean terms *)
+    let relevant _id _ _ = false
+
+    let mk_cst ?(do_cc=false) id : cst =
+      {cst_id=id;
+       cst_view=Cst_def {
+           pp=None; abs; ty=get_ty; relevant; do_cc; eval=eval id; }; }
+
+    let not = T.not_
+    let and_ = mk_cst id_and
+    let or_ = mk_cst id_or
+    let imply = mk_cst id_imply
+  end
+
+  let as_id id (t:T.t) : T.t IArray.t option =
+    match T.view t with
+    | App_cst ({cst_id; _}, args) when ID.equal id cst_id -> Some args
+    | _ -> None
+
+  (* flatten terms of the given ID *)
+  let flatten_id op sign (l:T.t list) : T.t list =
+    CCList.flat_map
+      (fun t -> match as_id op t with
+         | Some args -> IArray.to_list args
+         | None when (sign && T.is_true t) || (not sign && T.is_false t) ->
+           [] (* idempotent *)
+         | None -> [t])
+      l
+
+  let and_l st l =
+    match flatten_id id_and true l with
+    | [] -> T.true_ st
+    | l when List.exists T.is_false l -> T.false_ st
+    | [x] -> x
+    | args -> T.app_cst st C.and_ (IArray.of_list args)
+
+  let or_l st l =
+    match flatten_id id_or false l with
+    | [] -> T.false_ st
+    | l when List.exists T.is_true l -> T.true_ st
+    | [x] -> x
+    | args -> T.app_cst st C.or_ (IArray.of_list args)
+
+  let and_ st a b = and_l st [a;b]
+  let or_ st a b = or_l st [a;b]
+  let and_a st a = and_l st (IArray.to_list a)
+  let or_a st a = or_l st (IArray.to_list a)
+  let eq = T.eq
+  let not_ = T.not_
+
+  let neq st a b = not_ st @@ eq st a b
+
+  let imply_a st xs y =
+    if IArray.is_empty xs then y
+    else T.app_cst st C.imply (IArray.append (IArray.singleton y) xs)
+
+  let imply_l st xs y = match xs with
+    | [] -> y
+    | _ -> T.app_cst st C.imply (IArray.of_list @@ y :: xs)
+
+  let imply st a b = imply_a st (IArray.singleton a) b
+
+  let make st = function
+    | B_atom t -> t
+    | B_and l -> and_a st l
+    | B_or l -> or_a st l
+    | B_imply (a,b) -> imply_a st a b
+    | B_not t -> not_ st t
+end
+
+module Term_distinct = struct
+  open Sidekick_base_term
+
+  let id_distinct = ID.make "distinct"
+
+  let relevant _id _ _ = true
+  let get_ty _ _ = Ty.prop
+  let abs ~self _a = self, true
+
+  module T = struct
+    include Term
+    let mk_eq = eq
+
+    let as_distinct t : _ option =
+      match view t with
+      | App_cst ({cst_id;_}, args) when ID.equal cst_id id_distinct ->
+        Some (IArray.to_seq args)
+      | _ -> None
+  end
+
+  module Lit = Sidekick_smt.Lit
+
+  let eval args =
+    let module Value = Sidekick_smt.Value in
+    Log.debugf 5
+      (fun k->k "(@[distinct.eval@ %a@])" (Fmt.seq Value.pp) (IArray.to_seq args));
+    if
+      Iter.diagonal (IArray.to_seq args)
+      |> Iter.for_all (fun (x,y) -> not @@ Value.equal x y)
+    then Value.true_
+    else Value.false_
+
+  let c_distinct =
+    {cst_id=id_distinct;
+     cst_view=Cst_def {
+         pp=None; abs; ty=get_ty; relevant; do_cc=true; eval; }; }
+
+  let distinct st a =
+    if IArray.length a <= 1
+    then T.true_ st
+    else T.app_cst st c_distinct a
+
+  let distinct_l st = function
+    | [] | [_] -> T.true_ st
+    | xs -> distinct st (IArray.of_list xs)
+end
+
+module Term_ite = struct
+  open Sidekick_base_term
+
+  let[@inline] view_as_ite t = match Term.view t with
+    | If (a,b,c) -> T_ite (a,b,c)
+    | Bool b -> T_bool b
+    | _ -> T_other t
+end
+
+module Solver = Sidekick_msat_solver.Solver
+
+module Theories = struct
+  module Th_cstor = Sidekick_th_cstor.Make(struct
+      module Solver = Solver
+      module T = Solver.A.Term
+
+      let[@inline] view_as_cstor t = match view t with
+        | App_cst (c, args) when Fun.do_cc
+        | If (a,b,c) -> T_ite (a,b,c)
+        | Bool b -> T_bool b
+        | _ -> T_other t
+      end
+
+    end)
+end
+
 let parse = Parse.parse
 let parse_stdin = Parse.parse_stdin
diff --git a/src/smtlib/dune b/src/smtlib/dune
index d8c89385..edcab872 100644
--- a/src/smtlib/dune
+++ b/src/smtlib/dune
@@ -4,7 +4,7 @@
   (public_name sidekick.smtlib)
   (libraries containers zarith msat sidekick.core sidekick.util
    sidekick.msat-solver sidekick.base-term
-   sidekick.smt.th-bool sidekick.smt.th-distinct msat.backend)
+   sidekick.th-bool sidekick.th-distinct msat.backend)
   (flags :standard -open Sidekick_util))
 
 (menhir (modules Parser))