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

fix(th-data): need to propagate from is-a eagerly

Browse source 
the final check is too late: we need the info from `is_a c t` to be
fully propagated in the CC before we can run the acyclicity check.
This commit is contained in:
Simon Cruanes 2022-08-19 21:31:27 -04:00
parent 177cd70fac
commit 5fa5fb5bd7
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/th-data/Sidekick_th_data.ml
View file

@ -715,14 +715,17 @@ end = struct
SI.add_clause_permanent solver acts [ Lit.neg l1; Lit.neg l2 ] pr)
)
let on_partial_check self solver acts trail =
Profile.with_ "data.partial-check" @@ fun () ->
check_is_a self solver acts trail;
()
(* on final check, check acyclicity,
then make sure we have done case split on all terms that
need it. *)
let on_final_check (self : t) (solver : SI.t) (acts : SI.theory_actions) trail
=
let on_final_check (self : t) (solver : SI.t) (acts : SI.theory_actions)
_trail =
Profile.with_ "data.final-check" @@ fun () ->
check_is_a self solver acts trail;
(* acyclicity check first *)
Acyclicity_.check self solver acts;
@ -798,6 +801,7 @@ end = struct
SI.on_cc_new_term solver (on_new_term self);
(* 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);
SI.on_final_check solver (on_final_check self);
SI.on_model solver ~ask:(on_model_gen self);
self