wip: refactor(preprocess): recursive preprocess guided by theories

src/smt/Sidekick_smt_solver.ml

@@ -14,6 +14,7 @@ module Solver_internal = Solver_internal
 module Solver = Solver
 module Theory = Theory
 module Theory_id = Theory_id
+module Preprocess = Preprocess
 
 type theory = Theory.t
 type solver = Solver.t

src/smt/preprocess.ml

@@ -5,6 +5,7 @@ module type PREPROCESS_ACTS = sig
   val mk_lit : ?sign:bool -> term -> lit
   val add_clause : lit list -> step_id -> unit
   val add_lit : ?default_pol:bool -> lit -> unit
+  val declare_need_th_combination : term -> unit
 end
 
 type preprocess_actions = (module PREPROCESS_ACTS)
@@ -18,52 +19,44 @@ type delayed_action =
 type t = {
   tst: Term.store;  (** state for managing terms *)
   cc: CC.t;
+  simplify: Simplify.t;
   proof: proof_trace;
   mutable preprocess: preprocess_hook list;
-  mutable claim_term: claim_hook list;
   preprocessed: Term.t Term.Tbl.t;
   delayed_actions: delayed_action Vec.t;
   n_preprocess_clause: int Stat.counter;
 }
 
-and preprocess_hook = t -> preprocess_actions -> term -> term option
+and preprocess_hook =
-and claim_hook = Theory_id.t * (t -> term -> bool)
+  t ->
+  is_sub:bool ->
+  recurse:(term -> term) ->
+  preprocess_actions ->
+  term ->
+  term option
 
-let create ?(stat = Stat.global) ~proof ~cc tst : t =
+let create ?(stat = Stat.global) ~proof ~cc ~simplify tst : t =
   {
     tst;
     proof;
     cc;
+    simplify;
     preprocess = [];
-    claim_term = [];
     preprocessed = Term.Tbl.create 8;
     delayed_actions = Vec.create ();
     n_preprocess_clause = Stat.mk_int stat "smt.preprocess.n-clauses";
   }
 
 let on_preprocess self f = self.preprocess <- f :: self.preprocess
-let on_claim self h = self.claim_term <- h :: self.claim_term
+let cc self = self.cc
 
-(* find what theory claims [t], unless [t] is boolean. *)
+let pop_delayed_actions self =
-let claimed_by_ (self : t) (t : term) : Theory_id.t option =
+  if Vec.is_empty self.delayed_actions then
-  let ty_t = Term.ty t in
+    Iter.empty
-
-  if Term.is_bool ty_t then
-    None
   else (
-    match
+    let a = Vec.to_array self.delayed_actions in
-      CCList.find_map
+    Vec.clear self.delayed_actions;
-        (fun (th_id, f) ->
+    Iter.of_array a
-          if f self t then
-            Some th_id
-          else
-            None)
-        self.claim_term
-    with
-    | Some _ as r -> r
-    | None ->
-      Error.errorf "no theory claimed term@ `%a`@ of type `%a`" Term.pp t
-        Term.pp ty_t
   )
 
 let declare_need_th_combination (self : t) (t : term) : unit =
@@ -79,39 +72,45 @@ let preprocess_term_ (self : t) (t : term) : term =
 
     let add_clause c pr : unit =
       Vec.push self.delayed_actions (DA_add_clause (c, pr))
+
+    let declare_need_th_combination t = declare_need_th_combination self t
   end in
   let acts = (module A : PREPROCESS_ACTS) in
 
   (* how to preprocess a term and its subterms *)
-  let rec preproc_rec_ t0 : Term.t =
+  let rec preproc_rec_ ~is_sub t0 : Term.t =
     match Term.Tbl.find_opt self.preprocessed t0 with
     | Some u -> u
     | None ->
       Log.debugf 50 (fun k -> k "(@[smt.preprocess@ %a@])" Term.pp_debug t0);
 
-      let claim_t = claimed_by_ self t0 in
+      (* try hooks first *)
-
-      (* process sub-terms first, and find out if they are foreign in [t]  *)
       let t =
+        match
+          CCList.find_map
+            (fun f ->
+              f self ~is_sub ~recurse:(preproc_rec_ ~is_sub:true) acts t)
+            self.preprocess
+        with
+        | Some u ->
+          (* preprocess [u], to achieve fixpoint *)
+          preproc_rec_ ~is_sub u
+        | None ->
+          (* just preprocess subterms *)
           Term.map_shallow self.tst t0 ~f:(fun _inb u ->
-            let u = preproc_rec_ u in
+              let u = preproc_rec_ ~is_sub:true u in
+              (* TODO: is it automatically subject to TH combination?
+                    probably not, if hooks let this recurse by default (e.g. UF or data)
+
                  (match claim_t, claimed_by_ self u with
                  | Some th1, Some th2 when not (Theory_id.equal th1 th2) ->
                    (* [u] is foreign *)
                    declare_need_th_combination self u
                  | _ -> ());
+              *)
               u)
       in
 
