add th-bool-dyn for dynamic boolean clausification

src/base/Sidekick_base.ml

@@ -29,14 +29,19 @@ module Select = Data_ty.Select
 module Statement = Statement
 module Solver = Solver
 module Uconst = Uconst
+module Config = Config
 module Th_data = Th_data
 module Th_bool = Th_bool
 (* FIXME
    module Th_lra = Th_lra
 *)
 
-let th_bool : Solver.theory = Th_bool.theory
+let k_th_bool_config = Th_bool.k_config
+let th_bool = Th_bool.theory
+let th_bool_dyn : Solver.theory = Th_bool.theory_dyn
+let th_bool_static : Solver.theory = Th_bool.theory_static
 let th_data : Solver.theory = Th_data.theory
+
 (* FIXME
    let th_lra : Solver.theory = Th_lra.theory
 *)

src/base/dune

@@ -4,5 +4,5 @@
  (synopsis "Base term definitions for the standalone SMT solver and library")
  (libraries containers iter sidekick.core sidekick.util sidekick.smt-solver
    sidekick.cc sidekick.quip sidekick.th-lra sidekick.th-bool-static
-   sidekick.th-data sidekick.zarith zarith)
+   sidekick.th-bool-dyn sidekick.th-data sidekick.zarith zarith)
  (flags :standard -w +32 -open Sidekick_util))

src/base/th_bool.ml

@@ -1,8 +1,25 @@
 (** Reducing boolean formulas to clauses *)
 
-let theory : Solver.theory =
+let k_config : [ `Dyn | `Static ] Config.Key.t = Config.Key.create ()
+
+let theory_static : Solver.theory =
   Sidekick_th_bool_static.theory
     (module struct
       let view_as_bool = Form.view
       let mk_bool = Form.mk_of_view
     end : Sidekick_th_bool_static.ARG)
+
+let theory_dyn : Solver.theory =
+  Sidekick_th_bool_dyn.theory
+    (module struct
+      let view_as_bool = Form.view
+      let mk_bool = Form.mk_of_view
+    end : Sidekick_th_bool_static.ARG)
+
+let theory (conf : Config.t) : Solver.theory =
+  match Config.find k_config conf with
+  | Some `Dyn -> theory_dyn
+  | Some `Static -> theory_static
+  | None ->
+    (* default *)
+    theory_static

src/main/main.ml

@@ -7,6 +7,7 @@ Copyright 2014 Simon Cruanes
 module E = CCResult
 module Fmt = CCFormat
 module Term = Sidekick_base.Term
+module Config = Sidekick_base.Config
 module Solver = Sidekick_smtlib.Solver
 module Process = Sidekick_smtlib.Process
 module Proof = Sidekick_smtlib.Proof_trace
@@ -23,7 +24,7 @@ let p_proof = ref false
 let p_model = ref false
 let check = ref false
 let time_limit = ref 300.
-let size_limit = ref 1_000_000_000.
+let mem_limit = ref 1_000_000_000.
 let restarts = ref true
 let gc = ref true
 let p_stat = ref false
@@ -62,6 +63,7 @@ let int_arg r arg =
 let input_file s = file := s
 let usage = "Usage : main [options] <file>"
 let version = "%%version%%"
+let config = ref Config.empty
 
 let argspec =
   Arg.align
@@ -90,12 +92,23 @@ let argspec =
       "-o", Arg.Set_string proof_file, " file into which to output a proof";
       "--model", Arg.Set p_model, " print model";
       "--no-model", Arg.Clear p_model, " do not print model";
+      ( "--bool",
+        Arg.Symbol
+          ( [ "dyn"; "static" ],
+            function
+            | "dyn" ->
+              config := Config.add Sidekick_base.k_th_bool_config `Dyn !config
+            | "static" ->
+              config :=
+                Config.add Sidekick_base.k_th_bool_config `Static !config
+            | _s -> failwith "unknown" ),
+        " configure bool theory" );
       "--gc-stat", Arg.Set p_gc_stat, " outputs statistics about the GC";
       "-p", Arg.Set p_progress, " print progress bar";
       "--no-p", Arg.Clear p_progress, " no progress bar";
