From d53bd8671aa5a542b89743e631c7213b3ed073a2 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 19 Feb 2018 19:47:03 -0600
Subject: [PATCH] lower overhead for adding clauses to the SAT solver

- directly build clauses from arrays
- use IArrays rather than lists, when possible
- pushing local/persistent clauses is now direct, no more queues
---
 src/backend/Dimacs.ml          |  2 +-
 src/sat/Dagon_sat.ml           |  4 +--
 src/sat/Internal.ml            | 28 ++++++++--------
 src/sat/Res.ml                 |  6 ++--
 src/sat/Solver.ml              | 17 ++++++++--
 src/sat/Solver_intf.ml         | 21 ++++++++++--
 src/sat/Solver_types.ml        |  9 ++---
 src/sat/Solver_types_intf.ml   |  9 +++--
 src/sat/Theory_intf.ml         |  4 +--
 src/smt/Clause.ml              | 30 -----------------
 src/smt/Clause.mli             | 12 -------
 src/smt/Congruence_closure.ml  | 11 ++++++
 src/smt/Congruence_closure.mli | 12 ++++---
 src/smt/Explanation.ml         | 13 +++++++-
 src/smt/Lit.ml                 | 10 +++++-
 src/smt/Lit.mli                | 11 +++++-
 src/smt/Solver.ml              | 32 ++++++++++--------
 src/smt/Solver.mli             |  6 +++-
 src/smt/Theory.ml              | 27 +++++++++++----
 src/smt/Theory_combine.ml      | 61 +++++++++-------------------------
 src/smtlib/Process.ml          |  2 +-
 21 files changed, 178 insertions(+), 149 deletions(-)
 delete mode 100644 src/smt/Clause.ml
 delete mode 100644 src/smt/Clause.mli

diff --git a/src/backend/Dimacs.ml b/src/backend/Dimacs.ml
index d4ac3dcb..8a03a05b 100644
--- a/src/backend/Dimacs.ml
+++ b/src/backend/Dimacs.ml
@@ -103,7 +103,7 @@ module Make(St : Solver_types_intf.S) = struct
              | _ -> assert false)
         (Vec.to_list local)
     in
-    let local = St.Clause.make l St.Local in
+    let local = St.Clause.make_l l St.Local in
     (* Number of atoms and clauses *)
     Format.fprintf fmt
       "@[<v>%s@,%a%a%a@]@."
diff --git a/src/sat/Dagon_sat.ml b/src/sat/Dagon_sat.ml
index 069108ca..eb2ee408 100644
--- a/src/sat/Dagon_sat.ml
+++ b/src/sat/Dagon_sat.ml
@@ -40,8 +40,8 @@ type 'clause export = 'clause Solver_intf.export = {
 }
 
 type ('form, 'proof) actions = ('form,'proof) Theory_intf.actions = Actions of {
-  push : 'form list -> 'proof -> unit;
-  push_local : 'form list -> 'proof -> unit;
+  push_persistent : 'form IArray.t -> 'proof -> unit;
+  push_local : 'form IArray.t -> 'proof -> unit;
   on_backtrack: (unit -> unit) -> unit;
   at_level_0 : unit -> bool;
   propagate : 'form -> 'form list -> 'proof -> unit;
diff --git a/src/sat/Internal.ml b/src/sat/Internal.ml
index b085052d..8616f1ed 100644
--- a/src/sat/Internal.ml
+++ b/src/sat/Internal.ml
@@ -284,7 +284,7 @@ module Make
     ) else if !duplicates = [] then (
       clause
     ) else (
-      Clause.make !res (History [clause])
+      Clause.make_l !res (History [clause])
     )
 
   (* Partition literals for new clauses, into:
@@ -456,7 +456,7 @@ module Make
                with only one formula (which is [a]). So we explicitly create that clause
                and set it as the cause for the propagation of [a], that way we can
                rebuild the whole resolution tree when we want to prove [a]. *)