-      (* try hooks *)
-      let t =
-        match CCList.find_map (fun f -> f self acts t) self.preprocess with
-        | Some u ->
-          (* preprocess [u], to achieve fixpoint *)
-          preproc_rec_ u
-        | None -> t
-      in
-
       Term.Tbl.add self.preprocessed t0 t;
 
       (* signal boolean subterms, so as to decide them
@@ -130,20 +129,17 @@ let preprocess_term_ (self : t) (t : term) : term =
       );
       t
   in
-  preproc_rec_ t
+  preproc_rec_ ~is_sub:false t
 
-(* simplify literal, then preprocess the result *)
+(* preprocess the literal. The result must be logically equivalent;
-let preproc_lit (self : t) (lit : Lit.t) : Lit.t * step_id option =
+   as a rule of thumb, it should be the same term inside except with
+   some [box] added whenever a theory frontier is crossed. *)
+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
 
-  (* FIXME: get a proof in preprocess_term_, to account for rewriting?
-        or perhaps, it should only be allowed to introduce proxies so there is
-        no real proof if we consider proxy definitions to be transparent
-
-
   let u, pr =
-       match simplify_t self t with
+    match Simplify.normalize self.simplify t with
     | None -> t, None
     | Some (u, pr_t_u) ->
       Log.debugf 30 (fun k ->
@@ -151,9 +147,8 @@ let preproc_lit (self : t) (lit : Lit.t) : Lit.t * step_id option =
             Term.pp_debug u);
       u, Some pr_t_u
   in
-  *)
+  let v = preprocess_term_ self u in
-  preprocess_term_ self u;
+  Lit.atom ~sign self.tst v, pr
-  Lit.atom ~sign self.tst u, pr
 
 module type ARR = sig
   type 'a t

src/smt/preprocess.mli

@@ -3,7 +3,8 @@
     The preprocessor turn mixed, raw literals (possibly simplified) into
     literals suitable for reasoning.
     Every literal undergoes preprocessing.
-    Typically some clauses are also added to the solver on the side.
+    Typically some clauses are also added to the solver on the side, and some
+    subterms are found to be foreign variables.
 *)
 
 open Sigs
@@ -11,7 +12,13 @@ open Sigs
 type t
 (** Preprocessor *)
 
-val create : ?stat:Stat.t -> proof:proof_trace -> cc:CC.t -> Term.store -> t
+val create :
+  ?stat:Stat.t ->
+  proof:proof_trace ->
+  cc:CC.t ->
+  simplify:Simplify.t ->
+  Term.store ->
+  t
 
 (** Actions given to preprocessor hooks *)
 module type PREPROCESS_ACTS = sig
@@ -25,12 +32,20 @@ module type PREPROCESS_ACTS = sig
 
   val add_lit : ?default_pol:bool -> lit -> unit
   (** Ensure the literal will be decided/handled by the SAT solver. *)
+
+  val declare_need_th_combination : term -> unit
 end
 
 type preprocess_actions = (module PREPROCESS_ACTS)
 (** Actions available to the preprocessor *)
 
-type preprocess_hook = t -> preprocess_actions -> term -> term option
+type preprocess_hook =
+  t ->
+  is_sub:bool ->
+  recurse:(term -> term) ->
+  preprocess_actions ->
+  term ->
+  term option
 (** Given a term, preprocess it.
 
     The idea is to add literals and clauses to help define the meaning of
@@ -41,24 +56,13 @@ type preprocess_hook = t -> preprocess_actions -> term -> term option
     @param preprocess_actions actions available during preprocessing.
 *)
 
-type claim_hook = Theory_id.t * (t -> term -> bool)
-(** A claim hook is theory id, and a function that that theory registed.
-
-    For a hook [(th_id, f)], if [f preproc t] returns [true] it means that
-    the theory [th_id] claims ownership of the term [t]. Typically that occurs
-    because of the sort of [t] (e.g. LRA will claim terms of type ℚ).
-
-    Theories must not claim terms of type [Bool].
-  *)
-
 val on_preprocess : t -> preprocess_hook -> unit
 (** Add a hook that will be called when terms are preprocessed *)
 
-val on_claim : t -> claim_hook -> unit
+val simplify_and_preproc_lit : t -> lit -> lit * step_id option
-(** Add a hook to decide whether a term is claimed by a theory *)
-
 val preprocess_clause : t -> lit list -> step_id -> lit list * step_id
 val preprocess_clause_array : t -> lit array -> step_id -> lit array * step_id
