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

fix(data): bad explanations in on-new-term rules

Browse source
This commit is contained in:
Simon Cruanes 2021-03-18 12:53:06 -04:00
parent 4eeec5487a
commit b35ca4496f
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -304,7 +304,8 @@ module Make(A : ARG) : S with module A = A = struct
Log.debugf 5
(fun k->k "(@[%s.on-new-term.is-a.reduce@ :t %a@ :to %B@ :n %a@ :sub-cstor %a@])"
name T.pp t is_true N.pp n Monoid_cstor.pp cstor);
SI.CC.merge cc n (SI.CC.n_bool cc is_true) (Expl.mk_theory @@ Expl.mk_merge n_u repr_u)
SI.CC.merge cc n (SI.CC.n_bool cc is_true)
Expl.(mk_theory @@ mk_merge n_u cstor.c_n)
end
| T_select (c_t, i, u) ->
let n_u = SI.CC.add_term cc u in
@ -317,7 +318,7 @@ module Make(A : ARG) : S with module A = A = struct
assert (i < IArray.length cstor.c_args);
let u_i = IArray.get cstor.c_args i in
let n_u_i = SI.CC.add_term cc u_i in
SI.CC.merge cc n n_u_i (Expl.mk_theory @@ Expl.mk_merge n_u repr_u)
SI.CC.merge cc n n_u_i Expl.(mk_theory @@ mk_merge n_u cstor.c_n)
| Some _ -> ()
| None ->
N_tbl.add self.to_decide repr_u (); (* needs to be decided *)