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

feat(smt): simplify the final check loop significantly

Browse source
This commit is contained in:
Simon Cruanes 2022-02-17 21:20:43 -05:00
parent da18ba3620
commit 8fb0152754
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 45 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -604,62 +604,47 @@ module Make(A : ARG)
(* transmit to theories. *) (* transmit to theories. *)
CC.check cc acts; CC.check cc acts;
if final then ( if final then (
let continue = ref true in
while !continue do
(* do final checks in a loop *)
let fcheck = ref true in
while !fcheck do
List.iter (fun f -> f self acts lits) self.on_final_check;
if has_delayed_actions self then (
Perform_delayed_th.top self acts;
) else (
fcheck := false
)
done;
CC.check cc acts; List.iter (fun f -> f self acts lits) self.on_final_check;
let more_work_to_do = CC.new_merges cc || has_delayed_actions self in CC.check cc acts;
if not more_work_to_do then ( let new_work = CC.new_merges cc || has_delayed_actions self in
match check_th_combination_ self acts with (* do actual theory combination if nothing changed by pure "final check" *)
| Ok () -> if not new_work then (
continue := false; match check_th_combination_ self acts with
| Ok () -> ()
| Error {lits; semantic} -> | Error {lits; semantic} ->
(* bad model, we add a clause to remove it *) (* bad model, we add a clause to remove it *)
Log.debugf 5 Log.debugf 5
(fun k->k "(@[solver.th-comb.conflict@ :lits (@[%a@])@ \ (fun k->k "(@[solver.th-comb.conflict@ :lits (@[%a@])@ \
:same-val (@[%a@])@])" :same-val (@[%a@])@])"
(Util.pp_list Lit.pp) lits (Util.pp_list Lit.pp) lits
(Util.pp_list @@ Fmt.Dump.(triple bool Term.pp Term.pp)) semantic); (Util.pp_list @@ Fmt.Dump.(triple bool Term.pp Term.pp)) semantic);
let c1 = List.rev_map Lit.neg lits in let c1 = List.rev_map Lit.neg lits in
let c2 = let c2 =
semantic semantic
|> List.rev_map |> List.rev_map
(fun (sign,t,u) -> (fun (sign,t,u) ->
let eqn = A.mk_eq self.tst t u in let eqn = A.mk_eq self.tst t u in
let lit = Lit.atom ~sign:(not sign) self.tst eqn in let lit = Lit.atom ~sign:(not sign) self.tst eqn in
(* make sure to consider the new lit *) (* make sure to consider the new lit *)
add_lit self acts lit; add_lit self acts lit;
lit) lit)
in in
let c = List.rev_append c1 c2 in let c = List.rev_append c1 c2 in
let pr = P.lemma_cc (Iter.of_list c) self.proof in let pr = P.lemma_cc (Iter.of_list c) self.proof in
Log.debugf 20 Log.debugf 20
(fun k->k "(@[solver.th-comb.add-semantic-conflict-clause@ %a@])" (fun k->k "(@[solver.th-comb.add-semantic-conflict-clause@ %a@])"
(Util.pp_list Lit.pp) c); (Util.pp_list Lit.pp) c);
(* will add a delayed action *) (* will add a delayed action *)
add_clause_temp self acts c pr; add_clause_temp self acts c pr;
);
continue := false; (* FIXME *) Perform_delayed_th.top self acts;
);
Perform_delayed_th.top self acts;
(* FIXME: give a chance to the SAT solver to run again? *)
done;
) else ( ) else (
List.iter (fun f -> f self acts lits) self.on_partial_check; List.iter (fun f -> f self acts lits) self.on_partial_check;
Perform_delayed_th.top self acts; Perform_delayed_th.top self acts;
@ -754,10 +739,10 @@ module Make(A : ARG)
| U_asked_to_stop | U_asked_to_stop
let pp out = function let pp out = function
| U_timeout -> Fmt.string out "timeout" | U_timeout -> Fmt.string out {|"timeout"|}
| U_max_depth -> Fmt.string out "max depth reached" | U_max_depth -> Fmt.string out {|"max depth reached"|}
| U_incomplete -> Fmt.string out "incomplete fragment" | U_incomplete -> Fmt.string out {|"incomplete fragment"|}
| U_asked_to_stop -> Fmt.string out "asked to stop by callback" | U_asked_to_stop -> Fmt.string out {|"asked to stop by callback"|}
end [@@ocaml.warning "-37"] end [@@ocaml.warning "-37"]
module Model = struct module Model = struct
@ -944,19 +929,20 @@ module Make(A : ARG)
(* compute a value for [n]. *) (* compute a value for [n]. *)
let rec val_for_class (n:N.t) : term = 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 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) *) (* see if a value is found already (always the case if it's a boolean) *)
match M.get model (N.term repr) with match M.get model (N.term repr) with
| Some t_val -> t_val | Some t_val ->
Log.debugf 5 (fun k->k "cached val is %a" Term.pp t_val);
t_val
| None -> | None ->
(* try each model hook *) (* try each model hook *)
let rec try_hooks_ = function let rec try_hooks_ = function
| [] -> | [] -> N.term repr
let t = N.term repr in
Log.debugf 20 (fun k->k "(@[smt.model.default-to-repr@ %a@])" Term.pp t);
t
| h :: hooks -> | h :: hooks ->
begin match h ~recurse:(fun _ n -> val_for_class n) self.si repr with begin match h ~recurse:(fun _ n -> val_for_class n) self.si repr with
| None -> try_hooks_ hooks | None -> try_hooks_ hooks
@ -975,6 +961,7 @@ module Make(A : ARG)
in in
M.replace model (N.term repr) t_val; (* be sure to cache the value *) 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 t_val);
t_val t_val
in in