+val cc : t -> CC.t
 
 (** {2 Delayed actions} *)
 

src/smt/solver_internal.ml

@@ -16,14 +16,9 @@ type sat_acts = Sidekick_sat.acts
 type theory_actions = sat_acts
 type simplify_hook = Simplify.hook
 
-module type PREPROCESS_ACTS = sig
+module type PREPROCESS_ACTS = Preprocess.PREPROCESS_ACTS
-  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)
+type preprocess_actions = Preprocess.preprocess_actions
 
 module Registry = Registry
 
@@ -33,6 +28,14 @@ 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 preprocess_hook =
+  Preprocess.t ->
+  is_sub:bool ->
+  recurse:(term -> term) ->
+  preprocess_actions ->
+  term ->
+  term option
+
 type t = {
   tst: Term.store;  (** state for managing terms *)
   cc: CC.t;  (** congruence closure *)
@@ -44,11 +47,10 @@ type t = {
   th_comb: Th_combination.t;
   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 preprocess: preprocess_hook list;
+  preprocess: Preprocess.t;
   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 *)
@@ -56,13 +58,10 @@ type t = {
   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 =
   t -> Model_builder.t -> Term.t -> (value * Term.t list) option
 
@@ -83,10 +82,7 @@ let add_simplifier (self : t) f : unit = Simplify.add_hook self.simp f
 let[@inline] has_delayed_actions self =
   not (Queue.is_empty self.delayed_actions)
 
-let on_preprocess self f = self.preprocess <- f :: self.preprocess
+let on_preprocess self f = Preprocess.on_preprocess self.preprocess f
-
-let claim_sort self ~th_id ~ty =
-  Th_combination.claim_sort self.th_comb ~th_id ~ty
 
 let on_model ?ask ?complete self =
   Option.iter (fun f -> self.model_ask <- f :: self.model_ask) ask;
@@ -125,125 +121,13 @@ let delayed_add_lit (self : t) ?default_pol (lit : Lit.t) : unit =
 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 self.tst 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 ();
-
-      (* see if this is a new type *)
-      let ty = Term.ty t in
-      if not (Term.Weak_set.mem self.seen_types ty) then (
-        Log.debugf 5 (fun k -> k "(@[solver.seen-new-type@ %a@])" Term.pp ty);
-        Term.Weak_set.add self.seen_types ty;
-        Event.Emitter.emit self.on_new_ty ty
-      );
-
-      (* 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 self.tst 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 self.tst 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 lit, _ = Preprocess.simplify_and_preproc_lit self.preprocess 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_list : 'a t -> 'a list
-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;
-        Proof_trace.add_step self.proof @@ fun () ->
-        Proof_core.lemma_rw_clause pr_c ~res:(A.to_list c') ~using:!steps
-      )
-    in
-    c', pr_c'
-end
-[@@inline]
-
-module PC_list = Preprocess_clause (struct
-  type 'a t = 'a list
-
-  let map = CCList.map
-  let to_list l = l
-end)
-
-module PC_arr = Preprocess_clause (CCArray)
-
-let preprocess_clause = PC_list.top
-let preprocess_clause_array = PC_arr.top
-
 module type PERFORM_ACTS = sig
   type t
 
@@ -258,10 +142,10 @@ module Perform_delayed (A : PERFORM_ACTS) = struct
       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
+        let c', pr_c' = Preprocess.preprocess_clause self.preprocess 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);
+        let lit, _ = Preprocess.simplify_and_preproc_lit self.preprocess lit in
         A.add_lit self acts ?default_pol lit
     done
 end
@@ -277,12 +161,23 @@ module Perform_delayed_th = Perform_delayed (struct
     add_sat_lit_ self acts ?default_pol lit
 end)
 
+let[@inline] preprocess self = self.preprocess
+
+let preprocess_clause self c pr =
+  Preprocess.preprocess_clause self.preprocess c pr
+
+let preprocess_clause_array self c pr =
+  Preprocess.preprocess_clause_array self.preprocess c pr
+
+let simplify_and_preproc_lit self lit =
+  Preprocess.simplify_and_preproc_lit self.preprocess lit
+
 let[@inline] add_clause_temp self _acts c (proof : step_id) : unit =
-  let c, proof = preprocess_clause self c proof in
+  let c, proof = Preprocess.preprocess_clause self.preprocess 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
+  let c, proof = Preprocess.preprocess_clause self.preprocess c proof in
   delayed_add_clause self ~keep:true c proof
 
 let[@inline] mk_lit self ?sign t : lit = Lit.atom ?sign self.tst t
@@ -298,7 +193,7 @@ let[@inline] add_lit self _acts ?default_pol lit =
 
 let add_lit_t self _acts ?sign t =
   let lit = Lit.atom ?sign self.tst t in
-  let lit, _ = simplify_and_preproc_lit self lit in
+  let lit, _ = Preprocess.simplify_and_preproc_lit self.preprocess lit in
   delayed_add_lit self lit
 
 let on_final_check self f = self.on_final_check <- f :: self.on_final_check
@@ -416,32 +311,6 @@ let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
   compute_fixpoint ();
   MB.to_model model
 
-(* theory combination: find terms occurring as foreign variables in
-   other terms *)
-let theory_comb_register_new_term (self : t) (t : term) : unit =
-  Log.debugf 50 (fun k -> k "(@[solver.th-comb-register@ %a@])" Term.pp t);
-  match Th_combination.claimed_by self.th_comb ~ty:(Term.ty t) with
-  | None -> ()
-  | Some theory_for_t ->
-    let args =
-      let _f, args = Term.unfold_app t in
-      match Term.view _f, args, Term.view t with
-      | Term.E_const { Const.c_ops = (module OP); c_view; _ }, _, _
-        when OP.opaque_to_cc c_view ->
-        []
-      | _, [], Term.E_app_fold { args; _ } -> args
-      | _ -> args
-    in
-    List.iter
-      (fun arg ->
-        match Th_combination.claimed_by self.th_comb ~ty:(Term.ty arg) with
-        | Some theory_for_arg
-          when not (Theory_id.equal theory_for_t theory_for_arg) ->
-          (* [arg] is foreign *)
-          Th_combination.add_term_needing_combination self.th_comb arg
-        | _ -> ())
-      args
-
 (* call congruence closure, perform the actions it scheduled *)
 let check_cc_with_acts_ (self : t) (acts : theory_actions) =
   let (module A) = acts in
@@ -570,27 +439,28 @@ let add_theory_state ~st ~push_level ~pop_levels (self : t) =
     Ths_cons { st; push_level; pop_levels; next = self.th_states }
 
 let create (module A : ARG) ~stat ~proof (tst : Term.store) () : t =
+  let simp = Simplify.create tst ~proof in
+  let cc = CC.create (module A : CC.ARG) ~size:`Big tst proof in
+  let preprocess = Preprocess.create ~stat ~proof ~cc ~simplify:simp tst in
   let self =
     {
       tst;
-      cc = CC.create (module A : CC.ARG) ~size:`Big tst proof;
+      cc;
       proof;
       th_states = Ths_nil;
       stat;
-      simp = Simplify.create tst ~proof;
+      simp;
+      preprocess;
       last_model = None;
       seen_types = Term.Weak_set.create 8;
       th_comb = Th_combination.create ~stat tst;
       on_progress = Event.Emitter.create ();
       on_new_ty = Event.Emitter.create ();
-      preprocess = [];
       model_ask = [];
       model_complete = [];
       registry = Registry.create ();
-      preprocessed = Term.Tbl.create 32;
       delayed_actions = Queue.create ();
       count_axiom = Stat.mk_int stat "smt.solver.th-axioms";
-      count_preprocess_clause = Stat.mk_int stat "smt.solver.preprocess-clause";
       count_propagate = Stat.mk_int stat "smt.solver.th-propagations";
       count_conflict = Stat.mk_int stat "smt.solver.th-conflicts";
       on_partial_check = [];
@@ -599,8 +469,4 @@ let create (module A : ARG) ~stat ~proof (tst : Term.store) () : t =
       complete = true;
     }
   in
-  (* observe new terms in the CC *)
-  on_cc_new_term self (fun (_, _, t) ->
-      theory_comb_register_new_term self t;
-      []);
   self

src/smt/solver_internal.mli

@@ -61,24 +61,18 @@ val simp_t : t -> term -> term * step_id option
       literals suitable for reasoning.
       Typically some clauses are also added to the solver. *)
 
