Documentation

Lean.Elab.Tactic.BVDecide.LRAT.Trim

This module implements the LRAT trimming algorithm described in section 4 of "Faster LRAT Checking Than Solving with CaDiCaL" (https://drops.dagstuhl.de/storage/00lipics/lipics-vol271-sat2023/LIPIcs.SAT.2023.21/LIPIcs.SAT.2023.21.pdf).

The context used for trimming LRAT proofs.

Instances For
    • used : ByteArray

      For each proof step i contains at index i - initialId 0 if i is unused, 1 if it is used.

    • mapped : Array Nat

      For each proof step i contains at index i - initialId the step that i maps to in the new proof or 0 if that step is not yet set. Used such that the proof remains a sequence without gaps.

    Instances For
      @[reducible, inline]
      Equations
        Instances For
          @[inline]
          Equations
            Instances For
              @[inline]
              Equations
                Instances For
                  @[inline]
                  Equations
                    Instances For
                      @[inline]
                      Equations
                        Instances For
                          @[inline]
                          Equations
                            Instances For

                              Perform a use-def analysis of LRAT proof steps, starting at the empty clause and working its way up with DFS.

                              Equations
                                Instances For

                                  Map the set of used proof steps to a new LRAT proof that has no holes in the sequence of proof identifiers.

                                  Equations
                                    Instances For

                                      Trim the LRAT proof by removing all steps that are not used in reaching the empty clause conclusion.

                                      Equations
                                        Instances For