Documentation

Std.Tactic.BVDecide.Syntax

This tactic works just like bv_decide but skips calling a SAT solver by using a proof that is already stored on disk. It is called with the name of an LRAT file in the same directory as the current Lean file:

bv_check "proof.lrat"
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Close fixed-width BitVec and Bool goals by obtaining a proof from an external SAT solver and verifying it inside Lean. The solvable goals are currently limited to the Lean equivalent of QF_BV with the following changes:

    • Division and remainder operations are not yet implemented.
    • if-then-else is not yet implemented.
    • BitVec.ofBool is not yet implemented.
    example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
      intros
      bv_decide
    

    If bv_decide encounters an unknown definition it will be treated like an unconstrained BitVec variable. Sometimes this enables solving goals despite not understanding the definition because the precise properties of the definition do not matter in the specific proof.

    If bv_decide fails to close a goal it provides a counter-example, containing assignments for all terms that were considered as variables.

    In order to avoid calling a SAT solver every time, the proof can be cached with bv_decide?.

    Note: bv_decide uses ofReduceBool and thus trusts the correctness of the code generator.

    Equations
    Instances For

      Suggest a proof script for a bv_decide tactic call. Useful for caching LRAT proofs.

      Equations
      Instances For

        Run the normalization procedure of bv_decide only. Sometimes this is enough to solve basic BitVec goals already.

        Equations
        Instances For

          Auxiliary attribute for builtin bv_normalize simprocs.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For