-(* TODO: move into its own sig + library *)
+module type PREPROCESS_ACTS = Preprocess.PREPROCESS_ACTS
-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
+type preprocess_hook =
+  Preprocess.t ->
+  is_sub:bool ->
+  recurse:(term -> term) ->
+  preprocess_actions ->
+  term ->
+  term option
 (** Given a term, preprocess it.
 
       The idea is to add literals and clauses to help define the meaning of
@@ -89,6 +83,8 @@ type preprocess_hook = t -> preprocess_actions -> term -> unit
       @param preprocess_actions actions available during preprocessing.
   *)
 
+val preprocess : t -> Preprocess.t
+
 val on_preprocess : t -> preprocess_hook -> unit
 (** Add a hook that will be called when terms are preprocessed *)
 
@@ -98,11 +94,6 @@ val preprocess_clause_array : t -> lit array -> step_id -> lit array * step_id
 val simplify_and_preproc_lit : t -> lit -> lit * step_id option
 (** Simplify literal then preprocess it *)
 
-val claim_sort : t -> th_id:Theory_id.t -> ty:ty -> unit
-(** Claim a sort, to be called by the theory with id [th_id] which is
-    responsible for this sort in models. This is useful for theory combination.
-    *)
-
 (** {3 hooks for the theory} *)
 
 val raise_conflict : t -> theory_actions -> lit list -> step_id -> 'a

