Documentation

Lean.Elab.Tactic.BVDecide.Frontend.BVDecide

This module provides the implementation of the bv_decide frontend itself.

Given:

  • var2Cnf: The mapping from AIG to CNF variables.
  • assignments: A model for the CNF as provided by a SAT solver.
  • aigSize: The amount of nodes in the AIG that was used to produce the CNF.
  • atomsAssignment: The mapping of the reflection monad from atom indices to Expr.

Reconstruct bit by bit which value expression must have had which BitVec value and return all expression - pair values.

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

A counter example generated from the bitblaster.

@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.

The result of a spurious counter example diagnosis.

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

Diagnose spurious counter examples, currently this checks:

  • Whether uninterpreted symbols were used
  • Whether all hypotheses which contain any variable that was bitblasted were included
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

The result of calling bv_decide.

  • lratCert : Option LratCert

    If the normalization step was not enough to solve the goal this contains the LRAT proof certificate.

Try to close g using a bitblaster. Return either a CounterExample if one is found or a Result if g is proven.

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

Call bvDecide' and throw a pretty error if a counter example ends up being produced.

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