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(proof): do not emit trivial clause_rw steps

Browse source 
if there is no rewriting going on, we can skip the step.
This commit is contained in:
Simon Cruanes 2021-11-28 16:33:57 -05:00
parent aad1daa4e4
commit e9b395b643
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/base/Proof.ml
View file

@ -217,11 +217,16 @@ let lemma_cc lits (self:t) =
PS.(Step_view.Step_cc {Step_cc.eqns=lits})
let lemma_rw_clause c ~res ~using (self:t) =
emit_ self @@ fun() ->
let lits = Iter.map (emit_lit_ self) res |> Iter.to_array in
let res = Proof_ser.{Clause.lits} in
let using = Iter.to_array using in
PS.(Step_view.Step_clause_rw {Step_clause_rw.c; res; using})
if enabled self then (
let using = Iter.to_array using in
if Array.length using=0 then c (* useless step *)
else (
emit_ self @@ fun() ->
let lits = Iter.map (emit_lit_ self) res |> Iter.to_array in
let res = Proof_ser.{Clause.lits} in
PS.(Step_view.Step_clause_rw {Step_clause_rw.c; res; using})
)
) else dummy_step
(* TODO *)
let with_defs _ _ (_pr:t) = dummy_step