src/smt/th_combination.ml

@@ -3,7 +3,6 @@ module T = Term
 
 type t = {
   tst: Term.store;
-  claims: Theory_id.t T.Tbl.t;  (** type -> theory claiming it *)
   processed: T.Set.t T.Tbl.t;  (** type -> set of terms *)
   unprocessed: T.t Vec.t;
   n_terms: int Stat.counter;
@@ -13,7 +12,6 @@ type t = {
 let create ?(stat = Stat.global) tst : t =
   {
     tst;
-    claims = T.Tbl.create 8;
     processed = T.Tbl.create 8;
     unprocessed = Vec.create ();
     n_terms = Stat.mk_int stat "smt.thcomb.terms";
@@ -61,18 +59,3 @@ let pop_new_lits (self : t) : Lit.t list =
   done;
 
   !lits
-
-let claim_sort (self : t) ~th_id ~ty : unit =
-  match T.Tbl.find_opt self.claims ty with
-  | Some id' ->
-    if not (Theory_id.equal th_id id') then
-      Error.errorf "Type %a is claimed by two distinct theories" Term.pp ty
-  | None when T.is_bool ty -> Error.errorf "Cannot claim type Bool"
-  | None ->
-    Log.debugf 3 (fun k ->
-        k "(@[th-comb.claim-ty@ :th-id %a@ :ty %a@])" Theory_id.pp th_id Term.pp
-          ty);
-    T.Tbl.add self.claims ty th_id
-
-let[@inline] claimed_by (self : t) ~ty : _ option =
-  T.Tbl.find_opt self.claims ty

src/smt/th_combination.mli

@@ -6,14 +6,6 @@ type t
 
 val create : ?stat:Stat.t -> Term.store -> t
 
-val claim_sort : t -> th_id:Theory_id.t -> ty:Term.t -> unit
-(** [claim_sort ~th_id ~ty] means that type [ty] is handled by
-    theory [th_id]. A foreign term is a term handled by theory [T1] but
-    which occurs inside a term handled by theory [T2 != T1] *)
-
-val claimed_by : t -> ty:Term.t -> Theory_id.t option
-(** Find what theory claimed this type, if any *)
-
 val add_term_needing_combination : t -> Term.t -> unit
 (** [add_term_needing_combination self t] means that [t] occurs as a foreign
   variable in another term, so it is important that its theory, and the

src/th-bool-dyn/Sidekick_th_bool_dyn.ml

@@ -167,25 +167,27 @@ end = struct
     )
 
   (* preprocess. *)
-  let preprocess_ (self : state) (_si : SI.t) (module PA : SI.PREPROCESS_ACTS)
+  let preprocess_ (self : state) (_p : SMT.Preprocess.t) ~is_sub:_ ~recurse:_
-      (t : T.t) : unit =
+      (module PA : SI.PREPROCESS_ACTS) (t : T.t) : T.t option =
-    Log.debugf 50 (fun k -> k "(@[th-bool.dny.preprocess@ %a@])" T.pp_debug t);
+    Log.debugf 50 (fun k -> k "(@[th-bool.dyn.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
+    match A.view_as_bool t with
     | B_ite (a, b, c) ->
+      let box_t = Box.box self.tst t in
       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) ]
+        [ Lit.neg lit_a; PA.mk_lit (eq self.tst box_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) ]
+        [ lit_a; PA.mk_lit (eq self.tst box_t c) ]
-        (mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t)
+        (mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t);
-    | _ -> ());
+
-    ()
+      Some box_t
+    | _ -> None
 
   let tseitin ~final:_ (self : state) solver (acts : SI.theory_actions)
       (lit : Lit.t) (t : term) (v : term bool_view) : unit =

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -158,13 +158,13 @@ end = struct
     proxy, mk_lit proxy
 
   (* TODO: polarity? *)
-  let cnf (self : state) (si : SI.t) (module PA : SI.PREPROCESS_ACTS) (t : T.t)
+  let cnf (self : state) (_preproc : SMT.Preprocess.t) ~is_sub:_ ~recurse
-      : unit =
+      (module PA : SI.PREPROCESS_ACTS) (t : T.t) : T.t option =
     Log.debugf 50 (fun k -> k "(@[th-bool.cnf@ %a@])" T.pp_debug t);
     let[@inline] mk_step_ r = Proof_trace.add_step PA.proof r in
 
     (* handle boolean equality *)
-    let equiv_ (self : state) _si ~is_xor ~t t_a t_b : unit =
+    let equiv_ (self : state) ~is_xor ~t t_a t_b : unit =
       let a = PA.mk_lit t_a in
       let b = PA.mk_lit t_b in
       let a =
@@ -210,11 +210,12 @@ end = struct
           mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-i-" [ t ])
     in
 
-    (match A.view_as_bool t with
+    match A.view_as_bool t with
-    | B_bool _ -> ()
+    | B_bool _ | B_not _ -> None
-    | B_not _ -> ()
     | B_and l ->
-      let lit = PA.mk_lit t in
+      let box_t = Box.box self.tst t in
+      let l = CCList.map recurse l in
+      let lit = PA.mk_lit box_t in
       let subs = List.map PA.mk_lit l in
 
       (* add clauses *)
@@ -230,10 +231,13 @@ end = struct
       Stat.incr self.n_clauses;
       PA.add_clause
         (lit :: List.map Lit.neg subs)
-        (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-i" [ t ])
+        (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-i" [ t ]);
+      Some box_t
     | B_or l ->
+      let box_t = Box.box self.tst t in
+      let l = CCList.map recurse l in
       let subs = List.map PA.mk_lit l in
-      let lit = PA.mk_lit t in
+      let lit = PA.mk_lit box_t in
 
       (* add clauses *)
       List.iter
@@ -247,11 +251,13 @@ end = struct
 
       Stat.incr self.n_clauses;
       PA.add_clause (Lit.neg lit :: subs)
-        (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "or-e" [ t ])
+        (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "or-e" [ t ]);
+      Some box_t
     | B_imply (a, b) ->
       (* transform into [¬a \/ b] on the fly *)
-      let n_a = PA.mk_lit ~sign:false a in
+      let box_t = Box.box self.tst t in
-      let b = PA.mk_lit b in
+      let n_a = PA.mk_lit ~sign:false @@ recurse a in
+      let b = PA.mk_lit @@ recurse b in
       let subs = [ n_a; b ] in
 
       (* now the or-encoding *)
@@ -269,23 +275,35 @@ end = struct
 
       Stat.incr self.n_clauses;
       PA.add_clause (Lit.neg lit :: subs)
-        (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "imp-e" [ t ])
+        (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "imp-e" [ t ]);
+
+      Some box_t
     | B_ite (a, b, c) ->
+      let box_t = Box.box self.tst t in
+      let a = recurse a in
+      let b = recurse b in
+      let c = recurse c in
+
       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) ]
+        [ Lit.neg lit_a; PA.mk_lit (eq self.tst box_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) ]
+        [ lit_a; PA.mk_lit (eq self.tst box_t c) ]
-        (mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t)
+        (mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t);
-    | B_eq _ | B_neq _ -> ()
+
-    | B_equiv (a, b) -> equiv_ self si ~t ~is_xor:false a b
+      Some box_t
-    | B_xor (a, b) -> equiv_ self si ~t ~is_xor:true a b
+    | B_eq _ | B_neq _ -> None
-    | B_atom _ -> ());
+    | B_equiv (a, b) ->
-    ()
+      equiv_ self ~t ~is_xor:false a b;
+      None (* FIXME *)
+    | B_xor (a, b) ->
+      equiv_ self ~t ~is_xor:true a b;
+      None (* FIXME *)
+    | B_atom _ -> None
 
   let create_and_setup ~id:_ si =
     Log.debug 2 "(th-bool.setup)";

src/th-data/Sidekick_th_data.ml

@@ -327,11 +327,11 @@ end = struct
     | Ty_data _ -> true
     | _ -> false
 
-  let preprocess (self : t) _si (acts : SI.preprocess_actions) (t : Term.t) :
+  let preprocess (self : t) _p ~is_sub:_ ~recurse:_
-      unit =
+      (acts : SI.preprocess_actions) (t : Term.t) : Term.t option =
     let ty = Term.ty t in
     match A.view_as_data t, A.as_datatype ty with
-    | T_cstor _, _ -> ()
+    | T_cstor _, _ -> None
     | _, Ty_data { cstors; _ } ->
       (match cstors with
       | [ cstor ] when not (Term.Tbl.mem self.single_cstor_preproc_done t) ->
@@ -370,9 +370,11 @@ end = struct
         Term.Tbl.add self.case_split_done t ();
 
         (* no need to decide *)
-        Act.add_clause [ Act.mk_lit (A.mk_eq self.tst t u) ] proof
+        Act.add_clause [ Act.mk_lit (A.mk_eq self.tst t u) ] proof;
-      | _ -> ())
+
-    | _ -> ()
+        None
+      | _ -> None)
+    | _ -> None
 
   (* find if we need to split [t] based on its type (if it's
      a finite datatype) *)
@@ -464,11 +466,6 @@ end = struct
         [])
     | T_cstor _ | T_other _ -> []
 