-            let c' = Clause.make l (History (cl :: history)) in
+            let c' = Clause.make_l l (History (cl :: history)) in
             Log.debugf 5
               (fun k -> k "Simplified reason: @[<v>%a@,%a@]" Clause.debug cl Clause.debug c');
             Bcp c'
@@ -658,13 +658,13 @@ module Make
         if fuip.neg.is_true then (
           report_unsat st confl
         ) else (
-          let uclause = Clause.make cr.cr_learnt (History cr.cr_history) in
+          let uclause = Clause.make_l cr.cr_learnt (History cr.cr_history) in
           Vec.push st.clauses_learnt uclause;
           (* no need to attach [uclause], it is true at level 0 *)
           enqueue_bool st fuip (Bcp uclause)
         )
       | fuip :: _ ->
-        let lclause = Clause.make cr.cr_learnt (History cr.cr_history) in
+        let lclause = Clause.make_l cr.cr_learnt (History cr.cr_history) in
         Vec.push st.clauses_learnt lclause;
         attach_clause st lclause;
         clause_bump_activity st lclause;
@@ -778,7 +778,7 @@ module Make
           List.iteri (fun i a -> c.atoms.(i) <- a) atoms;
           c
         ) else (
-          Clause.make atoms (History (c :: history))
+          Clause.make_l atoms (History (c :: history))
         )
       in
       Log.debugf 3 (fun k->k "(@[sat.add_clause.new_clause@ %a@])" Clause.debug clause);
@@ -912,22 +912,22 @@ module Make
       f a.lit
     done
 
-  let act_push_ ~permanent st (l:formula list) (lemma:proof): unit =
-    let atoms = List.rev_map (mk_atom st) l in
+  let act_push_ ~permanent st (l:formula IArray.t) (lemma:proof): unit =
+    let atoms = IArray.to_array_map (mk_atom st) l in
     let c = Clause.make atoms (Lemma lemma) in
     Log.debugf 3 (fun k->k "(@[sat.push_clause@ %a@])" Clause.debug c);
     add_clause ~permanent st c
 
   (* TODO: ensure that the clause is removed upon backtracking *)
   let act_push_local = act_push_ ~permanent:false
-  let act_push = act_push_ ~permanent:true
+  let act_push_persistent = act_push_ ~permanent:true
 
   (* TODO: ensure that the clause is removed upon backtracking *)
   let act_propagate (st:t) f causes proof : unit =
     let l = List.rev_map (mk_atom st) causes in
     if List.for_all (fun a -> a.is_true) l then (
       let p = mk_atom st f in
-      let c = Clause.make (p :: List.map Atom.neg l) (Lemma proof) in
+      let c = Clause.make_l (p :: List.map Atom.neg l) (Lemma proof) in
       if p.is_true then (
       ) else if p.neg.is_true then (
         add_clause ~permanent:false st c
@@ -953,7 +953,7 @@ module Make
   let act_at_level_0 st () = at_level_0 st
 
   let actions st = Theory_intf.Actions {
-    push = act_push st;
+    push_persistent = act_push_persistent st;
     push_local = act_push_local st;
     on_backtrack = on_backtrack st;
     at_level_0 = act_at_level_0 st;
@@ -996,7 +996,7 @@ module Make
         (* conflict *)
         let l = List.rev_map (mk_atom st) l in
         List.iter (fun a -> insert_var_order st a.var) l;
-        let c = St.Clause.make l (Lemma p) in
+        let c = St.Clause.make_l l (Lemma p) in
         Some c
     )
 
@@ -1120,7 +1120,7 @@ module Make
                 )
               | Theory_intf.Unsat (l, p) ->
                 let atoms = List.rev_map (mk_atom st) l in
-                let c = Clause.make atoms (Lemma p) in
+                let c = Clause.make_l atoms (Lemma p) in
                 Log.debugf 3
                   (fun k -> k "(@[@{<Yellow>sat.theory_conflict_clause@}@ %a@])" Clause.debug c);
                 (* must backtrack *)
@@ -1136,7 +1136,7 @@ module Make
     let cs = List.rev_map
       (fun atoms ->
          let atoms = List.rev_map (mk_atom st) atoms in
-         Clause.make ?tag atoms Hyp)
+         Clause.make_l ?tag atoms Hyp)
       cnf
     in
     let add_clauses () =
