From e9b395b6434f169e13a19198d343fc9e043b2a10 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 28 Nov 2021 16:33:57 -0500 Subject: [PATCH] feat(proof): do not emit trivial clause_rw steps if there is no rewriting going on, we can skip the step. --- src/base/Proof.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/base/Proof.ml b/src/base/Proof.ml index 6e43f353..6d5fcad7 100644 --- a/src/base/Proof.ml +++ b/src/base/Proof.ml @@ -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