-  let on_is_subterm (self : t) (si : SI.t) (_cc, _repr, t) : _ list =
-    if is_data_ty (Term.ty t) then
-      SI.claim_sort si ~th_id:self.th_id ~ty:(Term.ty t);
-    []
-
   let cstors_of_ty (ty : ty) : A.Cstor.t list =
     match A.as_datatype ty with
     | Ty_data { cstors } -> cstors
@@ -811,7 +808,6 @@ end = struct
     Log.debugf 1 (fun k -> k "(setup :%s)" name);
     SI.on_preprocess solver (preprocess self);
     SI.on_cc_new_term solver (on_new_term self);
-    SI.on_cc_is_subterm solver (on_is_subterm self solver);
     (* note: this needs to happen before we modify the plugin data *)
     SI.on_cc_pre_merge solver (on_pre_merge self);
     SI.on_partial_check solver (on_partial_check self);

src/th-lra/sidekick_th_lra.ml

@@ -124,17 +124,16 @@ module Make (A : ARG) = (* : S with module A = A *) struct
   module ST_exprs = Sidekick_cc.Plugin.Make (Monoid_exprs)
 
   type state = {
-    th_id: Sidekick_smt_solver.Theory_id.t;
     tst: Term.store;
     proof: Proof_trace.t;
     gensym: Gensym.t;
     in_model: unit Term.Tbl.t; (* terms to add to model *)
     encoded_eqs: unit Term.Tbl.t;
     (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *)
-    encoded_lits: Lit.t Term.Tbl.t;  (** [t => lit for t], using gensym *)
+    encoded_lits: Term.t Term.Tbl.t;  (** [t => lit for t], using gensym *)
     simp_preds: (Term.t * S_op.t * A.Q.t) Term.Tbl.t;
     (* term -> its simplex meaning *)
-    simp_defined: LE.t Term.Tbl.t;
+    simp_defined: (Term.t * LE.t) Term.Tbl.t;
     (* (rational) terms that are equal to a linexp *)
     st_exprs: ST_exprs.t;
     mutable encoded_le: Term.t Comb_map.t; (* [le] -> var encoding [le] *)
@@ -144,12 +143,11 @@ module Make (A : ARG) = (* : S with module A = A *) struct
     n_conflict: int Stat.counter;
   }
 
