Documentation

Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.SatAtBVLogical

This module is the main entry point for reifying BitVec problems with boolean substructure. Given some proof h : exp = true where exp is a BitVec problem with boolean substructure, it returns a SatAtBVLogical, containing the reified version as well as a proof that the reified version must be equal to true.

A reified version of an Expr representing a BVLogicalExpr that we know to be true.

Instances For

    Reify an Expr that is a proof of some boolean structure on top of predicates about BitVecs.

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

      Logical conjunction of two ReifiedBVLogical.

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

        Given a proof that x.expr.Unsat, produce a proof of False.

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