-      ( "--size",
-        Arg.String (int_arg size_limit),
-        " <s>[kMGT] sets the size limit for the sat solver" );
+      ( "--memory",
+        Arg.String (int_arg mem_limit),
+        " <s>[kMGT] sets the memory limit for the sat solver" );
       ( "--time",
         Arg.String (int_arg time_limit),
         " <t>[smhd] sets the time limit for the sat solver" );
@@ -118,10 +131,10 @@ let check_limits () =
   let s = float heap_size *. float Sys.word_size /. 8. in
   if t > !time_limit then
     raise Out_of_time
-  else if s > !size_limit then
+  else if s > !mem_limit then
     raise Out_of_space
 
-let main_smt () : _ result =
+let main_smt ~config () : _ result =
   let tst = Term.Store.create ~size:4_096 () in
 
   let enable_proof_ = !check || !p_proof || !proof_file <> "" in
@@ -159,9 +172,14 @@ let main_smt () : _ result =
   let proof = Proof.dummy in
 
   let solver =
+    (* TODO: probes, to load only required theories *)
     let theories =
-      (* TODO: probes, to load only required theories *)
-      [ Process.th_bool; Process.th_data (* FIXME Process.th_lra *) ]
+      let th_bool = Process.th_bool config in
+      Log.debugf 1 (fun k ->
+          k "(@[main.th-bool.pick@ %S@])"
+            (Sidekick_smt_solver.Theory.name th_bool));
+      Sidekick_smt_solver.Theory.
+        [ th_bool; Process.th_data (* FIXME Process.th_lra *) ]
     in
     Process.Solver.create_default ~proof ~theories tst
   in
@@ -187,7 +205,7 @@ let main_smt () : _ result =
       E.fold_l
         (fun () ->
           Process.process_stmt ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf
-            ~time:!time_limit ~memory:!size_limit ~pp_model:!p_model ?proof_file
+            ~time:!time_limit ~memory:!mem_limit ~pp_model:!p_model ?proof_file
             ~check:!check ~progress:!p_progress solver)
         () input
     with Exit -> E.return ()
@@ -250,7 +268,7 @@ let main () =
     if is_cnf then
       main_cnf ()
     else
-      main_smt ()
+      main_smt ~config:!config ()
   in
   Gc.delete_alarm al;
   res

src/smtlib/Process.ml

@@ -163,8 +163,14 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false)
       let memory = Option.value ~default:4e9 memory in
       (* default: 4 GB *)
       let stop _ _ =
-        Sys.time () -. t1 > time
-        || (Gc.quick_stat ()).Gc.major_words *. 8. > memory
+        if Sys.time () -. t1 > time then (
+          Log.debugf 0 (fun k -> k "timeout");
+          true
+        ) else if (Gc.quick_stat ()).Gc.major_words *. 8. > memory then (
+          Log.debugf 0 (fun k -> k "%S" "exceeded memory limit");
+          true
+        ) else
+          false
       in
       Some stop
   in
@@ -335,7 +341,9 @@ module Th_bool = Sidekick_base.Th_bool
    module Th_lra = Sidekick_base.Th_lra
 *)
 