-  let create ~th_id (si : SI.t) : state =
+  let create (si : SI.t) : state =
     let stat = SI.stats si in
     let proof = SI.proof si in
     let tst = SI.tst si in
     {
-      th_id;
       tst;
       proof;
       in_model = Term.Tbl.create 8;
@@ -300,21 +298,23 @@ module Make (A : ARG) = (* : S with module A = A *) struct
         proxy, A.Q.one)
 
   (* preprocess linear expressions away *)
-  let preproc_lra (self : state) si (module PA : SI.PREPROCESS_ACTS)
+  let preproc_lra (self : state) _preproc ~is_sub ~recurse
-      (t : Term.t) : unit =
+      (module PA : SI.PREPROCESS_ACTS) (t : Term.t) : Term.t option =
     Log.debugf 50 (fun k -> k "(@[lra.preprocess@ %a@])" Term.pp_debug t);
-    let tst = SI.tst si in
+    let tst = self.tst in
 
     (* tell the CC this term exists *)
     let declare_term_to_cc ~sub:_ t =
       Log.debugf 50 (fun k ->
           k "(@[lra.declare-term-to-cc@ %a@])" Term.pp_debug t);
-      ignore (CC.add_term (SI.cc si) t : E_node.t)
+      ignore (CC.add_term (SMT.Preprocess.cc _preproc) t : E_node.t)
     in
 
     match A.view_as_lra t with
     | _ when Term.Tbl.mem self.simp_preds t ->
-      () (* already turned into a simplex predicate *)
+      let u, _, _ = Term.Tbl.find self.simp_preds t in
+      Some u
+      (* already turned into a simplex predicate *)
     | LRA_pred (((Eq | Neq) as pred), t1, t2) when is_const_ t1 && is_const_ t2
       ->
       (* comparison of constants: can decide right now *)
