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

fix: do not preprocess but add equations eagerly for single-cstor terms

Browse source
This commit is contained in:
Simon Cruanes 2021-12-17 11:58:39 -05:00
parent 6d72203437
commit 2d24a21908
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -312,7 +312,7 @@ module Make(A : ARG) : S with module A = A = struct
| _, Ty_data {cstors; _} -> | _, Ty_data {cstors; _} ->
begin match Iter.take 2 cstors |> Iter.to_rev_list with begin match Iter.take 2 cstors |> Iter.to_rev_list with
| [cstor] when not (T.Tbl.mem self.single_cstor_preproc_done t) -> | [cstor] when not (T.Tbl.mem self.single_cstor_preproc_done t) ->
(* single cstor: turn [t] into [cstor (sel-c-0 t, …, sel-c n t)] *) (* single cstor: assert [t = cstor (sel-c-0 t, …, sel-c n t)] *)
Log.debugf 50 Log.debugf 50
(fun k->k (fun k->k
"(@[%s.preprocess.single-cstor@ %a@ :ty %a@ :cstor %a@])" "(@[%s.preprocess.single-cstor@ %a@ :ty %a@ :cstor %a@])"
@ -342,10 +342,12 @@ module Make(A : ARG) : S with module A = A = struct
SI.P.proof_r1 pr_isa pr_eq_sel self.proof SI.P.proof_r1 pr_isa pr_eq_sel self.proof
in in
Log.debugf 20 (fun k->k "(@[%s.preproc-into@ %a@ :into %a@])" name T.pp t T.pp u);
T.Tbl.add self.single_cstor_preproc_done t (); (* avoid loops *) T.Tbl.add self.single_cstor_preproc_done t (); (* avoid loops *)
Some (u, Iter.return proof) T.Tbl.add self.case_split_done t (); (* no need to decide *)
Act.add_clause [Act.mk_lit_nopreproc (A.mk_eq self.tst t u)] proof;
None
| _ -> None | _ -> None
end end