diff --git a/src/smt/preprocess.ml b/src/smt/preprocess.ml index a6aa13fb..11aa4b58 100644 --- a/src/smt/preprocess.ml +++ b/src/smt/preprocess.ml @@ -13,31 +13,63 @@ type preprocess_actions = (module PREPROCESS_ACTS) type delayed_action = | DA_add_clause of lit list * step_id | DA_add_lit of { default_pol: bool option; lit: lit } + | DA_declare_need_th_combination of term type t = { tst: Term.store; (** state for managing terms *) + cc: CC.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 claim_hook = Theory_id.t * (t -> term -> bool) -let create ?(stat = Stat.global) ~proof tst : t = +let create ?(stat = Stat.global) ~proof ~cc tst : t = { tst; proof; + cc; 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 preprocess_term_ (self : t) (t0 : term) : unit = +(* find what theory claims [t], unless [t] is boolean. *) +let claimed_by_ (self : t) (t : term) : Theory_id.t option = + let ty_t = Term.ty t in + + if Term.is_bool ty_t then + None + else ( + match + CCList.find_map + (fun (th_id, f) -> + 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 = + Vec.push self.delayed_actions (DA_declare_need_th_combination t) + +let preprocess_term_ (self : t) (t : term) : term = let module A = struct let proof = self.proof let mk_lit ?sign t : Lit.t = Lit.atom ?sign self.tst t @@ -51,38 +83,119 @@ let preprocess_term_ (self : t) (t0 : term) : unit = let acts = (module A : PREPROCESS_ACTS) in (* how to preprocess a term and its subterms *) - let rec preproc_rec_ t : Term.t = - match Term.Tbl.find_opt self.preprocessed t with + let rec preproc_rec_ 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); - (* process sub-terms first *) - let u = Term.map_shallow self.tst t - ~f:(fun _inb u -> preproc_rec_ u); + let claim_t = claimed_by_ self t0 in - Log.debugf 50 (fun k -> k "(@[smt.preprocess@ %a@])" Term.pp_debug t); + (* process sub-terms first, and find out if they are foreign in [t] *) + let t = + Term.map_shallow self.tst t0 ~f:(fun _inb u -> + let u = preproc_rec_ u in + (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 in the SAT solver *) - if Ty.is_bool (Term.ty t) then ( + if Term.is_bool (Term.ty t) then ( Log.debugf 5 (fun k -> - k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp_debug - t); + k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp t); - (* make a literal *) + (* ensure that SAT solver has a boolean atom for [t] *) let lit = Lit.atom self.tst t in - (* ensure that SAT solver has a boolean atom for [u] *) - delayed_add_lit self lit; + A.add_lit 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; - - - Term.Tbl.add self.preprocessed t u; - ) - - List.iter (fun f -> f self acts t) self.preprocess - ) + (* FIXME: use a delayed action "DA_declare_cc_lit (t, lit)" instead *) + CC.set_as_lit self.cc (CC.add_term self.cc t) lit + ); + t in - preproc_rec_ t0 + preproc_rec_ t + +(* simplify literal, then preprocess the result *) +let 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 + | 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 + +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.n_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 + +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 diff --git a/src/smt/preprocess.mli b/src/smt/preprocess.mli index ac29b0fd..119c5c06 100644 --- a/src/smt/preprocess.mli +++ b/src/smt/preprocess.mli @@ -11,7 +11,7 @@ open Sigs type t (** Preprocessor *) -val create : ?stat:Stat.t -> proof:proof_trace -> Term.store -> t +val create : ?stat:Stat.t -> proof:proof_trace -> cc:CC.t -> Term.store -> t (** Actions given to preprocessor hooks *) module type PREPROCESS_ACTS = sig @@ -41,9 +41,22 @@ 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 +(** 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 @@ -54,5 +67,6 @@ val preprocess_clause_array : t -> lit array -> step_id -> lit array * step_id type delayed_action = | DA_add_clause of lit list * step_id | DA_add_lit of { default_pol: bool option; lit: lit } + | DA_declare_need_th_combination of term val pop_delayed_actions : t -> delayed_action Iter.t