simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 11:45:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor(preprocess): directly forward preprocess actions to solver

Browse source
This commit is contained in:
Simon Cruanes 2022-09-08 22:05:40 -04:00
parent c9138144f3
commit e94a7bd31c
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 51 additions and 80 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/smt/preprocess.ml
View file

@ -10,12 +10,6 @@ end
type preprocess_actions = (module PREPROCESS_ACTS)
(* action taken later *)
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;
@ -23,7 +17,6 @@ type t = {
proof: proof_trace;
mutable preprocess: preprocess_hook list;
preprocessed: Term.t Term.Tbl.t;
delayed_actions: delayed_action Vec.t;
n_preprocess_clause: int Stat.counter;
}
@ -43,40 +36,14 @@ let create ?(stat = Stat.global) ~proof ~cc ~simplify tst : t =
simplify;
preprocess = [];
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 cc self = self.cc
let pop_delayed_actions self =
if Vec.is_empty self.delayed_actions then
Iter.empty
else (
let a = Vec.to_array self.delayed_actions in
Vec.clear self.delayed_actions;
Iter.of_array a
)
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
let add_lit ?default_pol lit : unit =
Vec.push self.delayed_actions (DA_add_lit { default_pol; lit })
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
let preprocess_term_ (self : t) ((module A : PREPROCESS_ACTS) as acts)
(t : term) : term =
(* how to preprocess a term and its subterms *)
let rec preproc_rec_ ~is_sub t0 : Term.t =
match Term.Tbl.find_opt self.preprocessed t0 with
@ -137,7 +104,8 @@ let preprocess_term_ (self : t) (t : term) : term =
(* preprocess the literal. The result must be logically equivalent;
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 simplify_and_preproc_lit (self : t) acts (lit : Lit.t) :
Lit.t * step_id option =
let t = Lit.term lit in
let sign = Lit.sign lit in
@ -150,7 +118,7 @@ let simplify_and_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
let v = preprocess_term_ self acts u in
Lit.atom ~sign self.tst v, pr
module type ARR = sig
@ -163,12 +131,12 @@ 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 top (self : t) acts (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
let lit, pr = simplify_and_preproc_lit self acts lit in
Option.iter (fun pr -> steps := pr :: !steps) pr;
lit
in

23
src/smt/preprocess.mli
View file

@ -59,18 +59,13 @@ type preprocess_hook =
val on_preprocess : t -> preprocess_hook -> unit
(** Add a hook that will be called when terms are preprocessed *)
val simplify_and_preproc_lit : t -> lit -> lit * step_id option
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 simplify_and_preproc_lit :
t -> preprocess_actions -> lit -> lit * step_id option
val preprocess_clause :
t -> preprocess_actions -> lit list -> step_id -> lit list * step_id
val preprocess_clause_array :
t -> preprocess_actions -> lit array -> step_id -> lit array * step_id
val cc : t -> CC.t
(** {2 Delayed actions} *)
(** Action that preprocess hooks took, but were not effected yet.
The SMT solver itself should obtain these actions and perform them. *)
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

62
src/smt/solver_internal.ml
View file

@ -121,18 +121,24 @@ 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 add_preprocess_delayed_actions (self : t) : unit =
Preprocess.pop_delayed_actions self.preprocess (function
| DA_add_clause (c, pr) -> delayed_add_clause self ~keep:true c pr
| DA_add_lit { default_pol; lit } -> delayed_add_lit self ?default_pol lit
| DA_declare_need_th_combination t ->
Th_combination.add_term_needing_combination self.th_comb t)
let preprocess_acts (self : t) : Preprocess.preprocess_actions =
(module struct
let proof = self.proof
let mk_lit ?sign t : Lit.t = Lit.atom ?sign self.tst t
let add_clause c pr = delayed_add_clause self ~keep:true c pr
let add_lit ?default_pol lit = delayed_add_lit self ?default_pol lit
let declare_need_th_combination t =
Th_combination.add_term_needing_combination self.th_comb t
end)
let push_decision (self : t) (acts : theory_actions) (lit : lit) : unit =
let (module A) = acts in
(* make sure the literal is preprocessed *)
let lit, _ = Preprocess.simplify_and_preproc_lit self.preprocess lit in
add_preprocess_delayed_actions self;
let lit, _ =
Preprocess.simplify_and_preproc_lit self.preprocess (preprocess_acts self)
lit
in
let sign = Lit.sign lit in
A.add_decision_lit (Lit.abs lit) sign
@ -150,12 +156,16 @@ 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.preprocess_clause self.preprocess c pr_c in
add_preprocess_delayed_actions self;
let c', pr_c' =
Preprocess.preprocess_clause self.preprocess (preprocess_acts self) c
pr_c
in
A.add_clause self acts ~keep c' pr_c'
| DA_add_lit { default_pol; lit } ->
let lit, _ = Preprocess.simplify_and_preproc_lit self.preprocess lit in
add_preprocess_delayed_actions self;
let lit, _ =
Preprocess.simplify_and_preproc_lit self.preprocess
(preprocess_acts self) lit
in
A.add_lit self acts ?default_pol lit
done
end
@ -174,28 +184,24 @@ end)
let[@inline] preprocess self = self.preprocess
let preprocess_clause self c pr =
let r = Preprocess.preprocess_clause self.preprocess c pr in
add_preprocess_delayed_actions self;
r
Preprocess.preprocess_clause self.preprocess (preprocess_acts self) c pr
let preprocess_clause_array self c pr =
let r = Preprocess.preprocess_clause_array self.preprocess c pr in
add_preprocess_delayed_actions self;
r
Preprocess.preprocess_clause_array self.preprocess (preprocess_acts self) c pr
let simplify_and_preproc_lit self lit =
let r = Preprocess.simplify_and_preproc_lit self.preprocess lit in
add_preprocess_delayed_actions self;
r
Preprocess.simplify_and_preproc_lit self.preprocess (preprocess_acts self) lit
let[@inline] add_clause_temp self _acts c (proof : step_id) : unit =
let c, proof = Preprocess.preprocess_clause self.preprocess c proof in
add_preprocess_delayed_actions self;
let c, proof =
Preprocess.preprocess_clause self.preprocess (preprocess_acts 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.preprocess_clause self.preprocess c proof in
add_preprocess_delayed_actions self;
let c, proof =
Preprocess.preprocess_clause self.preprocess (preprocess_acts self) 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
@ -211,8 +217,10 @@ 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, _ = Preprocess.simplify_and_preproc_lit self.preprocess lit in
add_preprocess_delayed_actions self;
let lit, _ =
Preprocess.simplify_and_preproc_lit self.preprocess (preprocess_acts self)
lit
in
delayed_add_lit self lit
let on_final_check self f = self.on_final_check <- f :: self.on_final_check