-let th_bool : Solver.theory = Th_bool.theory
+let th_bool = Th_bool.theory
+let th_bool_dyn : Solver.theory = Th_bool.theory_dyn
+let th_bool_static : Solver.theory = Th_bool.theory_static
 let th_data : Solver.theory = Th_data.theory
 (* FIXME
    let th_lra : Solver.theory = Th_lra.theory

src/smtlib/Process.mli

@@ -3,7 +3,9 @@
 open Sidekick_base
 module Solver = Sidekick_base.Solver
 
-val th_bool : Solver.theory
+val th_bool_dyn : Solver.theory
+val th_bool_static : Solver.theory
+val th_bool : Config.t -> Solver.theory
 val th_data : Solver.theory
 (* FIXME
    val th_lra : Solver.theory

src/th-bool-dyn/Sidekick_th_bool_dyn.ml

@@ -1,126 +1,354 @@
-(** {1 Theory of Booleans} *)
+open Sidekick_core
+module Intf = Intf
+open Intf
+module SI = SMT.Solver_internal
+module Proof_rules = Proof_rules
+module T = Term
 
-(** {2 Signatures for booleans} *)
-module View = struct
-  type 'a t =
-    | B_not of 'a
-    | B_and of 'a array
-    | B_or of 'a array
-    | B_imply of 'a array * 'a
-    | B_atom of 'a
-end
-
-module type ARG = sig
-  module S : Sidekick_core.SOLVER
-
-  type term = S.A.Term.t
-
-  val view_as_bool : term -> term View.t
-  val mk_bool : S.A.Term.state -> term View.t -> term
-end
-
-module type S = sig
-  module A : ARG
-
-  val theory : A.S.theory
-end
+module type ARG = Intf.ARG
 
 (** Theory with dynamic reduction to clauses *)
-module Make_dyn_tseitin (A : ARG) = (*   : S with module A = A *)
-struct
+module Make (A : ARG) : sig
+  val theory : SMT.theory
+end = struct
   (* TODO (long term): relevancy propagation *)
 
-  (* TODO: Tseitin on the fly when a composite boolean term is asserted.
-     --> maybe, cache the clause inside the literal *)
-
-  module A = A
-  module SI = A.S.Solver_internal
-  module T = SI.A.Term
-  module Lit = SI.A.Lit
-
   type term = T.t
 
-  module T_tbl = CCHashtbl.Make (T)
+  type state = {
+    tst: T.store;
+    expanded: unit Lit.Tbl.t; (* set of literals already expanded *)
+    n_simplify: int Stat.counter;
+    n_expanded: int Stat.counter;
+    n_clauses: int Stat.counter;
+    n_propagate: int Stat.counter;
+  }
 
-  type t = { expanded: unit T_tbl.t (* set of literals already expanded *) }
+  let create ~stat tst : state =
+    {
+      tst;
+      expanded = Lit.Tbl.create 256;
+      n_simplify = Stat.mk_int stat "th.bool.simplified";
+      n_expanded = Stat.mk_int stat "th.bool.expanded";
+      n_clauses = Stat.mk_int stat "th.bool.clauses";
+      n_propagate = Stat.mk_int stat "th.bool.propagations";
+    }
 
-  let tseitin ~final (self : t) (solver : SI.t) (lit : Lit.t) (lit_t : term)
-      (v : term View.t) : unit =
-    Log.debugf 5 (fun k -> k "(@[th_bool.tseitin@ %a@])" Lit.pp lit);
-    let expanded () = T_tbl.mem self.expanded lit_t in
-    let add_axiom c =
-      T_tbl.replace self.expanded lit_t ();
-      SI.add_persistent_axiom solver c
+  let[@inline] not_ tst t = A.mk_bool tst (B_not t)
+  let[@inline] eq tst a b = A.mk_bool tst (B_eq (a, b))
+  let pp_c_ = Fmt.Dump.list Lit.pp
+
+  let is_true t =
+    match T.as_bool_val t with
+    | Some true -> true
+    | _ -> false
+
+  let is_false t =
+    match T.as_bool_val t with
+    | Some false -> true
+    | _ -> false
+
+  (* TODO: share this with th-bool-static by way of a library for
+     boolean simplification? (also handle one-point rule and the likes) *)
+  let simplify (self : state) (simp : Simplify.t) (t : T.t) :
+      (T.t * Proof_step.id Iter.t) option =
+    let tst = self.tst in
+
+    let proof = Simplify.proof simp in
+    let steps = ref [] in
+    let add_step_ s = steps := s :: !steps in
+    let mk_step_ r = Proof_trace.add_step proof r in
+
+    let add_step_eq a b ~using ~c0 : unit =
+      add_step_ @@ mk_step_
+      @@ fun () ->
+      Proof_core.lemma_rw_clause c0 ~using
+        ~res:[ Lit.atom (A.mk_bool tst (B_eq (a, b))) ]
     in
-    match v with
-    | B_not _ -> assert false (* normalized *)
-    | B_atom _ -> () (* CC will manage *)
-    | B_and subs ->
-      if Lit.sign lit then
-        (* propagate [lit => subs_i] *)
-        CCArray.iter
-          (fun sub ->
-            let sublit = SI.mk_lit solver sub in
-            SI.propagate_l solver sublit [ lit ])
-          subs
-      else if final && (not @@ expanded ()) then (
-        (* axiom [¬lit => ∨_i ¬ subs_i] *)
-        let subs = CCArray.to_list subs in
-        let c = Lit.neg lit :: List.map (SI.mk_lit solver ~sign:false) subs in
-        add_axiom c
-      )
-    | B_or subs ->
-      if not @@ Lit.sign lit then
-        (* propagate [¬lit => ¬subs_i] *)
-        CCArray.iter
-          (fun sub ->
-            let sublit = SI.mk_lit solver ~sign:false sub in
-            SI.add_local_axiom solver [ Lit.neg lit; sublit ])
-          subs
-      else if final && (not @@ expanded ()) then (
-        (* axiom [lit => ∨_i subs_i] *)
-        let subs = CCArray.to_list subs in
-        let c = Lit.neg lit :: List.map (SI.mk_lit solver ~sign:true) subs in
-        add_axiom c
-      )
-    | B_imply (guard, concl) ->
-      if Lit.sign lit && final && (not @@ expanded ()) then (
-        (* axiom [lit => ∨_i ¬guard_i ∨ concl] *)
-        let guard = CCArray.to_list guard in
-        let c =
-          SI.mk_lit solver concl :: Lit.neg lit
-          :: List.map (SI.mk_lit solver ~sign:false) guard
-        in
-        add_axiom c
-      ) else if not @@ Lit.sign lit then (
-        (* propagate [¬lit => ¬concl] *)
-        SI.propagate_l solver (SI.mk_lit solver ~sign:false concl) [ lit ];
-        (* propagate [¬lit => ∧_i guard_i] *)
-        CCArray.iter
-          (fun sub ->
-            let sublit = SI.mk_lit solver ~sign:true sub in
-            SI.propagate_l solver sublit [ lit ])
-          guard
-      )
 
-  let check_ ~final self solver lits =
+    let[@inline] ret u =
+      Stat.incr self.n_simplify;
+      Some (u, Iter.of_list !steps)
+    in
+
+    (* proof is [t <=> u] *)
+    let ret_bequiv t1 u =
+      (add_step_ @@ mk_step_ @@ fun () -> Proof_rules.lemma_bool_equiv t1 u);
+      ret u
+    in
+
+    match A.view_as_bool t with
+    | B_bool _ -> None
+    | B_not u when is_true u -> ret_bequiv t (T.false_ tst)
+    | B_not u when is_false u -> ret_bequiv t (T.true_ tst)
+    | B_not _ -> None
+    | B_atom _ -> None
+    | B_and (a, b) ->
+      if is_false a || is_false b then
+        ret (T.false_ tst)
+      else if is_true a && is_true b then
+        ret (T.true_ tst)
+      else
+        None
+    | B_or (a, b) ->
+      if is_true a || is_true b then
+        ret (T.true_ tst)
+      else if is_false a && is_false b then
+        ret (T.false_ tst)
+      else
+        None
+    | B_imply (a, b) ->
+      if is_false a || is_true b then
+        ret (T.true_ tst)
+      else if is_true a && is_false b then
+        ret (T.false_ tst)
+      else
+        None
+    | B_ite (a, b, c) ->
+      (* directly simplify [a] so that maybe we never will simplify one
+         of the branches *)
+      let a, prf_a = Simplify.normalize_t simp a in
+      Option.iter add_step_ prf_a;
+      (match A.view_as_bool a with
+      | B_bool true ->
+        add_step_eq t b ~using:(Option.to_list prf_a)
+          ~c0:(mk_step_ @@ fun () -> Proof_rules.lemma_ite_true ~ite:t);
+        ret b
+      | B_bool false ->
+        add_step_eq t c ~using:(Option.to_list prf_a)
+          ~c0:(mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t);
+        ret c
+      | _ -> None)
+    | B_equiv (a, b) when is_true a -> ret_bequiv t b
+    | B_equiv (a, b) when is_false a -> ret_bequiv t (not_ tst b)
+    | B_equiv (a, b) when is_true b -> ret_bequiv t a
+    | B_equiv (a, b) when is_false b -> ret_bequiv t (not_ tst a)
+    | B_xor (a, b) when is_false a -> ret_bequiv t b
+    | B_xor (a, b) when is_true a -> ret_bequiv t (not_ tst b)
+    | B_xor (a, b) when is_false b -> ret_bequiv t a
+    | B_xor (a, b) when is_true b -> ret_bequiv t (not_ tst a)
+    | B_equiv _ | B_xor _ -> None
+    | B_eq (a, b) when T.equal a b -> ret_bequiv t (T.true_ tst)
+    | B_neq (a, b) when T.equal a b -> ret_bequiv t (T.true_ tst)
+    | B_eq _ | B_neq _ -> None
+
+  let[@inline] expanded self lit = Lit.Tbl.mem self.expanded lit
+
+  let set_expanded self lit : unit =
+    if not (expanded self lit) then (
+      Stat.incr self.n_expanded;
+      Lit.Tbl.add self.expanded lit ()
+    )
+
+  (* preprocess. *)
+  let preprocess_ (self : state) (_si : SI.t) (module PA : SI.PREPROCESS_ACTS)
+      (t : T.t) : unit =
+    Log.debugf 50 (fun k -> k "(@[th-bool.dny.preprocess@ %a@])" T.pp_debug t);
+    let[@inline] mk_step_ r = Proof_trace.add_step PA.proof r in
+
+    (match A.view_as_bool t with
+    | B_ite (a, b, c) ->
+      let lit_a = PA.mk_lit a in
+      Stat.incr self.n_clauses;
+      PA.add_clause
+        [ Lit.neg lit_a; PA.mk_lit (eq self.tst t b) ]
+        (mk_step_ @@ fun () -> Proof_rules.lemma_ite_true ~ite:t);
+
+      Stat.incr self.n_clauses;
+      PA.add_clause
+        [ lit_a; PA.mk_lit (eq self.tst t c) ]
+        (mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t)
+    | _ -> ());
+    ()
+
+  let tseitin ~final (self : state) solver (acts : SI.theory_actions)
+      (lit : Lit.t) (t : term) (v : term bool_view) : unit =
+    Log.debugf 50 (fun k -> k "(@[th-bool-dyn.tseitin@ %a@])" Lit.pp lit);
+
+    let add_axiom c pr : unit =
+      Log.debugf 50 (fun k ->
+          k "(@[th-bool-dyn.add-axiom@ %a@ :expanding %a@])" pp_c_ c Lit.pp lit);
+      Stat.incr self.n_clauses;
+      set_expanded self lit;
+      SI.add_clause_permanent solver acts c pr
+    in
+
+    let[@inline] mk_step_ r = Proof_trace.add_step (SI.proof solver) r in
+
+    (* handle boolean equality *)
+    let equiv_ ~is_xor a b : unit =
+      (* [a xor b] is [(¬a) = b] *)
+      let a =
+        if is_xor then
+          Lit.neg a
+        else
+          a
+      in
+
+      (* [lit => a<=> b],
+         [¬lit => a xor b] *)
+      add_axiom
+        [ Lit.neg lit; Lit.neg a; b ]
+        (if is_xor then
+          mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-e+" [ t ]
+        else
+          mk_step_ @@ fun () ->
+          Proof_rules.lemma_bool_c "eq-e" [ t; Lit.term a ]);
+
+      add_axiom
+        [ Lit.neg lit; Lit.neg b; a ]
+        (if is_xor then
+          mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-e-" [ t ]
+        else
+          mk_step_ @@ fun () ->
+          Proof_rules.lemma_bool_c "eq-e" [ t; Lit.term b ]);
+
+      add_axiom [ lit; a; b ]
+        (if is_xor then
+          mk_step_ @@ fun () ->
+          Proof_rules.lemma_bool_c "xor-i" [ t; Lit.term a ]
+        else
+          mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-i+" [ t ]);
+
+      add_axiom
+        [ lit; Lit.neg a; Lit.neg b ]
+        (if is_xor then
+          mk_step_ @@ fun () ->
+          Proof_rules.lemma_bool_c "xor-i" [ t; Lit.term b ]
+        else
+          mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-i-" [ t ])
+    in
+
+    match v with
+    | B_not _ -> ()
+    | B_atom _ -> () (* CC will manage *)
+    | B_bool true -> ()
+    | B_bool false ->
+      SI.add_clause_permanent solver acts
+        [ Lit.neg lit ]
+        (mk_step_ @@ fun () -> Proof_core.lemma_true (Lit.term lit))
+    | _ when expanded self lit -> () (* already done *)
+    | B_and (a, b) ->
+      let subs = List.map Lit.atom [ a; b ] in
+
+      if Lit.sign lit then
+        (* propagate [(and …t_i) => t_i] *)
+        List.iter
+          (fun sub ->
+            Stat.incr self.n_propagate;
+            SI.propagate_l solver acts sub [ lit ]
+              ( mk_step_ @@ fun () ->
+                Proof_rules.lemma_bool_c "and-e" [ t; Lit.term sub ] ))
+          subs
+      else if final then (
+        (* axiom [¬(and …t_i)=> \/_i (¬ t_i)], only in final-check *)
+        let c = Lit.neg lit :: List.map Lit.neg subs in
+        add_axiom c
+          (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-i" [ t ])
+      )
+    | B_or (a, b) ->
+      let subs = List.map Lit.atom [ a; b ] in
+
+      if not @@ Lit.sign lit then
+        (* propagate [¬sub_i \/ lit] *)
+        List.iter
+          (fun sub ->
+            Stat.incr self.n_propagate;
+            SI.propagate_l solver acts (Lit.neg sub) [ lit ]
+              ( mk_step_ @@ fun () ->
+                Proof_rules.lemma_bool_c "or-i" [ t; Lit.term sub ] ))
+          subs
+      else if final then (
+        (* axiom [lit => \/_i subs_i] *)
+        let c = Lit.neg lit :: subs in
+        add_axiom c (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "or-e" [ t ])
+      )
+    | B_imply (a, b) ->
+      let a = Lit.atom a in
+      let b = Lit.atom b in
+      if Lit.sign lit && final then (
+        (* axiom [lit => a => b] *)
+        let c = [ Lit.neg lit; Lit.neg a; b ] in
+        add_axiom c
+          (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "imp-e" [ t ])
+      ) else if not @@ Lit.sign lit then (
+        (* propagate [¬ lit => ¬b] and [¬lit => a] *)
+        Stat.incr self.n_propagate;
+        SI.propagate_l solver acts a [ lit ]
+          ( mk_step_ @@ fun () ->
+            Proof_rules.lemma_bool_c "imp-i" [ t; Lit.term a ] );
+
+        Stat.incr self.n_propagate;
+        SI.propagate_l solver acts (Lit.neg b) [ lit ]
+          ( mk_step_ @@ fun () ->
+            Proof_rules.lemma_bool_c "imp-i" [ t; Lit.term b ] )
+      )
+    | B_ite (a, b, c) ->
+      assert (T.is_bool b);
+      if final then (
+        (* boolean ite:
+           just add [a => (ite a b c <=> b)]
+           and [¬a => (ite a b c <=> c)] *)
+        let lit_a = Lit.atom a in
+        add_axiom
+          [ Lit.neg lit_a; Lit.make_eq self.tst t b ]
+          (mk_step_ @@ fun () -> Proof_rules.lemma_ite_true ~ite:t);
+        add_axiom
+          [ Lit.neg lit; lit_a; Lit.make_eq self.tst t c ]
+          (mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t)
+      )
+    | B_equiv (a, b) ->
+      let a = Lit.atom a in
+      let b = Lit.atom b in
+      equiv_ ~is_xor:false a b
+    | B_eq (a, b) when T.is_bool a ->
+      let a = Lit.atom a in
+      let b = Lit.atom b in
+      equiv_ ~is_xor:false a b
+    | B_xor (a, b) ->
+      let a = Lit.atom a in
+      let b = Lit.atom b in
+      equiv_ ~is_xor:true a b
+    | B_neq (a, b) when T.is_bool a ->
+      let a = Lit.atom a in
+      let b = Lit.atom b in
+      equiv_ ~is_xor:true a b
+    | B_eq _ | B_neq _ -> ()
+
+  let check_ ~final self solver acts lits =
     lits (fun lit ->
         let t = Lit.term lit in
         match A.view_as_bool t with
         | B_atom _ -> ()
-        | v -> tseitin ~final self solver lit t v)
+        | v -> tseitin ~final self solver acts lit t v)
 
-  let partial_check (self : t) acts (lits : Lit.t Iter.t) =
-    check_ ~final:false self acts lits
+  let partial_check (self : state) solver acts (lits : Lit.t Iter.t) =
+    check_ ~final:false self solver acts lits
 
-  let final_check (self : t) acts (lits : Lit.t Iter.t) =
-    check_ ~final:true self acts lits
+  let final_check (self : state) solver acts (lits : Lit.t Iter.t) =
+    check_ ~final:true self solver acts lits
 
-  let create_and_setup (solver : SI.t) : t =
-    let self = { expanded = T_tbl.create 24 } in
+  let create_and_setup (solver : SI.t) : state =
+    let tst = SI.tst solver in
+    let stat = SI.stats solver in
+    let self =
+      {
+        tst;
+        expanded = Lit.Tbl.create 24;
+        n_expanded = Stat.mk_int stat "th.bool.dyn.expanded";
+        n_clauses = Stat.mk_int stat "th.bool.dyn.clauses";
+        n_propagate = Stat.mk_int stat "th.bool.dyn.propagate";
+        n_simplify = Stat.mk_int stat "th.bool.dyn.simplify";
+      }
+    in
+    SI.on_preprocess solver (preprocess_ self);
     SI.on_final_check solver (final_check self);
     SI.on_partial_check solver (partial_check self);
     self
 
-  let theory = A.S.mk_theory ~name:"boolean" ~create_and_setup ()
+  let theory = SMT.Solver.mk_theory ~name:"th-bool.dyn" ~create_and_setup ()
 end
+
+let theory (module A : ARG) : SMT.theory =
+  let module M = Make (A) in
+  M.theory

src/th-bool-dyn/dune.bak

@@ -1,6 +0,0 @@
-(library
-  (name Sidekick_th_bool_dyn)
-  (public_name sidekick.th-bool-dyn)
-  (libraries containers sidekick.core sidekick.util)
-  (flags :standard -open Sidekick_util))
-

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -270,7 +270,7 @@ end = struct
     SI.on_preprocess si (cnf st);
     st
 
-  let theory = SMT.Solver.mk_theory ~name:"th-bool" ~create_and_setup ()
+  let theory = SMT.Solver.mk_theory ~name:"th-bool.static" ~create_and_setup ()
 end
 
 let theory (module A : ARG) : SMT.theory =