@@ -1194,7 +1194,7 @@ module Make
       Log.debugf 3 (fun k-> k "(@[sat.local_assumption@ %a@])" Atom.debug a);
       assert (decision_level st = base_level st);
       if not a.is_true then (
-        let c = Clause.make [a] Local in
+        let c = Clause.make [|a|] Local in
         Log.debugf 5 (fun k -> k "(@[sat.add_temp_clause@ %a@])" Clause.debug c);
         Vec.push st.clauses_temp c;
         if a.neg.is_true then (
diff --git a/src/sat/Res.ml b/src/sat/Res.ml
index 7b5e4010..ae07761e 100644
--- a/src/sat/Res.ml
+++ b/src/sat/Res.ml
@@ -126,7 +126,7 @@ module Make(St : Solver_types.S) = struct
       ) else (
         assert (a.St.neg.St.is_true);
         let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in
-        let c' = St.Clause.make [a.St.neg] r in
+        let c' = St.Clause.make [| a.St.neg |] r in
         a.St.var.St.reason <- Some St.(Bcp c');
         Log.debugf debug
           (fun k -> k "New reason: @[%a@ %a@]" St.Atom.debug a St.Clause.debug c');
@@ -141,7 +141,7 @@ module Make(St : Solver_types.S) = struct
     else (
       Log.debugf info (fun k -> k "Proving unsat from: @[%a@]" St.Clause.debug conflict);
       let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in
-      let res = St.Clause.make [] (St.History (conflict :: l)) in
+      let res = St.Clause.make [| |] (St.History (conflict :: l)) in
       Log.debugf info (fun k -> k "Proof found: @[%a@]" St.Clause.debug res);
       res
     )
@@ -175,7 +175,7 @@ module Make(St : Solver_types.S) = struct
           begin match r with
             | [] -> (l, c, d, a)
             | _ ->
-              let new_clause = St.Clause.make l (St.History [c; d]) in
+              let new_clause = St.Clause.make_l l (St.History [c; d]) in
               chain_res (new_clause, l) r
           end
         | _ ->
diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml
index 84186dba..96c4ee8b 100644
--- a/src/sat/Solver.ml
+++ b/src/sat/Solver.ml
@@ -24,6 +24,7 @@ module Make
 
   type formula = St.formula
   type atom = St.formula
+  type lit = St.atom
   type clause = St.clause
   type theory = Th.t
 
@@ -130,15 +131,25 @@ module Make
     let local = S.temp st in
     {hyps; history; local}
 
+  module Lit = struct
+    type t = lit
+
+    let pp = St.Atom.pp
+    let make = S.mk_atom
+  end
+
   module Clause = struct
     include St.Clause
 
-    let atoms c = St.Clause.atoms c |> Array.map (fun a -> a.St.lit)
+    let atoms c = St.Clause.atoms c |> IArray.of_array_map (fun a -> a.St.lit)
     let atoms_l c = St.Clause.atoms_l c |> List.map (fun a -> a.St.lit)
 
-    let make st ?tag l =
+    let[@inline] make ?tag (a:lit array) : t = St.Clause.make ?tag a St.Hyp
+    let[@inline] make_l ?tag l : t = St.Clause.make_l ?tag l St.Hyp
+
+    let of_atoms st ?tag l =
       let l = List.map (S.mk_atom st) l in
-      St.Clause.make ?tag l St.Hyp
+      make_l ?tag l
   end
 
   module Formula = St.Formula
diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml
index 18f327fa..1f7a5ca6 100644
--- a/src/sat/Solver_intf.ml
+++ b/src/sat/Solver_intf.ml
@@ -48,7 +48,9 @@ module type S = sig
 
   type formula (** user formulas *)
 
-  type clause
+  type lit (** SAT solver literals *)
+
+  type clause (** SAT solver clauses *)
 
   type theory (** user theory *)
 
@@ -133,15 +135,28 @@ module type S = sig
 
   type solver = t
 
+  module Lit : sig
+    type t = lit
+
+    val make : solver -> atom -> t
+    val pp : t CCFormat.printer
+  end
+
   module Clause : sig
     type t = clause
 
-    val atoms : t -> atom array
+    val atoms : t -> atom IArray.t
     val atoms_l : t -> atom list
     val tag : t -> int option
     val equal : t -> t -> bool
 
-    val make : solver -> ?tag:int -> atom list -> t
+    val make : ?tag:int -> lit array -> t
+    (** Make a clause from this array of SAT literals.
+        The array's ownership is transferred to the clause, do not mutate it *)
+
+    val make_l : ?tag:int -> lit list -> t
+
+    val of_atoms : solver -> ?tag:int -> atom list -> t
 
     val pp : t printer
   end
diff --git a/src/sat/Solver_types.ml b/src/sat/Solver_types.ml
index fdc142cf..6446aa2a 100644
--- a/src/sat/Solver_types.ml
+++ b/src/sat/Solver_types.ml
@@ -269,7 +269,7 @@ module Make (E : Theory_intf.S) = struct
         (sign a) (a.var.vid+1) debug_value a E.Form.print a.lit
 
     let debug_a out vec =
-      Array.iter (fun a -> Format.fprintf out "%a@ " debug a) vec
+      Array.iteri (fun i a -> if i>0 then Format.fprintf out "@ "; debug out a) vec
   end
 
   module Clause = struct
@@ -278,8 +278,7 @@ module Make (E : Theory_intf.S) = struct
 
     let make =
       let n = ref 0 in
-      fun ?tag ali premise ->
-        let atoms = Array.of_list ali in
+      fun ?tag atoms premise ->
         let name = !n in
         incr n;
         { name;
@@ -290,7 +289,9 @@ module Make (E : Theory_intf.S) = struct
           cpremise = premise;
         }
 
-    let empty = make [] (History [])
+    let make_l ?tag l pr = make ?tag (Array.of_list l) pr
+
+    let empty = make [| |] (History [])
     let name = name_of_clause
     let[@inline] equal c1 c2 = c1==c2
     let[@inline] atoms c = c.atoms
diff --git a/src/sat/Solver_types_intf.ml b/src/sat/Solver_types_intf.ml
index 7f0024f8..4e99e2a1 100644
--- a/src/sat/Solver_types_intf.ml
+++ b/src/sat/Solver_types_intf.ml
@@ -184,8 +184,13 @@ module type S = sig
     val empty : t
     (** The empty clause *)
 
-    val make : ?tag:int -> Atom.t list -> premise -> clause
-    (** [make_clause name atoms size premise] creates a clause with the given attributes. *)
+    val make : ?tag:int -> Atom.t array -> premise -> t
+    (** [make_clause name atoms size premise] creates a clause with
+        the given attributes.
+        The array's ownership is transferred to the clause, do not
+        mutate it after that. *)
+
+    val make_l : ?tag:int -> Atom.t list -> premise -> t
 
     val pp : t printer
     val pp_dimacs : t printer
diff --git a/src/sat/Theory_intf.ml b/src/sat/Theory_intf.ml
index 96472a62..f2e09027 100644
--- a/src/sat/Theory_intf.ml
+++ b/src/sat/Theory_intf.ml
@@ -42,10 +42,10 @@ type ('formula, 'proof) res =
 (** Actions given to the theory during initialization, to be used
     at any time *)
 type ('form, 'proof) actions = Actions of {
-  push : 'form list -> 'proof -> unit;
+  push_persistent : 'form IArray.t -> 'proof -> unit;
   (** Allows to add a persistent clause to the solver. *)
 
-  push_local : 'form list -> 'proof -> unit;
+  push_local : 'form IArray.t -> 'proof -> unit;
   (** Allows to add a local clause to the solver. The clause
       will be removed after backtracking. *)
 
diff --git a/src/smt/Clause.ml b/src/smt/Clause.ml
deleted file mode 100644
index 63aa7eb7..00000000
--- a/src/smt/Clause.ml
+++ /dev/null
@@ -1,30 +0,0 @@
-
-open Solver_types
-
-type t = Lit.t list
-
-let lits c = c
-
-let pp out c = match lits c with
-  | [] -> Fmt.string out "false"
-  | [lit] -> Lit.pp out lit
-  | l ->
-    Format.fprintf out "[@[<hv>%a@]]"
-      (Util.pp_list ~sep:" ∨ " Lit.pp) l
-
-(* canonical form: sorted list *)
-let make =
-  fun l -> CCList.sort_uniq ~cmp:Lit.compare l
-
-let equal_ c1 c2 = CCList.equal Lit.equal (lits c1) (lits c2)
-let hash_ c = Hash.list Lit.hash (lits c)
-
-module Tbl = CCHashtbl.Make(struct
-    type t_ = t
-    type t = t_
-    let equal = equal_
-    let hash = hash_
-  end)
-
-let iter f c = List.iter f (lits c)
-let to_seq c = Sequence.of_list (lits c)
diff --git a/src/smt/Clause.mli b/src/smt/Clause.mli
deleted file mode 100644
index c2601141..00000000
--- a/src/smt/Clause.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-
-open Solver_types
-
-type t = Lit.t list
-
-val make : Lit.t list -> t
-val lits : t -> Lit.t list
-val iter : (Lit.t -> unit) -> t -> unit
-val to_seq : t -> Lit.t Sequence.t
-val pp : t Fmt.printer
-
-module Tbl : CCHashtbl.S with type key = t
diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml
index 2875defa..1b2cc247 100644
--- a/src/smt/Congruence_closure.ml
+++ b/src/smt/Congruence_closure.ml
@@ -411,6 +411,17 @@ let assert_lit cc lit : unit = match Lit.view lit with
     push_combine cc n rhs (E_lit lit);
     ()
 
+let assert_eq cc (t:term) (u:term) expl : unit =
+  let n1 = add cc t in
+  let n2 = add cc u in
+  if not (same_class cc n1 n2) then (
+    union cc n1 n2 expl
+  )
+
+let assert_distinct _cc (l:term list) _expl : unit =
+  assert (match l with[] | [_] -> false | _ -> true);
+  Util.errorf "unimplemented: CC.distinct"
+
 let create ?(size=2048) ~actions (tst:Term.state) : t =
   assert (actions.at_lvl_0 ());
   let nd = Equiv_class.dummy in
diff --git a/src/smt/Congruence_closure.mli b/src/smt/Congruence_closure.mli
index 79b3abe7..b0cc1313 100644
--- a/src/smt/Congruence_closure.mli
+++ b/src/smt/Congruence_closure.mli
@@ -46,10 +46,6 @@ val same_class : t -> node -> node -> bool
 val union : t -> node -> node -> explanation -> unit
 (** Merge the two equivalence classes. Will be undone on backtracking. *)
 
-val assert_lit : t -> Lit.t -> unit
-(** Given a literal, assume it in the congruence closure and propagate
-    its consequences. Will be backtracked. *)
-
 val mem : t -> term -> bool
 (** Is the term properly added to the congruence closure? *)
 
@@ -63,6 +59,14 @@ val add_seq : t -> term Sequence.t -> unit
 val all_classes : t -> repr Sequence.t
 (** All current classes *)
 
+val assert_lit : t -> Lit.t -> unit
+(** Given a literal, assume it in the congruence closure and propagate
+    its consequences. Will be backtracked. *)
+
+val assert_eq : t -> term -> term -> explanation -> unit
+
+val assert_distinct : t -> term list -> explanation -> unit
+
 val check : t -> unit
 
 val final_check : t -> unit
diff --git a/src/smt/Explanation.ml b/src/smt/Explanation.ml
index 9c5264be..9a301cf2 100644
--- a/src/smt/Explanation.ml
+++ b/src/smt/Explanation.ml
@@ -1,13 +1,24 @@
 
 open Solver_types
 
-type t = explanation
+type t = explanation =
+  | E_reduction
+  | E_lit of lit
+  | E_congruence of cc_node * cc_node
+  | E_injectivity of cc_node * cc_node
+  | E_reduce_eq of cc_node * cc_node
+  | E_custom of {
+      name : ID.t; args : explanation list;
+      pp : (ID.t * explanation list) Fmt.printer;
+    }
 
 let compare = cmp_exp
 let equal a b = cmp_exp a b = 0
 
 let pp = pp_explanation
 
+let[@inline] lit l : t = E_lit l
+
 module Set = CCSet.Make(struct
     type t = explanation
     let compare = compare
diff --git a/src/smt/Lit.ml b/src/smt/Lit.ml
index f13095b5..0b3f35ce 100644
--- a/src/smt/Lit.ml
+++ b/src/smt/Lit.ml
@@ -1,7 +1,15 @@
 
 open Solver_types
 
-type t = lit
+type t = lit = {
+  lit_view : lit_view;
+  lit_sign : bool
+}
+
+and view = lit_view =
+  | Lit_fresh of ID.t
+  | Lit_atom of term
+  | Lit_expanded of term
 
 let neg l = {l with lit_sign=not l.lit_sign}
 
diff --git a/src/smt/Lit.mli b/src/smt/Lit.mli
index 1584d750..d0569339 100644
--- a/src/smt/Lit.mli
+++ b/src/smt/Lit.mli
@@ -2,7 +2,16 @@
 
 open Solver_types
 
-type t = lit
+type t = lit = {
+  lit_view : lit_view;
+  lit_sign : bool
+}
+
+and view = lit_view =
+  | Lit_fresh of ID.t
+  | Lit_atom of term
+  | Lit_expanded of term
+
 val neg : t -> t
 val abs : t -> t
 val sign : t -> bool
diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml
index c2cb5ec4..ff194d06 100644
--- a/src/smt/Solver.ml
+++ b/src/smt/Solver.ml
@@ -13,8 +13,8 @@ type level = int
 
 module Sat_solver = Dagon_sat.Make(Theory_combine)
 
-let[@inline] clause_of_mclause (c:Sat_solver.clause): Clause.t =
-  Sat_solver.Clause.atoms_l c |> Clause.make
+let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
+  Sat_solver.Clause.atoms c
 
 module Proof = struct
   type t = Sat_solver.Proof.proof
@@ -22,8 +22,7 @@ module Proof = struct
   let pp out (p:t) : unit =
     let pp_step_res out p =
       let {Sat_solver.Proof.conclusion; _ } = Sat_solver.Proof.expand p in
-      let conclusion = clause_of_mclause conclusion in
-      Clause.pp out conclusion
+      Sat_solver.Clause.pp out conclusion
     in
     let pp_step out = function
       | Sat_solver.Proof.Lemma _ -> Format.fprintf out "(@[<1>lemma@ ()@])"
@@ -35,9 +34,8 @@ module Proof = struct
     Format.fprintf out "(@[<v>";
     Sat_solver.Proof.fold
       (fun () {Sat_solver.Proof.conclusion; step } ->
-         let conclusion = clause_of_mclause conclusion in
          Format.fprintf out "(@[<hv1>step@ %a@ @[<1>from:@ %a@]@])@,"
-           Clause.pp conclusion pp_step step)
+           Sat_solver.Clause.pp conclusion pp_step step)
       () p;
     Format.fprintf out "@])";
     ()
@@ -51,11 +49,12 @@ type t = {
   config: Config.t
 }
 
-let solver self = self.solver
-let th_combine (self:t) : Theory_combine.t = Sat_solver.theory self.solver
-let add_theory self th = Theory_combine.add_theory (th_combine self) th
+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 tst self = Theory_combine.tst (th_combine self)
+let[@inline] tst self = Theory_combine.tst (th_combine self)
 
 let create ?size ?(config=Config.empty) ~theories () : t =
   let self = {
@@ -359,7 +358,7 @@ end
 (** {2 Main} *)
 
 (* convert unsat-core *)
-let clauses_of_unsat_core (core:Sat_solver.clause list): Clause.t Sequence.t =
+let clauses_of_unsat_core (core:Sat_solver.clause list): Lit.t IArray.t Sequence.t =
   Sequence.of_list core
   |> Sequence.map clause_of_mclause
 
@@ -388,11 +387,18 @@ let do_on_exit ~on_exit =
   List.iter (fun f->f()) on_exit;
   ()
 
-let assume (self:t) (c:Clause.t) : unit =
+let assume (self:t) (c:Lit.t IArray.t) : unit =
   let sat = solver self in
-  let c = Sat_solver.Clause.make sat (Clause.lits c) in
+  let c = Sat_solver.Clause.make (IArray.to_array_map (Sat_solver.Lit.make sat) c) in
   Sat_solver.add_clause ~permanent:false sat c
 
+let[@inline] assume_eq self t u expl : unit =
+  Congruence_closure.assert_eq (cc self) t u (E_lit expl)
+
+let[@inline] assume_distinct self l expl : unit =
+  (* FIXME: custom evaluation instead (register to subterms) *)
+  Congruence_closure.assert_distinct (cc self) l (E_lit expl)
+
 (*
 type unsat_core = Sat.clause list
    *)
diff --git a/src/smt/Solver.mli b/src/smt/Solver.mli
index 72657584..ce7fcc75 100644
--- a/src/smt/Solver.mli
+++ b/src/smt/Solver.mli
@@ -44,10 +44,14 @@ val create :
 val solver : t -> Sat_solver.t
 val th_combine : t -> Theory_combine.t
 val add_theory : t -> Theory.t -> unit
+val cc : t -> Congruence_closure.t
 val stats : t -> Stat.t
 val tst : t -> Term.state
 
-val assume : t -> Clause.t -> unit
+val assume : t -> Lit.t IArray.t -> unit
+
+val assume_eq : t -> Term.t -> Term.t -> Lit.t -> unit
+val assume_distinct : t -> Term.t list -> Lit.t -> unit
 
 val solve :
   ?on_exit:(unit -> unit) list ->
diff --git a/src/smt/Theory.ml b/src/smt/Theory.ml
index 3ec2b03b..a7d696ff 100644
--- a/src/smt/Theory.ml
+++ b/src/smt/Theory.ml
@@ -1,4 +1,19 @@
 
+module 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
+
 (** Runtime state of a theory, with all the operations it provides.
     ['a] is the internal state *)
 type state = State : {
@@ -37,13 +52,13 @@ type actions = {
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 
-  case_split: Clause.t -> unit;
-  (** Force the solver to case split on this clause.
-      The clause will be removed upon backtracking. *)
+  add_local_axiom: Lit.t IArray.t -> unit;
+  (** Add local clause to the SAT solver. This clause will be
+      removed when the solver backtracks. *)
 
-  add_axiom: Clause.t -> unit;
-  (** Add a persistent axiom to the SAT solver. This will not
-      be backtracked *)
+  add_persistent_axiom: Lit.t IArray.t -> unit;
+  (** Add toplevel clause to the SAT solver. This clause will
+      not be backtracked. *)
 
   find: Term.t -> Equiv_class.t;
   (** Find representative of this term *)
diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml
index 8435369f..5e8142d9 100644
--- a/src/smt/Theory_combine.ml
+++ b/src/smt/Theory_combine.ml
@@ -30,13 +30,6 @@ type t = {
   (** congruence closure *)
   mutable theories : Theory.state list;
   (** Set of theories *)
-  lemma_q : Clause.t Queue.t;
-  (** list of clauses that have been newly generated, waiting
-      to be propagated to the core solver.
-      invariant: those clauses must be tautologies *)
-  split_q : Clause.t Queue.t;
-  (** Local clauses to be added to the core solver, that will
-      be removed on backtrack *)
   mutable conflict: conflict option;
   (** current conflict, if any *)
 }
@@ -64,27 +57,10 @@ let assume_lit (self:t) (lit:Lit.t) : unit =
       theories self (fun (Theory.State th) -> th.on_assert th.st lit);
   end
 
-(* push clauses from {!lemma_queue} into the slice *)
-let push_new_clauses_into_cdcl (self:t) : unit =
-  let Sat_solver.Actions r = self.cdcl_acts in
-  (* persistent lemmas *)
-  while not (Queue.is_empty self.lemma_q) do
-    let c = Queue.pop self.lemma_q in
-    Sat_solver.Log.debugf 5 (fun k->k "(@[<2>push_lemma@ %a@])" Clause.pp c);
-    r.push c Proof.default
-  done;
-  (* local splits *)
-  while not (Queue.is_empty self.split_q) do
-    let c = Queue.pop self.split_q in
-    Sat_solver.Log.debugf 5 (fun k->k "(@[<2>split_on@ %a@])" Clause.pp c);
-    r.push_local c Proof.default
-  done
-
 (* return result to the SAT solver *)
 let cdcl_return_res (self:t) : _ Sat_solver.res =
   begin match self.conflict with
     | None ->
-      push_new_clauses_into_cdcl self;
       Sat_solver.Sat
     | Some c ->
       let lit_set =
@@ -93,13 +69,12 @@ let cdcl_return_res (self:t) : _ Sat_solver.res =
       in
       let conflict_clause =
         Lit.Set.to_list lit_set
-        |> List.map Lit.neg
-        |> Clause.make
+        |> IArray.of_list_map Lit.neg
       in
       Sat_solver.Log.debugf 3
         (fun k->k "(@[<1>conflict@ clause: %a@])"
-            Clause.pp conflict_clause);
-      Sat_solver.Unsat (Clause.lits conflict_clause, Proof.default)
+            Theory.Clause.pp conflict_clause);
+      Sat_solver.Unsat (IArray.to_list conflict_clause, Proof.default)
   end
 
 let[@inline] check (self:t) : unit =
@@ -153,7 +128,7 @@ let act_propagate (self:t) f guard : unit =
   in
   Sat_solver.Log.debugf 2
     (fun k->k "(@[@{<green>propagate@}@ %a@ :guard %a@])"
-        Lit.pp f Clause.pp guard);
+        Lit.pp f (Util.pp_list Lit.pp) guard);
   r.propagate f guard Proof.default
 
 (** {2 Interface to Congruence Closure} *)
@@ -190,8 +165,6 @@ let create (cdcl_acts:_ Sat_solver.actions) : t =
       Congruence_closure.create ~size:1024 ~actions self.tst;
     );
     theories = [];
-    lemma_q = Queue.create();
-    split_q = Queue.create();
     conflict = None;
   } in
   ignore @@ Lazy.force @@ self.cc;
@@ -202,37 +175,35 @@ let create (cdcl_acts:_ Sat_solver.actions) : t =
 let act_all_classes self = Congruence_closure.all_classes (cc self)
 
 let act_propagate_eq self t u guard =
-  let r_t = Congruence_closure.add (cc self) t in
-  let r_u = Congruence_closure.add (cc self) u in
-  Congruence_closure.union (cc self) r_t r_u guard
+  Congruence_closure.assert_eq (cc self) t u guard
 
 let act_find self t =
   Congruence_closure.add (cc self) t
   |> Congruence_closure.find (cc self)
 
-let act_case_split self (c:Clause.t) =
-  Sat_solver.Log.debugf 2 (fun k->k "(@[<1>add_split@ @[%a@]@])" Clause.pp c);
-  Queue.push c self.split_q
+let act_add_local_axiom self c : unit =
+  Sat_solver.Log.debugf 5 (fun k->k "(@[<2>th_combine.push_local_lemma@ %a@])" Theory.Clause.pp c);
+  let Sat_solver.Actions r = self.cdcl_acts in
+  r.push_local c Proof.default
 
 (* push one clause into [M], in the current level (not a lemma but
    an axiom) *)
-let act_add_axiom self (c:Clause.t): unit =
-  Sat_solver.Log.debugf 2 (fun k->k "(@[<1>add_axiom@ @[%a@]@])" Clause.pp c);
-  (* TODO incr stat_num_clause_push; *)
-  Queue.push c self.lemma_q
+let act_add_persistent_axiom self c : unit =
+  Sat_solver.Log.debugf 5 (fun k->k "(@[<2>th_combine.push_persistent_lemma@ %a@])" Theory.Clause.pp c);
+  let Sat_solver.Actions r = self.cdcl_acts in
+  r.push_persistent c Proof.default
 
 let mk_theory_actions (self:t) : Theory.actions =
   let Sat_solver.Actions r = self.cdcl_acts in
-  {
-    Theory.
+  { Theory.
     on_backtrack = r.on_backtrack;
     at_lvl_0 = r.at_level_0;
     raise_conflict = act_raise_conflict;
     propagate = act_propagate self;
     all_classes = act_all_classes self;
     propagate_eq = act_propagate_eq self;
-    case_split = act_case_split self;
-    add_axiom = act_add_axiom self;
+    add_local_axiom = act_add_local_axiom self;
+    add_persistent_axiom = act_add_persistent_axiom self;
     find = act_find self;
   }
 
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index f57dc829..027c3f9a 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -310,7 +310,7 @@ let process_stmt
       (* TODO
       hyps := clauses @ !hyps;
          *)
-      Solver.assume solver (Clause.make [Lit.atom t]);
+      Solver.assume solver (IArray.singleton (Lit.atom t));
       E.return()
     | A.Goal (_, _) ->
       Util.errorf "cannot deal with goals yet"