wip: refactor(smt): remove layers of functors, split into modules

src/smt/Sidekick_smt_solver.ml

@@ -0,0 +1,14 @@
+(** Core of the SMT solver using Sidekick_sat
+
+    Sidekick_sat (in src/sat/) is a modular SAT solver in
+    pure OCaml.
+
+    This builds a SMT solver on top of it.
+*)
+
+module Sigs = Sigs
+module Model = Model
+module Registry = Registry
+module Simplify = Simplify
+module Solver_internal = Solver_internal
+module Solver = Solver

src/smt/dune

@@ -0,0 +1,7 @@
+(library
+ (name Sidekick_smt_solver)
+ (public_name sidekick.smt-solver)
+ (synopsis "main SMT solver")
+ (libraries containers iter sidekick.core sidekick.util sidekick.cc
+   sidekick.sat)
+ (flags :standard -w +32 -open Sidekick_util))

src/smt/model.ml

@@ -0,0 +1,24 @@
+open Sigs
+
+type t = Empty | Map of term Term.Tbl.t
+
+let empty = Empty
+
+let mem = function
+  | Empty -> fun _ -> false
+  | Map tbl -> Term.Tbl.mem tbl
+
+let find = function
+  | Empty -> fun _ -> None
+  | Map tbl -> Term.Tbl.get tbl
+
+let eval = find
+
+let pp out = function
+  | Empty -> Fmt.string out "(model)"
+  | Map tbl ->
+    let pp_pair out (t, v) =
+      Fmt.fprintf out "(@[<1>%a@ := %a@])" Term.pp_debug t Term.pp_debug v
+    in
+    Fmt.fprintf out "(@[<hv>model@ %a@])" (Util.pp_iter pp_pair)
+      (Term.Tbl.to_iter tbl)

src/smt/registry.ml

@@ -0,0 +1,37 @@
+
+  (* registry keys *)
+  module type KEY = sig
+    type elt
+
+    val id : int
+
+    exception E of elt
+  end
+
+  type 'a key = (module KEY with type elt = 'a)
+  type t = { tbl: exn Util.Int_tbl.t } [@@unboxed]
+
+  let create () : t = { tbl = Util.Int_tbl.create 8 }
+  let n_ = ref 0
+
+  let create_key (type a) () : a key =
+    let id = !n_ in
+    incr n_;
+    let module K = struct
+      type elt = a
+
+      exception E of a
+
+      let id = id
+    end in
+    (module K)
+
+  let get (type a) (self : t) (k : a key) : _ option =
+    let (module K : KEY with type elt = a) = k in
+    match Util.Int_tbl.get self.tbl K.id with
+    | Some (K.E x) -> Some x
+    | _ -> None
+
+  let set (type a) (self : t) (k : a key) (v : a) : unit =
+    let (module K) = k in
+    Util.Int_tbl.replace self.tbl K.id (K.E v)

src/smt/registry.mli

@@ -0,0 +1,14 @@
+
+
+(** Registry to extract values *)
+
+  type t
+  type 'a key
+
+  val create_key : unit -> 'a key
+  (** Call this statically, typically at program initialization, for
+      each distinct key. *)
+
+  val create : unit -> t
+  val get : t -> 'a key -> 'a option
+  val set : t -> 'a key -> 'a -> unit

src/smt/sigs.ml

