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

refactor(smt-solver): preprocess literals in push_decision

Browse source
This commit is contained in:
Simon Cruanes 2022-02-08 13:13:23 -05:00
parent a81a21c341
commit f268e86100
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 15 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/smt-solver/Sidekick_smt_solver.ml
View file

@ -319,11 +319,6 @@ module Make(A : ARG)
CCOpt.iter (fun f -> self.model_complete <- f :: self.model_complete) complete; CCOpt.iter (fun f -> self.model_complete <- f :: self.model_complete) complete;
() ()
let push_decision (_self:t) (acts:theory_actions) (lit:lit) : unit =
let (module A) = acts in
let sign = Lit.sign lit in
A.add_decision_lit (Lit.abs lit) sign
let[@inline] raise_conflict self (acts:theory_actions) c proof : 'a = let[@inline] raise_conflict self (acts:theory_actions) c proof : 'a =
let (module A) = acts in let (module A) = acts in
Stat.incr self.count_conflict; Stat.incr self.count_conflict;
@ -371,6 +366,10 @@ module Make(A : ARG)
let rec preproc_rec_ t = let rec preproc_rec_ t =
if not (Term.Tbl.mem self.preprocessed t) then ( if not (Term.Tbl.mem self.preprocessed t) then (
Term.Tbl.add self.preprocessed t (); Term.Tbl.add self.preprocessed t ();
(* process sub-terms first *)
Term.iter_shallow self.tst preproc_rec_ t;
Log.debugf 50 (fun k->k "(@[smt.preprocess@ %a@])" Term.pp t); Log.debugf 50 (fun k->k "(@[smt.preprocess@ %a@])" Term.pp t);
(* signal boolean subterms, so as to decide them (* signal boolean subterms, so as to decide them
@ -391,14 +390,12 @@ module Make(A : ARG)
List.iter List.iter
(fun f -> f self acts t) self.preprocess; (fun f -> f self acts t) self.preprocess;
(* process sub-terms *)
Term.iter_shallow self.tst preproc_rec_ t;
) )
in in
preproc_rec_ t0 preproc_rec_ t0
let simplify_lit_ (self:t) (lit:Lit.t) : Lit.t * proof_step option = (* simplify literal, then preprocess the result *)
let simplify_and_preproc_lit_ (self:t) (lit:Lit.t) : Lit.t * proof_step option =
let t = Lit.term lit in let t = Lit.term lit in
let sign = Lit.sign lit in let sign = Lit.sign lit in
let u, pr = match simplify_t self t with let u, pr = match simplify_t self t with
@ -412,6 +409,13 @@ module Make(A : ARG)
preprocess_term_ self u; preprocess_term_ self u;
Lit.atom self.tst ~sign u, pr Lit.atom self.tst ~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 module type ARR = sig
type 'a t type 'a t
val map : ('a -> 'b) -> 'a t -> 'b t val map : ('a -> 'b) -> 'a t -> 'b t
@ -428,7 +432,7 @@ module Make(A : ARG)
(* simplify a literal, then preprocess it *) (* simplify a literal, then preprocess it *)
let[@inline] simp_lit lit = let[@inline] simp_lit lit =
let lit, pr = simplify_lit_ self lit in let lit, pr = simplify_and_preproc_lit_ self lit in
CCOpt.iter (fun pr -> steps := pr :: !steps) pr; CCOpt.iter (fun pr -> steps := pr :: !steps) pr;
lit lit
in in
@ -499,7 +503,7 @@ module Make(A : ARG)
let add_lit_t self _acts ?sign t = let add_lit_t self _acts ?sign t =
let lit = Lit.atom self.tst ?sign t in let lit = Lit.atom self.tst ?sign t in
let lit, _ = simplify_lit_ self lit in let lit, _ = simplify_and_preproc_lit_ self lit in
delayed_add_lit self lit delayed_add_lit self lit
let on_final_check self f = self.on_final_check <- f :: self.on_final_check let on_final_check self f = self.on_final_check <- f :: self.on_final_check