@@ -323,12 +323,19 @@ module Make (A : ARG) = (* : S with module A = A *) struct
         let is_eq = pred = Eq in
         let t_is_true = is_eq = A.Q.equal n1 n2 in
         let lit = PA.mk_lit ~sign:t_is_true t in
-        add_clause_lra_ (module PA) [ lit ]
+        add_clause_lra_ (module PA) [ lit ];
+        None
       | _ -> assert false)
     | LRA_pred ((Eq | Neq), t1, t2) ->
       (* equality: just punt to [t1 = t2 <=> (t1 <= t2 /\ t1 >= t2)] *)
+      (* TODO: box [t], recurse on [t1 <= t2] and [t1 >= t2],
+         add 3 atomic clauses, return [box t] *)
       let _, t = Term.abs self.tst t in
       if not (Term.Tbl.mem self.encoded_eqs t) then (
+        (* preprocess t1, t2 recursively *)
+        let t1 = recurse t1 in
+        let t2 = recurse t2 in
+
         let u1 = A.mk_lra tst (LRA_pred (Leq, t1, t2)) in
         let u2 = A.mk_lra tst (LRA_pred (Geq, t1, t2)) in
 
@@ -341,10 +348,14 @@ module Make (A : ARG) = (* : S with module A = A *) struct
         add_clause_lra_ (module PA) [ Lit.neg lit_t; lit_u1 ];
         add_clause_lra_ (module PA) [ Lit.neg lit_t; lit_u2 ];
         add_clause_lra_ (module PA) [ Lit.neg lit_u1; Lit.neg lit_u2; lit_t ]
-      )
+      );
+      None
     | LRA_pred _ when Term.Tbl.mem self.encoded_lits t ->
-      (* already encoded *) ()
+      (* already encoded *)
+      let u = Term.Tbl.find self.encoded_lits t in
+      Some u
     | LRA_pred (pred, t1, t2) ->
+      let box_t = Box.box self.tst t in
       let l1 = as_linexp t1 in
       let l2 = as_linexp t2 in
       let le = LE.(l1 - l2) in
@@ -376,19 +387,27 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       let constr = SimpSolver.Constraint.mk v op q in
       SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
       Term.Tbl.add self.simp_preds (Lit.term lit) (v, op, q);
+      Term.Tbl.add self.encoded_lits (Lit.term lit) box_t;
 
       Log.debugf 50 (fun k ->
           k "(@[lra.preproc@ :t %a@ :to-constr %a@])" Term.pp_debug t
-            SimpSolver.Constraint.pp constr)
+            SimpSolver.Constraint.pp constr);
+
+      Some box_t
     | LRA_op _ | LRA_mult _ ->
-      if not (Term.Tbl.mem self.simp_defined t) then (
+      (match Term.Tbl.find_opt self.simp_defined t with
+      | Some (t, _le) -> Some t
+      | None ->
+        let box_t = Box.box self.tst t in
         (* we define these terms so their value in the model make sense *)
         let le = as_linexp t in
-        Term.Tbl.add self.simp_defined t le
+        Term.Tbl.add self.simp_defined t (box_t, le);
-      )
+        Some box_t)
-    | LRA_const _n -> ()
+    | LRA_const _n -> None
-    | LRA_other t when A.has_ty_real t -> ()
+    | LRA_other t when A.has_ty_real t && is_sub ->
-    | LRA_other _ -> ()
+      PA.declare_need_th_combination t;
+      None
+    | LRA_other _ -> None
 
   let simplify (self : state) (_recurse : _) (t : Term.t) :
       (Term.t * Proof_step.id Iter.t) option =
@@ -705,16 +724,15 @@ module Make (A : ARG) = (* : S with module A = A *) struct
 
   let k_state = SMT.Registry.create_key ()
 
-  let create_and_setup ~id si =
+  let create_and_setup ~id:_ si =
     Log.debug 2 "(th-lra.setup)";
-    let st = create ~th_id:id si in
+    let st = create si in
     SMT.Registry.set (SI.registry si) k_state st;
     SI.add_simplifier si (simplify st);
     SI.on_preprocess si (preproc_lra st);
     SI.on_final_check si (final_check_ st);
     (* SI.on_partial_check si (partial_check_ st); *)
     SI.on_model si ~ask:(model_ask_ st) ~complete:(model_complete_ st);
-    SI.claim_sort si ~th_id:id ~ty:(A.ty_real (SI.tst si));
     SI.on_cc_pre_merge si (fun (_cc, n1, n2, expl) ->
         match as_const_ (E_node.term n1), as_const_ (E_node.term n2) with
         | Some q1, Some q2 when A.Q.(q1 <> q2) ->