@@ -0,0 +1,48 @@
+(** Signature for the main SMT solver types.
+
+    Theories and concrete solvers rely on an environment that defines
+    several important types:
+
+    - sorts
+    - terms (to represent logic expressions and formulas)
+    - a congruence closure instance
+    - a bridge to some SAT solver
+
+    In this module we collect signatures defined elsewhere and define
+    the module types for the main SMT solver.
+*)
+
+include Sidekick_core
+module CC = Sidekick_cc.CC
+module E_node = Sidekick_cc.E_node
+module CC_expl = Sidekick_cc.Expl
+
+type term = Term.t
+type ty = term
+type value = Term.t
+type lit = Lit.t
+type term_store = Term.store
+type proof_trace = Proof_trace.t
+type step_id = Proof_step.id
+
+(* actions from the sat solver *)
+type sat_acts = Sidekick_sat.acts
+
+type th_combination_conflict = {
+  lits: lit list;
+  semantic: (bool * term * term) list;
+      (* set of semantic eqns/diseqns (ie true only in current model) *)
+}
+(** Conflict obtained during theory combination. It involves equalities
+      merged because of the current model so it's not a "true" conflict
+      and doesn't need to kill the current trail. *)
+
+(** Argument to pass to the functor {!Make} in order to create a
+    new Msat-based SMT solver. *)
+module type ARG = sig
+  val view_as_cc : Sidekick_cc.view_as_cc
+
+  val is_valid_literal : Term.t -> bool
+  (** Is this a valid boolean literal? (e.g. is it a closed term, not inside
+      a quantifier) *)
+end

src/smt/simplify.ml

@@ -0,0 +1,81 @@
+open Sidekick_core
+open Sigs
+
+open struct
+  module P = Proof_trace
+  module Rule_ = Proof_core
+end
+
+type t = {
+  tst: term_store;
+  proof: proof_trace;
+  mutable hooks: hook list;
+  (* store [t --> u by step_ids] in the cache.
+     We use a bag for the proof steps because it gives us structural
+     sharing of subproofs. *)
+  cache: (Term.t * step_id Bag.t) Term.Tbl.t;
+}
+
+and hook = t -> term -> (term * step_id Iter.t) option
+
+let create tst ~proof : t =
+  { tst; proof; hooks = []; cache = Term.Tbl.create 32 }
+
+let[@inline] tst self = self.tst
+let[@inline] proof self = self.proof
+let add_hook self f = self.hooks <- f :: self.hooks
+let clear self = Term.Tbl.clear self.cache
+
+let normalize (self : t) (t : Term.t) : (Term.t * step_id) option =
+  (* compute and cache normal form of [t] *)
+  let rec loop t : Term.t * _ Bag.t =
+    match Term.Tbl.find self.cache t with
+    | res -> res
+    | exception Not_found ->
+      let steps_u = ref Bag.empty in
+      let u = aux_rec ~steps:steps_u t self.hooks in
+      Term.Tbl.add self.cache t (u, !steps_u);
+      u, !steps_u
+  and loop_add ~steps t =
+    let u, pr_u = loop t in
+    steps := Bag.append !steps pr_u;
+    u
+  (* try each function in [hooks] successively, and rewrite subterms *)
+  and aux_rec ~steps t hooks : Term.t =
+    match hooks with
+    | [] ->
+      let u =
+        Term.map_shallow self.tst ~f:(fun _inb u -> loop_add ~steps u) t
+      in
+      if Term.equal t u then
+        t
+      else
+        loop_add ~steps u
+    | h :: hooks_tl ->
+      (match h self t with
+      | None -> aux_rec ~steps t hooks_tl
+      | Some (u, _) when Term.equal t u -> aux_rec ~steps t hooks_tl
+      | Some (u, pr_u) ->
+        let bag_u = Bag.of_iter pr_u in
+        steps := Bag.append !steps bag_u;
+        let v, pr_v = loop u in
+        (* fixpoint *)
+        steps := Bag.append !steps pr_v;
+        v)
+  in
+  let u, pr_u = loop t in
+  if Term.equal t u then
+    None
+  else (
+    (* proof: [sub_proofs |- t=u] by CC + subproof *)
+    let step =
+      P.add_step self.proof
+      @@ Rule_.lemma_preprocess t u ~using:(Bag.to_iter pr_u)
+    in
+    Some (u, step)
+  )
+
+let normalize_t self t =
+  match normalize self t with
+  | Some (u, pr_u) -> u, Some pr_u
+  | None -> t, None

src/smt/simplify.mli

@@ -0,0 +1,39 @@
+(** Term simplifier *)
+
+open Sidekick_core
+open Sigs
+
+type t
+
+val tst : t -> term_store
+
+val clear : t -> unit
+(** Reset internal cache, etc. *)
+
+val proof : t -> proof_trace
+(** Access proof *)
+
+type hook = t -> term -> (term * step_id Iter.t) option
+(** Given a term, try to simplify it. Return [None] if it didn't change.
+
+        A simple example could be a hook that takes a term [t],
+        and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number,
+        returns [Some (const (x+y))], and [None] otherwise.
+
+        The simplifier will take care of simplifying the resulting term further,
+        caching (so that work is not duplicated in subterms), etc.
+    *)
+
+val add_hook : t -> hook -> unit
+
+val normalize : t -> term -> (term * step_id) option
+(** Normalize a term using all the hooks. This performs
+    a fixpoint, i.e. it only stops when no hook applies anywhere inside
+    the term. *)
+
+val normalize_t : t -> term -> term * step_id option
+(** Normalize a term using all the hooks, along with a proof that the
+    simplification is correct.
+    returns [t, ø] if no simplification occurred. *)
+
+val create : Term.store -> proof:Proof_trace.t -> t

src/smt/solver.ml

@@ -0,0 +1,261 @@
+open Sigs
+
+open struct
+  module P = Proof_trace
+  module Rule_ = Proof_core
+end
+
+(* TODO
+   let mk_cc_acts_ (pr : P.t) (a : sat_acts) : CC.actions =
+     let (module A) = a in
+
+     (module struct
+       module T = T
+       module Lit = Lit
+
+       type nonrec lit = lit
+       type nonrec term = term
+       type nonrec proof_trace = Proof_trace.t
+       type nonrec step_id = step_id
+
+       let proof_trace () = pr
+       let[@inline] raise_conflict lits (pr : step_id) = A.raise_conflict lits pr
+
+       let[@inline] raise_semantic_conflict lits semantic =
+         raise (Semantic_conflict { lits; semantic })
+
+       let[@inline] propagate lit ~reason =
+         let reason = Sidekick_sat.Consequence reason in
+         A.propagate lit reason
+     end)
+*)
+
+module Sat_solver = Sidekick_sat.Make_cdcl_t (Solver_internal)
+(** the parametrized SAT Solver *)
+
+(** {2 Result} *)
+
+module Unknown = struct
+  type t = U_timeout | U_max_depth | U_incomplete | U_asked_to_stop
+
+  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"|}
+    | U_asked_to_stop -> Fmt.string out {|"asked to stop by callback"|}
+end
+[@@ocaml.warning "-37"]
+
+type res =
+  | Sat of Model.t
+  | Unsat of {
+      unsat_core: unit -> lit Iter.t;
+          (** Unsat core (subset of assumptions), or empty *)
+      unsat_step_id: unit -> step_id option;
+          (** Proof step for the empty clause *)
+    }
+  | Unknown of Unknown.t
+      (** Result of solving for the current set of clauses *)
+
+(* main solver state *)
+type t = {
+  si: Solver_internal.t;
+  solver: Sat_solver.t;
+  mutable last_res: res option;
+  stat: Stat.t;
+  proof: P.t;
+  count_clause: int Stat.counter;
+  count_solve: int Stat.counter; (* config: Config.t *)
+}
+
+type solver = t
+
+(** {2 Main} *)
+
+type theory = Theory.t
+
+let mk_theory = Theory.make
+
+let add_theory_p (type a) (self : t) (th : a Theory.p) : a =
+  let (module Th) = th in
+  Log.debugf 2 (fun k -> k "(@[smt-solver.add-theory@ :name %S@])" Th.name);
+  let st = Th.create_and_setup self.si in
+  (* add push/pop to the internal solver *)
+  Solver_internal.add_theory_state self.si ~st ~push_level:Th.push_level
+    ~pop_levels:Th.pop_levels;
+  st
+
+let add_theory (self : t) (th : theory) : unit =
+  let (module Th) = th in
+  ignore (add_theory_p self (module Th))
+
+let add_theory_l self = List.iter (add_theory self)
+
+(* create a new solver *)
+let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t =
+  Log.debug 5 "smt-solver.create";
+  let si = Solver_internal.create arg ~stat ~proof tst () in
+  let self =
+    {
+      si;
+      proof;
+      last_res = None;
+      solver = Sat_solver.create ~proof ?size ~stat si;
+      stat;
+      count_clause = Stat.mk_int stat "solver.add-clause";
+      count_solve = Stat.mk_int stat "solver.solve";
+    }
+  in
+  add_theory_l self theories;
+  (* assert [true] and [not false] *)
+  (let tst = Solver_internal.tst self.si in
+   let t_true = Term.true_ tst in
+   Sat_solver.add_clause self.solver
+     [ Lit.atom t_true ]
+     (P.add_step self.proof @@ Rule_.lemma_true t_true));
+  self
+
+let[@inline] solver self = self.solver
+let[@inline] cc self = Solver_internal.cc self.si
+let[@inline] stats self = self.stat
+let[@inline] tst self = Solver_internal.tst self.si
+let[@inline] proof self = self.proof
+let[@inline] last_res self = self.last_res
+let[@inline] registry self = Solver_internal.registry self.si
+let reset_last_res_ self = self.last_res <- None
+
+(* preprocess clause, return new proof *)
+let preprocess_clause_ (self : t) (c : lit array) (pr : step_id) :
+    lit array * step_id =
+  Solver_internal.preprocess_clause_iarray_ self.si c pr
+
+let mk_lit_t (self : t) ?sign (t : term) : lit =
+  let lit = Lit.atom ?sign t in
+  let lit, _ = Solver_internal.simplify_and_preproc_lit_ self.si lit in
+  lit
+
+(** {2 Main} *)
+
+let pp_stats out (self : t) : unit = Stat.pp_all out (Stat.all @@ stats self)
+
+(* add [c], without preprocessing its literals *)
+let add_clause_nopreproc_ (self : t) (c : lit array) (proof : step_id) : unit =
+  Stat.incr self.count_clause;
+  reset_last_res_ self;
+  Log.debugf 50 (fun k ->
+      k "(@[solver.add-clause@ %a@])" (Util.pp_array Lit.pp) c);
+  let pb = Profile.begin_ "add-clause" in
+  Sat_solver.add_clause_a self.solver (c :> lit array) proof;
+  Profile.exit pb
+
+let add_clause_nopreproc_l_ self c p =
+  add_clause_nopreproc_ self (CCArray.of_list c) p
+
+module Perform_delayed_ = Solver_internal.Perform_delayed (struct
+  type nonrec t = t
+
+  let add_clause _si solver ~keep:_ c pr : unit =
+    add_clause_nopreproc_l_ solver c pr
+
+  let add_lit _si solver ?default_pol lit : unit =
+    Sat_solver.add_lit solver.solver ?default_pol lit
+end)
+
+let add_clause (self : t) (c : lit array) (proof : step_id) : unit =
+  let c, proof = preprocess_clause_ self c proof in
+  add_clause_nopreproc_ self c proof;
+  Perform_delayed_.top self.si self;
+  (* finish preproc *)
+  ()
+
+let add_clause_l self c p = add_clause self (CCArray.of_list c) p
+
+let assert_terms self c =
+  let c = CCList.map (fun t -> Lit.atom (tst self) t) c in
+  let pr_c =
+    P.add_step self.proof @@ A.Rule_sat.sat_input_clause (Iter.of_list c)
+  in
+  add_clause_l self c pr_c
+
+let assert_term self t = assert_terms self [ t ]
+
+exception Resource_exhausted = Sidekick_sat.Resource_exhausted
+
+let solve ?(on_exit = []) ?(check = true) ?(on_progress = fun _ -> ())
+    ?(should_stop = fun _ _ -> false) ~assumptions (self : t) : res =
+  Profile.with_ "smt-solver.solve" @@ fun () ->
+  let do_on_exit () = List.iter (fun f -> f ()) on_exit in
+
+  let on_progress =
+    let resource_counter = ref 0 in
+    fun () ->
+      incr resource_counter;
+      on_progress self;
+      if should_stop self !resource_counter then
+        raise_notrace Resource_exhausted
+  in
+  self.si.on_progress <- on_progress;
+
+  let res =
+    match
+      Stat.incr self.count_solve;
+      Sat_solver.solve ~on_progress ~assumptions (solver self)
+    with
+    | Sat_solver.Sat _ when not self.si.complete ->
+      Log.debugf 1 (fun k ->
+          k
+            "(@[sidekick.smt-solver: SAT@ actual: UNKNOWN@ :reason \
+             incomplete-fragment@])");
+      Unknown Unknown.U_incomplete
+    | Sat_solver.Sat _ ->
+      Log.debug 1 "(sidekick.smt-solver: SAT)";
+
+      Log.debugf 5 (fun k ->
+          let ppc out n =
+            Fmt.fprintf out "{@[<hv>class@ %a@]}" (Util.pp_iter N.pp)
+              (N.iter_class n)
+          in
+          k "(@[sidekick.smt-solver.classes@ (@[%a@])@])" (Util.pp_iter ppc)
+            (CC.all_classes @@ Solver_internal.cc self.si));
+
+      let m =
+        match self.si.last_model with
+        | Some m -> m
+        | None -> assert false
+      in
+      (* TODO: check model *)
+      let _ = check in
+
+      do_on_exit ();
+      Sat m
+    | Sat_solver.Unsat (module UNSAT) ->
+      let unsat_core () = UNSAT.unsat_assumptions () in
+      let unsat_step_id () = Some (UNSAT.unsat_proof ()) in
+      do_on_exit ();
+      Unsat { unsat_core; unsat_step_id }
+    | exception Resource_exhausted -> Unknown Unknown.U_asked_to_stop
+  in
+  self.last_res <- Some res;
+  res
+
+let push_assumption self a =
+  reset_last_res_ self;
+  Sat_solver.push_assumption self.solver a
+
+let pop_assumptions self n =
+  reset_last_res_ self;
+  Sat_solver.pop_assumptions self.solver n
+
+type propagation_result =
+  | PR_sat
+  | PR_conflict of { backtracked: int }
+  | PR_unsat of { unsat_core: unit -> lit Iter.t }
+
+let check_sat_propagations_only ~assumptions self : propagation_result =
+  reset_last_res_ self;
+  match Sat_solver.check_sat_propagations_only ~assumptions self.solver with
+  | Sat_solver.PR_sat -> PR_sat
+  | Sat_solver.PR_conflict { backtracked } -> PR_conflict { backtracked }
+  | Sat_solver.PR_unsat (module UNSAT) ->
+    let unsat_core () = UNSAT.unsat_assumptions () in
+    PR_unsat { unsat_core }

src/smt/solver.mli

@@ -0,0 +1,189 @@
+(** Main solver type, user facing.
+
+    This is the solver a user of sidekick can see, after instantiating
+    everything. The user can add some theories, clauses, etc. and asks
+    the solver to check satisfiability.
+
+    Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *)
+
+open Sigs
+
+type t
+(** The solver's state. *)
+
+val registry : t -> Registry.t
+(** A solver contains a registry so that theories can share data *)
+
+type theory = Theory.t
+type 'a theory_p = 'a Theory.p
+
+val mk_theory :
+  name:string ->
+  create_and_setup:(Solver_internal.t -> 'th) ->
+  ?push_level:('th -> unit) ->
+  ?pop_levels:('th -> int -> unit) ->
+  unit ->
+  theory
+(** Helper to create a theory. *)
+
+(** Models
+
+      A model can be produced when the solver is found to be in a
+      satisfiable state after a call to {!solve}. *)
+module Model : sig
+  type t
+
+  val empty : t
+  val mem : t -> term -> bool
+  val find : t -> term -> term option
+  val eval : t -> term -> term option
+  val pp : t Fmt.printer
+end
+
+(* TODO *)
+module Unknown : sig
+  type t
+
+  val pp : t CCFormat.printer
+
+  (*
+    type unknown =
+      | U_timeout
+      | U_incomplete
+       *)
+end
+
+(** {3 Main API} *)
+
+val stats : t -> Stat.t
+val tst : t -> Term.store
+val proof : t -> proof_trace
+
+val create :
+  (module ARG) ->
+  ?stat:Stat.t ->
+  ?size:[ `Big | `Tiny | `Small ] ->
+  (* TODO? ?config:Config.t -> *)
+  proof:proof_trace ->
+  theories:theory list ->
+  Term.store ->
+  unit ->
+  t
+(** Create a new solver.
+
+      It needs a term state and a type state to manipulate terms and types.
+      All terms and types interacting with this solver will need to come
+      from these exact states.
+
+      @param store_proof if true, proofs from the SAT solver and theories
+      are retained and potentially accessible after {!solve}
+      returns UNSAT.
+      @param size influences the size of initial allocations.
+      @param theories theories to load from the start. Other theories
+      can be added using {!add_theory}. *)
+
+val add_theory : t -> theory -> unit
+(** Add a theory to the solver. This should be called before
+      any call to {!solve} or to {!add_clause} and the likes (otherwise
+      the theory will have a partial view of the problem). *)
+
+val add_theory_p : t -> 'a theory_p -> 'a
+(** Add the given theory and obtain its state *)
+
+val add_theory_l : t -> theory list -> unit
+
+val mk_lit_t : t -> ?sign:bool -> term -> lit
+(** [mk_lit_t _ ~sign t] returns [lit'],
+      where [lit'] is [preprocess(lit)] and [lit] is
+      an internal representation of [± t].
+
+      The proof of [|- lit = lit'] is directly added to the solver's proof. *)
+
+val add_clause : t -> lit array -> step_id -> unit
+(** [add_clause solver cs] adds a boolean clause to the solver.
+      Subsequent calls to {!solve} will need to satisfy this clause. *)
+
+val add_clause_l : t -> lit list -> step_id -> unit
+(** Add a clause to the solver, given as a list. *)
+
+val assert_terms : t -> term list -> unit
+(** Helper that turns each term into an atom, before adding the result
+      to the solver as an assertion *)
+
+val assert_term : t -> term -> unit
+(** Helper that turns the term into an atom, before adding the result
+      to the solver as a unit clause assertion *)
+
+(** Result of solving for the current set of clauses *)
+type res =
+  | Sat of Model.t  (** Satisfiable *)
+  | Unsat of {
+      unsat_core: unit -> lit Iter.t;
+          (** Unsat core (subset of assumptions), or empty *)
+      unsat_step_id: unit -> step_id option;
+          (** Proof step for the empty clause *)
+    }  (** Unsatisfiable *)
+  | Unknown of Unknown.t
+      (** Unknown, obtained after a timeout, memory limit, etc. *)
+
+(* TODO: API to push/pop/clear assumptions, in addition to ~assumptions param *)
+
+val solve :
+  ?on_exit:(unit -> unit) list ->
+  ?check:bool ->
+  ?on_progress:(t -> unit) ->
+  ?should_stop:(t -> int -> bool) ->
+  assumptions:lit list ->
+  t ->
+  res
+(** [solve s] checks the satisfiability of the clauses added so far to [s].
+      @param check if true, the model is checked before returning.
+      @param on_progress called regularly during solving.
+      @param assumptions a set of atoms held to be true. The unsat core,
+        if any, will be a subset of [assumptions].
+      @param should_stop a callback regularly called with the solver,
+        and with a number of "steps" done since last call. The exact notion
+        of step is not defined, but is guaranteed to increase regularly.
+        The function should return [true] if it judges solving
+        must stop (returning [Unknown]), [false] if solving can proceed.
+      @param on_exit functions to be run before this returns *)
+
+val last_res : t -> res option
+(** Last result, if any. Some operations will erase this (e.g. {!assert_term}). *)
+
+val push_assumption : t -> lit -> unit
+(** Pushes an assumption onto the assumption stack. It will remain
+      there until it's pop'd by {!pop_assumptions}. *)
+
+val pop_assumptions : t -> int -> unit
+(** [pop_assumptions solver n] removes [n] assumptions from the stack.
+      It removes the assumptions that were the most
+      recently added via {!push_assumptions}.
+      Note that {!check_sat_propagations_only} can call this if it meets
+      a conflict. *)
+
+type propagation_result =
+  | PR_sat
+  | PR_conflict of { backtracked: int }
+  | PR_unsat of { unsat_core: unit -> lit Iter.t }
+
+val check_sat_propagations_only :
+  assumptions:lit list -> t -> propagation_result
+(** [check_sat_propagations_only solver] uses assumptions (including
+      the [assumptions] parameter, and atoms previously added via {!push_assumptions})
+      and boolean+theory propagation to quickly assess satisfiability.
+      It is not complete; calling {!solve} is required to get an accurate
+      result.
+      @returns one of:
+
+      - [PR_sat] if the current state seems satisfiable
+      - [PR_conflict {backtracked=n}] if a conflict was found and resolved,
+      leading to backtracking [n] levels of assumptions
+      - [PR_unsat …] if the assumptions were found to be unsatisfiable, with
+        the given core.
+  *)
+
+(* TODO: allow on_progress to return a bool to know whether to stop? *)
+
+val pp_stats : t CCFormat.printer
+(** Print some statistics. What it prints exactly is unspecified. *)

src/smt/solver_internal.ml

@@ -0,0 +1,608 @@
+open Sigs
+module Proof_rules = Sidekick_core.Proof_sat
+module P_core_rules = Sidekick_core.Proof_core
+module N = Sidekick_cc.E_node
+module Ty = Term
+
+open struct
+  module P = Proof_trace
+  module Rule_ = Proof_core
+end
+
+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 the sat solver *)
+type sat_acts = Sidekick_sat.acts
+type theory_actions = sat_acts
+type simplify_hook = Simplify.hook
+
+module type PREPROCESS_ACTS = sig
+  val proof : proof_trace
+  val mk_lit : ?sign:bool -> term -> lit
+  val add_clause : lit list -> step_id -> unit
+  val add_lit : ?default_pol:bool -> lit -> unit
+end
+
+type preprocess_actions = (module PREPROCESS_ACTS)
+
+module Registry = Registry
+
+(* delayed actions. We avoid doing them on the spot because, when
+   triggered by a theory, they might go back to the theory "too early". *)
+type delayed_action =
+  | DA_add_clause of { c: lit list; pr: step_id; keep: bool }
+  | DA_add_lit of { default_pol: bool option; lit: lit }
+
+type t = {
+  tst: Term.store;  (** state for managing terms *)
+  cc: CC.t;  (** congruence closure *)
+  proof: proof_trace;  (** proof logger *)
+  registry: Registry.t;
+  mutable on_progress: unit -> unit;
+  mutable on_partial_check: (t -> theory_actions -> lit Iter.t -> unit) list;
+  mutable on_final_check: (t -> theory_actions -> lit Iter.t -> unit) list;
+  mutable on_th_combination:
+    (t -> theory_actions -> (term * value) Iter.t) list;
+  mutable preprocess: preprocess_hook list;
+  mutable model_ask: model_ask_hook list;
+  mutable model_complete: model_completion_hook list;
+  simp: Simplify.t;
+  preprocessed: unit Term.Tbl.t;
+  delayed_actions: delayed_action Queue.t;
+  mutable last_model: Model.t option;
+  mutable th_states: th_states;  (** Set of theories *)
+  mutable level: int;
+  mutable complete: bool;
+  stat: Stat.t;
+  count_axiom: int Stat.counter;
+  count_preprocess_clause: int Stat.counter;
+  count_conflict: int Stat.counter;
+  count_propagate: int Stat.counter;
+}
+
+and preprocess_hook = t -> preprocess_actions -> term -> unit
+and model_ask_hook = recurse:(t -> N.t -> term) -> t -> N.t -> term option
+and model_completion_hook = t -> add:(term -> term -> unit) -> unit
+
+type solver = t
+
+let[@inline] cc (self : t) = self.cc
+let[@inline] tst self = self.tst
+let[@inline] proof self = self.proof
+let stats self = self.stat
+
+let[@inline] has_delayed_actions self =
+  not (Queue.is_empty self.delayed_actions)
+
+let registry self = self.registry
+let simplifier self = self.simp
+let simplify_t self (t : Term.t) : _ option = Simplify.normalize self.simp t
+let simp_t self (t : Term.t) : Term.t * _ = Simplify.normalize_t self.simp t
+let add_simplifier (self : t) f : unit = Simplify.add_hook self.simp f
+
+let on_th_combination self f =
+  self.on_th_combination <- f :: self.on_th_combination
+
+let on_preprocess self f = self.preprocess <- f :: self.preprocess
+
+let on_model ?ask ?complete self =
+  Option.iter (fun f -> self.model_ask <- f :: self.model_ask) ask;
+  Option.iter
+    (fun f -> self.model_complete <- f :: self.model_complete)
+    complete;
+  ()
+
+let[@inline] raise_conflict self (acts : theory_actions) c proof : 'a =
+  let (module A) = acts in
+  Stat.incr self.count_conflict;
+  A.raise_conflict c proof
+
+let[@inline] propagate self (acts : theory_actions) p ~reason : unit =
+  let (module A) = acts in
+  Stat.incr self.count_propagate;
+  A.propagate p (Sidekick_sat.Consequence reason)
+
+let[@inline] propagate_l self acts p cs proof : unit =
+  propagate self acts p ~reason:(fun () -> cs, proof)
+
+let add_sat_clause_ self (acts : theory_actions) ~keep lits (proof : step_id) :
+    unit =
+  let (module A) = acts in
+  Stat.incr self.count_axiom;
+  A.add_clause ~keep lits proof
+
+let add_sat_lit_ _self ?default_pol (acts : theory_actions) (lit : Lit.t) : unit
+    =
+  let (module A) = acts in
+  A.add_lit ?default_pol lit
+
+let delayed_add_lit (self : t) ?default_pol (lit : Lit.t) : unit =
+  Queue.push (DA_add_lit { default_pol; lit }) self.delayed_actions
+
+let delayed_add_clause (self : t) ~keep (c : Lit.t list) (pr : step_id) : unit =
+  Queue.push (DA_add_clause { c; pr; keep }) self.delayed_actions
+
+let preprocess_term_ (self : t) (t0 : term) : unit =
+  let module A = struct
+    let proof = self.proof
+    let mk_lit ?sign t : Lit.t = Lit.atom ?sign t
+    let add_lit ?default_pol lit : unit = delayed_add_lit self ?default_pol lit
+    let add_clause c pr : unit = delayed_add_clause self ~keep:true c pr
+  end in
+  let acts = (module A : PREPROCESS_ACTS) in
+
+  (* how to preprocess a term and its subterms *)
+  let rec preproc_rec_ t =
+    if not (Term.Tbl.mem self.preprocessed t) then (
+      Term.Tbl.add self.preprocessed t ();
+
+      (* process sub-terms first *)
+      Term.iter_shallow t ~f:(fun _inb u -> preproc_rec_ u);
+
+      Log.debugf 50 (fun k -> k "(@[smt.preprocess@ %a@])" Term.pp_debug t);
+
+      (* signal boolean subterms, so as to decide them
+         in the SAT solver *)
+      if Ty.is_bool (Term.ty t) then (
+        Log.debugf 5 (fun k ->
+            k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp_debug
+              t);
+
+        (* make a literal *)
+        let lit = Lit.atom t in
+        (* ensure that SAT solver has a boolean atom for [u] *)
+        delayed_add_lit self lit;
+
+        (* also map [sub] to this atom in the congruence closure, for propagation *)
+        let cc = cc self in
+        CC.set_as_lit cc (CC.add_term cc t) lit
+      );
+
+      List.iter (fun f -> f self acts t) self.preprocess
+    )
+  in
+  preproc_rec_ t0
+
+(* simplify literal, then preprocess the result *)
+let simplify_and_preproc_lit_ (self : t) (lit : Lit.t) : Lit.t * step_id option
+    =
+  let t = Lit.term lit in
+  let sign = Lit.sign lit in
+  let u, pr =
+    match simplify_t self t with
+    | None -> t, None
+    | Some (u, pr_t_u) ->
+      Log.debugf 30 (fun k ->
+          k "(@[smt-solver.simplify@ :t %a@ :into %a@])" Term.pp_debug t
+            Term.pp_debug u);
+      u, Some pr_t_u
+  in
+  preprocess_term_ self u;
+  Lit.atom ~sign u, pr
+
+let push_decision (self : t) (acts : theory_actions) (lit : lit) : unit =
+  let (module A) = acts in
+  (* make sure the literal is preprocessed *)
+  let lit, _ = simplify_and_preproc_lit_ self lit in
+  let sign = Lit.sign lit in
+  A.add_decision_lit (Lit.abs lit) sign
+
+module type ARR = sig
+  type 'a t
+
+  val map : ('a -> 'b) -> 'a t -> 'b t
+  val to_iter : 'a t -> 'a Iter.t
+end
+
+module Preprocess_clause (A : ARR) = struct
+  (* preprocess a clause's literals, possibly emitting a proof
+     for the preprocessing. *)
+  let top (self : t) (c : lit A.t) (pr_c : step_id) : lit A.t * step_id =
+    let steps = ref [] in
+
+    (* simplify a literal, then preprocess it *)
+    let[@inline] simp_lit lit =
+      let lit, pr = simplify_and_preproc_lit_ self lit in
+      Option.iter (fun pr -> steps := pr :: !steps) pr;
+      lit
+    in
+    let c' = A.map simp_lit c in
+
+    let pr_c' =
+      if !steps = [] then
+        pr_c
+      else (
+        Stat.incr self.count_preprocess_clause;
+        P.add_step self.proof
+        @@ Rule_.lemma_rw_clause pr_c ~res:(A.to_iter c')
+             ~using:(Iter.of_list !steps)
+      )
+    in
+    c', pr_c'
+end
+[@@inline]
+
+module PC_list = Preprocess_clause (CCList)
+module PC_arr = Preprocess_clause (CCArray)
+
+let preprocess_clause_ = PC_list.top
+let preprocess_clause_iarray_ = PC_arr.top
+
+module type PERFORM_ACTS = sig
+  type t
+
+  val add_clause : solver -> t -> keep:bool -> lit list -> step_id -> unit
+  val add_lit : solver -> t -> ?default_pol:bool -> lit -> unit
+end
+
+module Perform_delayed (A : PERFORM_ACTS) = struct
+  (* perform actions that were delayed *)
+  let top (self : t) (acts : A.t) : unit =
+    while not (Queue.is_empty self.delayed_actions) do
+      let act = Queue.pop self.delayed_actions in
+      match act with
+      | DA_add_clause { c; pr = pr_c; keep } ->
+        let c', pr_c' = preprocess_clause_ self c pr_c in
+        A.add_clause self acts ~keep c' pr_c'
+      | DA_add_lit { default_pol; lit } ->
+        preprocess_term_ self (Lit.term lit);
+        A.add_lit self acts ?default_pol lit
+    done
+end
+[@@inline]
+
+module Perform_delayed_th = Perform_delayed (struct
+  type t = theory_actions
+
+  let add_clause self acts ~keep c pr : unit =
+    add_sat_clause_ self acts ~keep c pr
+
+  let add_lit self acts ?default_pol lit : unit =
+    add_sat_lit_ self acts ?default_pol lit
+end)
+
+let[@inline] add_clause_temp self _acts c (proof : step_id) : unit =
+  let c, proof = preprocess_clause_ self c proof in
+  delayed_add_clause self ~keep:false c proof
+
+let[@inline] add_clause_permanent self _acts c (proof : step_id) : unit =
+  let c, proof = preprocess_clause_ self c proof in
+  delayed_add_clause self ~keep:true c proof
+
+let[@inline] mk_lit _ ?sign t : lit = Lit.atom ?sign t
+
+let[@inline] add_lit self _acts ?default_pol lit =
+  delayed_add_lit self ?default_pol lit
+
+let add_lit_t self _acts ?sign t =
+  let lit = Lit.atom ?sign t in
+  let lit, _ = simplify_and_preproc_lit_ self lit in
+  delayed_add_lit self lit
+
+let on_final_check self f = self.on_final_check <- f :: self.on_final_check
+
+let on_partial_check self f =
+  self.on_partial_check <- f :: self.on_partial_check
+
+let on_cc_new_term self f = Event.on (CC.on_new_term (cc self)) ~f
+let on_cc_pre_merge self f = Event.on (CC.on_pre_merge (cc self)) ~f
+let on_cc_post_merge self f = Event.on (CC.on_post_merge (cc self)) ~f
+let on_cc_conflict self f = Event.on (CC.on_conflict (cc self)) ~f
+let on_cc_propagate self f = Event.on (CC.on_propagate (cc self)) ~f
+let on_cc_is_subterm self f = Event.on (CC.on_is_subterm (cc self)) ~f
+let cc_add_term self t = CC.add_term (cc self) t
+let cc_mem_term self t = CC.mem_term (cc self) t
+let cc_find self n = CC.find (cc self) n
+
+let cc_are_equal self t1 t2 =
+  let n1 = cc_add_term self t1 in
+  let n2 = cc_add_term self t2 in
+  N.equal (cc_find self n1) (cc_find self n2)
+
+let cc_resolve_expl self e : lit list * _ =
+  let r = CC.explain_expl (cc self) e in
+  r.lits, r.pr self.proof
+
+(*
+    let cc_merge self _acts n1 n2 e = CC.merge (cc self) n1 n2 e
+
+    let cc_merge_t self acts t1 t2 e =
+      let cc_acts = mk_cc_acts_ self.proof acts in
+      cc_merge self cc_acts (cc_add_term self t1) (cc_add_term self t2) e
+
+    let cc_raise_conflict_expl self acts e =
+      let cc_acts = mk_cc_acts_ self.proof acts in
+      CC.raise_conflict_from_expl (cc self) cc_acts e
+      *)
+
+(** {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 =
+  self.level <- 1 + self.level;
+  CC.push_level (cc self);
+  push_lvl_ self.th_states
+
+let pop_levels (self : t) n : unit =
+  self.last_model <- None;
+  self.level <- self.level - n;
+  CC.pop_levels (cc self) n;
+  pop_lvls_ n self.th_states
+
+let n_levels self = self.level
+
+(** {2 Model construction and theory combination} *)
+
+(* make model from the congruence closure *)
+let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
+  Log.debug 1 "(smt.solver.mk-model)";
+  Profile.with_ "smt-solver.mk-model" @@ fun () ->
+  let module M = Term.Tbl in
+  let { cc; tst; model_ask = model_ask_hooks; model_complete; _ } = self in
+
+  let model = M.create 128 in
+
+  (* first, add all literals to the model using the given propositional model
+     [lits]. *)
+  lits (fun lit ->
+      let t, sign = Lit.signed_term lit in
+      M.replace model t (Term.bool_val tst sign));
+
+  (* populate with information from the CC *)
+  (* FIXME
+     CC.get_model_for_each_class cc (fun (_, ts, v) ->
+         Iter.iter
+           (fun n ->
+             let t = N.term n in
+             M.replace model t v)
+           ts);
+  *)
+
+  (* complete model with theory specific values *)
+  let complete_with f =
+    f self ~add:(fun t u ->
+        if not (M.mem model t) then (
+          Log.debugf 20 (fun k ->
+              k "(@[smt.model-complete@ %a@ :with-val %a@])" Term.pp_debug t
+                Term.pp_debug u);
+          M.replace model t u
+        ))
+  in
+  List.iter complete_with model_complete;
+
+  (* compute a value for [n]. *)
+  let rec val_for_class (n : N.t) : term =
+    Log.debugf 5 (fun k -> k "val-for-term %a" N.pp n);
+    let repr = CC.find cc n in
+    Log.debugf 5 (fun k -> k "val-for-term.repr %a" N.pp repr);
+
+    (* see if a value is found already (always the case if it's a boolean) *)
+    match M.get model (N.term repr) with
+    | Some t_val ->
+      Log.debugf 5 (fun k -> k "cached val is %a" Term.pp_debug t_val);
+      t_val
+    | None ->
+      (* try each model hook *)
+      let rec try_hooks_ = function
+        | [] -> N.term repr
+        | h :: hooks ->
+          (match h ~recurse:(fun _ n -> val_for_class n) self repr with
+          | None -> try_hooks_ hooks
+          | Some t -> t)
+      in
+
+      let t_val =
+        try_hooks_ model_ask_hooks
+        (* FIXME: the more complete version?
+           match
+             (* look for a value in the model for any term in the class *)
+             N.iter_class repr
+             |> Iter.find_map (fun n -> M.get model (N.term n))
+           with
+           | Some v -> v
+           | None -> try_hooks_ model_ask_hooks
+        *)
+      in
+
+      M.replace model (N.term repr) t_val;
+      (* be sure to cache the value *)
+      Log.debugf 5 (fun k -> k "val is %a" Term.pp_debug t_val);
+      t_val
+  in
+
+  (* map terms of each CC class to the value computed for their class. *)
+  CC.all_classes cc (fun repr ->
+      let t_val = val_for_class repr in
+      (* value for this class *)
+      N.iter_class repr (fun u ->
+          let t_u = N.term u in
+          if (not (N.equal u repr)) && not (Term.equal t_u t_val) then
+            M.replace model t_u t_val));
+  Model.Map model
+
+(* do theory combination using the congruence closure. Each theory
+   can merge classes, *)
+let check_th_combination_ (self : t) (_acts : theory_actions) lits :
+    (Model.t, th_combination_conflict) result =
+  (* FIXME
+
+     (* enter model mode, disabling most of congruence closure *)
+              CC.with_model_mode cc @@ fun () ->
+              let set_val (t, v) : unit =
+                Log.debugf 50 (fun k ->
+                    k "(@[solver.th-comb.cc-set-term-value@ %a@ :val %a@])" Term.pp_debug t
+                      Term.pp_debug v);
+                CC.set_model_value cc t v
+              in
+
+           (* obtain assignments from the hook, and communicate them to the CC *)
+           let add_th_values f : unit =
+             let vals = f self acts in
+             Iter.iter set_val vals
+           in
+        try
+          List.iter add_th_values self.on_th_combination;
+          CC.check cc;
+          let m = mk_model_ self in
+          Ok m
+        with Semantic_conflict c -> Error c
+  *)
+  let m = mk_model_ self lits in
+  Ok m
+
+(* call congruence closure, perform the actions it scheduled *)
+let check_cc_with_acts_ (self : t) (acts : theory_actions) =
+  let (module A) = acts in
+  let cc = cc self in
+  match CC.check cc with
+  | Ok acts ->
+    List.iter
+      (function
+        | CC.Result_action.Act_propagate { lit; reason } ->
+          let reason = Sidekick_sat.Consequence reason in
+          A.propagate lit reason)
+      acts
+  | Error (CC.Result_action.Conflict (lits, pr)) -> A.raise_conflict lits pr
+
+(* handle a literal assumed by the SAT solver *)
+let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t)
+    : unit =
+  Log.debugf 2 (fun k ->
+      k "(@[<hv1>@{<green>smt-solver.assume_lits@}%s[lvl=%d]@ %a@])"
+        (if final then
+          "[final]"
+        else
+          "")
+        self.level
+        (Util.pp_iter ~sep:"; " Lit.pp)
+        lits);
+  (* transmit to CC *)
+  let cc = cc self in
+
+  if not final then CC.assert_lits cc lits;
+  (* transmit to theories. *)
+  check_cc_with_acts_ self acts;
+  if final then (
+    List.iter (fun f -> f self acts lits) self.on_final_check;
+    check_cc_with_acts_ self acts;
+
+    (match check_th_combination_ self acts lits with
+    | Ok m -> self.last_model <- Some m
+    | Error { lits; semantic } ->
+      (* bad model, we add a clause to remove it *)
+      Log.debugf 5 (fun k ->
+          k "(@[solver.th-comb.conflict@ :lits (@[%a@])@ :same-val (@[%a@])@])"
+            (Util.pp_list Lit.pp) lits
+            (Util.pp_list @@ Fmt.Dump.(triple bool Term.pp_debug Term.pp_debug))
+            semantic);
+
+      let c1 = List.rev_map Lit.neg lits in
+      let c2 =
+        semantic
+        |> List.rev_map (fun (sign, t, u) ->
+               let eqn = Term.eq self.tst t u in
+               let lit = Lit.atom ~sign:(not sign) eqn in
+               (* make sure to consider the new lit *)
+               add_lit self acts lit;
+               lit)
+      in
+
+      let c = List.rev_append c1 c2 in
+      let pr = P.add_step self.proof @@ Rule_.lemma_cc (Iter.of_list c) in
+
+      Log.debugf 20 (fun k ->
+          k "(@[solver.th-comb.add-semantic-conflict-clause@ %a@])"
+            (Util.pp_list Lit.pp) c);
+      (* will add a delayed action *)
+      add_clause_temp self acts c pr);
+
+    Perform_delayed_th.top self acts
+  ) else (
+    List.iter (fun f -> f self acts lits) self.on_partial_check;
+    Perform_delayed_th.top self acts
+  );
+  ()
+
+let[@inline] iter_atoms_ (acts : theory_actions) : _ Iter.t =
+ fun f ->
+  let (module A) = acts in
+  A.iter_assumptions f
+
+(* propagation from the bool solver *)
+let check_ ~final (self : t) (acts : sat_acts) =
+  let pb =
+    if final then
+      Profile.begin_ "solver.final-check"
+    else
+      Profile.null_probe
+  in
+  let iter = iter_atoms_ acts in
+  Log.debugf 5 (fun k -> k "(smt-solver.assume :len %d)" (Iter.length iter));
+  self.on_progress ();
+  assert_lits_ ~final self acts iter;
+  Profile.exit pb
+
+(* propagation from the bool solver *)
+let[@inline] partial_check (self : t) (acts : Sidekick_sat.acts) : unit =
+  check_ ~final:false self acts
+
+(* perform final check of the model *)
+let[@inline] final_check (self : t) (acts : Sidekick_sat.acts) : unit =
+  check_ ~final:true self acts
+
+let declare_pb_is_incomplete self =
+  if self.complete then Log.debug 1 "(solver.declare-pb-is-incomplete)";
+  self.complete <- false
+
+let add_theory_state ~st ~push_level ~pop_levels (self : t) =
+  self.th_states <-
+    Ths_cons { st; push_level; pop_levels; next = self.th_states }
+
+let create (module A : ARG) ~stat ~proof (tst : Term.store) () : t =
+  let self =
+    {
+      tst;
+      cc = CC.create (module A : CC.ARG) ~size:`Big tst proof;
+      proof;
+      th_states = Ths_nil;
+      stat;
+      simp = Simplify.create tst ~proof;
+      last_model = None;
+      on_progress = (fun () -> ());
+      preprocess = [];
+      model_ask = [];
+      model_complete = [];
+      registry = Registry.create ();
+      preprocessed = Term.Tbl.create 32;
+      delayed_actions = Queue.create ();
+      count_axiom = Stat.mk_int stat "solver.th-axioms";
+      count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause";
+      count_propagate = Stat.mk_int stat "solver.th-propagations";
+      count_conflict = Stat.mk_int stat "solver.th-conflicts";
+      on_partial_check = [];
+      on_final_check = [];
+      on_th_combination = [];
+      level = 0;
+      complete = true;
+    }
+  in
+  self

src/smt/solver_internal.mli

@@ -0,0 +1,256 @@
+(** A view of the solver from a theory's point of view.
+
+    Theories should interact with the solver via this module, to assert
+    new lemmas, propagate literals, access the congruence closure, etc. *)
+
+open Sigs
+
+type t
+(** Main type for the SMT solver *)
+
+type solver = t
+
+val tst : t -> term_store
+val stats : t -> Stat.t
+
+val proof : t -> proof_trace
+(** Access the proof object *)
+
+val registry : t -> Registry.t
+(** A solver contains a registry so that theories can share data *)
+
+(** {3 Actions for the theories} *)
+
+type theory_actions
+(** Handle that the theories can use to perform actions. *)
+
+(** {3 Congruence Closure} *)
+
+val cc : t -> CC.t
+(** Congruence closure for this solver *)
+
+(** {3 Backtracking} *)
+
+include Sidekick_sigs.BACKTRACKABLE0 with type t := t
+
+(** {3 Interface to SAT} *)
+
+include Sidekick_sat.PLUGIN_CDCL_T with type t := t
+
+(** {3 Simplifiers} *)
+
+type simplify_hook = Simplify.hook
+
+val add_simplifier : t -> Simplify.hook -> unit
+(** Add a simplifier hook for preprocessing. *)
+
+val simplify_t : t -> term -> (term * step_id) option
+(** Simplify input term, returns [Some u] if some
+      simplification occurred. *)
+
+val simp_t : t -> term -> term * step_id option
+(** [simp_t si t] returns [u] even if no simplification occurred
+      (in which case [t == u] syntactically).
+      It emits [|- t=u].
+      (see {!simplifier}) *)
+
+(** {3 Preprocessors}
+      These preprocessors turn mixed, raw literals (possibly simplified) into
+      literals suitable for reasoning.
+      Typically some clauses are also added to the solver. *)
+
+(* TODO: move into its own sig + library *)
+module type PREPROCESS_ACTS = sig
+  val proof : proof_trace
+
+  val mk_lit : ?sign:bool -> term -> lit
+  (** [mk_lit t] creates a new literal for a boolean term [t]. *)
+
+  val add_clause : lit list -> step_id -> unit
+  (** pushes a new clause into the SAT solver. *)
+
+  val add_lit : ?default_pol:bool -> lit -> unit
+  (** Ensure the literal will be decided/handled by the SAT solver. *)
+end
+
+type preprocess_actions = (module PREPROCESS_ACTS)
+(** Actions available to the preprocessor *)
+
+type preprocess_hook = t -> preprocess_actions -> term -> unit
+(** Given a term, preprocess it.
+
+      The idea is to add literals and clauses to help define the meaning of
+      the term, if needed. For example for boolean formulas, clauses
+      for their Tseitin encoding can be added, with the formula acting
+      as its own proxy symbol.
+
+      @param preprocess_actions actions available during preprocessing.
+  *)
+
+val on_preprocess : t -> preprocess_hook -> unit
+(** Add a hook that will be called when terms are preprocessed *)
+
+(** {3 hooks for the theory} *)
+
+val raise_conflict : t -> theory_actions -> lit list -> step_id -> 'a
+(** Give a conflict clause to the solver *)
+
+val push_decision : t -> theory_actions -> lit -> unit
+(** Ask the SAT solver to decide the given literal in an extension of the
+      current trail. This is useful for theory combination.
+      If the SAT solver backtracks, this (potential) decision is removed
+      and forgotten. *)
+
+val propagate :
+  t -> theory_actions -> lit -> reason:(unit -> lit list * step_id) -> unit
+(** Propagate a boolean using a unit clause.
+      [expl => lit] must be a theory lemma, that is, a T-tautology *)
+
+val propagate_l : t -> theory_actions -> lit -> lit list -> step_id -> unit
+(** Propagate a boolean using a unit clause.
+      [expl => lit] must be a theory lemma, that is, a T-tautology *)
+
+val add_clause_temp : t -> theory_actions -> lit list -> step_id -> unit
+(** Add local clause to the SAT solver. This clause will be
+      removed when the solver backtracks. *)
+
+val add_clause_permanent : t -> theory_actions -> lit list -> step_id -> unit
+(** Add toplevel clause to the SAT solver. This clause will
+      not be backtracked. *)
+
+val mk_lit : t -> ?sign:bool -> term -> lit
+(** Create a literal. This automatically preprocesses the term. *)
+
+val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unit
+(** Add the given literal to the SAT solver, so it gets assigned
+      a boolean value.
+      @param default_pol default polarity for the corresponding atom *)
+
+val add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unit
+(** Add the given (signed) bool term to the SAT solver, so it gets assigned
+      a boolean value *)
+
+val cc_find : t -> E_node.t -> E_node.t
+(** Find representative of the node *)
+
+val cc_are_equal : t -> term -> term -> bool
+(** Are these two terms equal in the congruence closure? *)
+
+val cc_resolve_expl : t -> CC_expl.t -> lit list * step_id
+
+(*
+  val cc_raise_conflict_expl : t -> theory_actions -> CC_expl.t -> 'a
+  (** Raise a conflict with the given congruence closure explanation.
+      it must be a theory tautology that [expl ==> absurd].
+      To be used in theories. *)
+
+  val cc_merge :
+    t -> theory_actions -> E_node.t -> E_node.t -> CC_expl.t -> unit
+  (** Merge these two nodes in the congruence closure, given this explanation.
+      It must be a theory tautology that [expl ==> n1 = n2].
+      To be used in theories. *)
+
+  val cc_merge_t : t -> theory_actions -> term -> term -> CC_expl.t -> unit
+  (** Merge these two terms in the congruence closure, given this explanation.
+      See {!cc_merge} *)
+  *)
+
+val cc_add_term : t -> term -> E_node.t
+(** Add/retrieve congruence closure node for this term.
+      To be used in theories *)
+
+val cc_mem_term : t -> term -> bool
+(** Return [true] if the term is explicitly in the congruence closure.
+      To be used in theories *)
+
+val on_cc_pre_merge :
+  t ->
+  (CC.t * E_node.t * E_node.t * CC_expl.t -> CC.Handler_action.or_conflict) ->
+  unit
+(** Callback for when two classes containing data for this key are merged (called before) *)
+
+val on_cc_post_merge :
+  t -> (CC.t * E_node.t * E_node.t -> CC.Handler_action.t list) -> unit
+(** Callback for when two classes containing data for this key are merged (called after)*)
+
+val on_cc_new_term :
+  t -> (CC.t * E_node.t * term -> CC.Handler_action.t list) -> unit
+(** Callback to add data on terms when they are added to the congruence
+      closure *)
+
+val on_cc_is_subterm :
+  t -> (CC.t * E_node.t * term -> CC.Handler_action.t list) -> unit
+(** Callback for when a term is a subterm of another term in the
+      congruence closure *)
+
+val on_cc_conflict : t -> (CC.ev_on_conflict -> unit) -> unit
+(** Callback called on every CC conflict *)
+
+val on_cc_propagate :
+  t ->
+  (CC.t * lit * (unit -> lit list * step_id) -> CC.Handler_action.t list) ->
+  unit
+(** Callback called on every CC propagation *)
+
+val on_partial_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit
+(** 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 -> theory_actions -> lit Iter.t -> unit) -> unit
+(** Register callback to be called during the final check.
+
+      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.
+  *)
+
+val on_th_combination :
+  t -> (t -> theory_actions -> (term * value) Iter.t) -> unit
+(** Add a hook called during theory combination.
+      The hook must return an iterator of pairs [(t, v)]
+      which mean that term [t] has value [v] in the model.
+
+      Terms with the same value (according to {!Term.equal}) will be
+      merged in the CC; if two terms with different values are merged,
+      we get a semantic conflict and must pick another model. *)
+
+val declare_pb_is_incomplete : t -> unit
+(** Declare that, in some theory, the problem is outside the logic fragment
+      that is decidable (e.g. if we meet proper NIA formulas).
+      The solver will not reply "SAT" from now on. *)
+
+(** {3 Model production} *)
+
+type model_ask_hook =
+  recurse:(t -> E_node.t -> term) -> t -> E_node.t -> term option
+(** A model-production hook to query values from a theory.
+
+      It takes the solver, a class, and returns
+      a term for this class. For example, an arithmetic theory
+      might detect that a class contains a numeric constant, and return
+      this constant as a model value.
+
+      If no hook assigns a value to a class, a fake value is created for it.
+  *)
+
+type model_completion_hook = t -> add:(term -> term -> unit) -> unit
+(** A model production hook, for the theory to add values.
+      The hook is given a [add] function to add bindings to the model. *)
+
+val on_model :
+  ?ask:model_ask_hook -> ?complete:model_completion_hook -> t -> unit
+(** Add model production/completion hooks. *)
+
+val add_theory_state :
+  st:'a ->
+  push_level:('a -> unit) ->
+  pop_levels:('a -> int -> unit) ->
+  t ->
+  unit
+
+val create :
+  (module ARG) -> stat:Stat.t -> proof:Proof_trace.t -> Term.store -> unit -> t

src/smt/th_key.ml.bak

@@ -0,0 +1,145 @@
+  
+
+module type S = sig
+  type ('term,'lit,'a) t
+  (** An access key for theories which have per-class data ['a] *)
+
+  val create :
+    ?pp:'a Fmt.printer ->
+    name:string ->
+    eq:('a -> 'a -> bool) ->
+    merge:('a -> 'a -> 'a) ->
+    unit ->
+    ('term,'lit,'a) t
+  (** Generative creation of keys for the given theory data.
+
+      @param eq : Equality. This is used to optimize backtracking info.
+
+      @param merge :
+        [merge d1 d2] is called when merging classes with data [d1] and [d2]
+        respectively. The theory should already have checked that the merge
+        is compatible, and this produces the combined data  for terms in the
+        merged class.
+      @param name name of the theory which owns this data
+      @param pp a printer for the data
+  *)
+
+  val equal : ('t,'lit,_) t -> ('t,'lit,_) t -> bool
+  (** Checks if two keys are equal (generatively) *)
+
+  val pp : _ t Fmt.printer
+  (** Prints the name of the key. *)
+end
+
+
+(** 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 Key = struct
+  module type KEY_IMPL = sig
+    type term
+    type lit
+    type t
+    val id : int
+    val name : string
+    val pp : t Fmt.printer
+    val equal : t -> t -> bool
+    val merge : t -> t -> t
+    exception Store of t
+  end
+
+  type ('term,'lit,'a) t =
+    (module KEY_IMPL with type term = 'term and type lit = 'lit and type t = 'a)
+
+  let n_ = ref 0
+
+  let create (type term)(type lit)(type d)
+      ?(pp=fun out _ -> Fmt.string out "<opaque>")
+      ~name ~eq ~merge () : (term,lit,d) t =
+    let module K = struct
+      type nonrec term = term
+      type nonrec lit = lit
+      type t = d
+      let id = !n_
+      let name = name
+      let pp = pp
+      let merge = merge
+      let equal = eq
+      exception Store of d
+    end in
+    incr n_;
+    (module K)
+
+  let[@inline] id
+    : type term lit a. (term,lit,a) t -> int
+    = fun (module K) -> K.id
+
+  let[@inline] equal
+    : type term lit a b. (term,lit,a) t -> (term,lit,b) t -> bool
+    = fun (module K1) (module K2) -> K1.id = K2.id
+
+  let pp
+    : type term lit a. (term,lit,a) t Fmt.printer
+    = fun out (module K) -> Fmt.string out K.name
+end
+
+
+
+(*
+  (** Map for theory data associated with representatives *)
+  module K_map = struct
+    type 'a key = (term,lit,'a) Key.t
+    type pair = Pair : 'a key * exn -> pair
+
+    type t = pair IM.t
+
+    let empty = IM.empty
+
+    let[@inline] mem k t = IM.mem (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
+      | Pair (_, 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 (Pair (k, K.Store v)) self
+      
+    let remove (type a) (k: a key) self : t =
+      let (module K) = k in
+      IM.remove K.id self
+
+    let equal (m1:t) (m2:t) : bool =
+      IM.equal
+        (fun p1 p2 ->
+           let Pair ((module K1), v1) = p1 in
+           let Pair ((module K2), v2) = p2 in
+           assert (K1.id = K2.id);
+           match v1, v2 with K1.Store v1, K1.Store v2 -> K1.equal v1 v2 | _ -> false)
+        m1 m2
+
+    let merge ~f_both (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 (Pair ((module K1) as key1, pair1)), Some (Pair (_, pair2)) ->
+             match pair1, pair2 with
+             | K1.Store v1, K1.Store v2 ->
+               f_both K1.id pair1 pair2;  (* callback for checking compat *)
+               let v12 = K1.merge v1 v2 in (* merge content *)
+               Some (Pair (key1, K1.Store v12))
+             | _ -> assert false
+        )
+        m1 m2
+  end
+   *)

src/smt/theory.ml

@@ -0,0 +1,44 @@
+(** Signatures for theory plugins *)
+
+(** A theory
+
+      Theories are abstracted over the concrete implementation of the solver,
+      so they can work with any implementation.
+
+      Typically a theory should be a functor taking an argument containing
+      a [SOLVER_INTERNAL] or even a full [SOLVER],
+      and some additional views on terms, literals, etc.
+      that are specific to the theory (e.g. to map terms to linear
+      expressions).
+      The theory can then be instantiated on any kind of solver for any
+      term representation that also satisfies the additional theory-specific
+      requirements. Instantiated theories (ie values of type {!SOLVER.theory})
+      can be added to the solver.
+  *)
+module type S = 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 t = (module S)
+(** A theory that can be used for this particular solver. *)
+
+type 'a p = (module S with type t = 'a)
+(** A theory that can be used for this particular solver, with state
+      of type ['a]. *)
+
+let make (type st) ~name ~create_and_setup ?(push_level = fun _ -> ())
+    ?(pop_levels = fun _ _ -> ()) () : t =
+  let module Th = struct
+    type t = st
+
+    let name = name
+    let create_and_setup = create_and_setup
+    let push_level = push_level
+    let pop_levels = pop_levels
+  end in
+  (module Th)