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`

:

```
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?`

.

If solving your problem relies inherently on using associativity or commutativity, consider enabling
the `bv.ac_nf`

option.

Note: `bv_decide`

uses `ofReduceBool`

and thus trusts the correctness of the code generator.

## Equations

- Lean.Parser.Tactic.bvDecide = Lean.ParserDescr.node `Lean.Parser.Tactic.bvDecide 1024 (Lean.ParserDescr.nonReservedSymbol "bv_decide" false)

## Instances For

Suggest a proof script for a `bv_decide`

tactic call. Useful for caching LRAT proofs.

## Equations

- Lean.Parser.Tactic.bvTrace = Lean.ParserDescr.node `Lean.Parser.Tactic.bvTrace 1024 (Lean.ParserDescr.nonReservedSymbol "bv_decide?" false)

## Instances For

Run the normalization procedure of `bv_decide`

only. Sometimes this is enough to solve basic
`BitVec`

goals already.

## Equations

- Lean.Parser.Tactic.bvNormalize = Lean.ParserDescr.node `Lean.Parser.Tactic.bvNormalize 1024 (Lean.ParserDescr.nonReservedSymbol "bv_normalize" false)

## Instances For

Auxiliary attribute for builtin `bv_normalize`

simprocs.

## Equations

- One or more equations did not get rendered due to their size.