Documentation

Lean.Elab.Tactic.BVDecide.Frontend.BVDecide

This module provides the implementation of the bv_decide frontend itself.

source
def Lean.Elab.Tactic.BVDecide.Frontend.reconstructCounterExample (var2Cnf : Std.HashMap Std.Tactic.BVDecide.BVBit Nat) (assignment : Array (Bool × Nat)) (aigSize : Nat) (atomsAssignment : Std.HashMap Nat Lean.Expr) :
Array (Lean.Expr × Std.Tactic.BVDecide.BVExpr.PackedBitVec)

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.
Instances For
    source
    structure Lean.Elab.Tactic.BVDecide.Frontend.UnsatProver.Result :
    Type
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Elab.Tactic.BVDecide.Frontend.UnsatProver :
      Type
      Equations
      Instances For
        source
        def Lean.Elab.Tactic.BVDecide.Frontend.lratBitblaster (cfg : Lean.Elab.Tactic.BVDecide.Frontend.TacticContext) (bv : Std.Tactic.BVDecide.BVLogicalExpr) (atomsAssignment : Std.HashMap Nat Lean.Expr) :
        Lean.MetaM Lean.Elab.Tactic.BVDecide.Frontend.UnsatProver.Result
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Elab.Tactic.BVDecide.Frontend.reflectBV (g : Lean.MVarId) :
          Lean.Elab.Tactic.BVDecide.Frontend.M (Std.Tactic.BVDecide.BVLogicalExpr × (Lean.Expr → Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr))
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Elab.Tactic.BVDecide.Frontend.closeWithBVReflection (g : Lean.MVarId) (unsatProver : Lean.Elab.Tactic.BVDecide.Frontend.UnsatProver) :
            Lean.MetaM Lean.Elab.Tactic.BVDecide.Frontend.LratCert
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lean.Elab.Tactic.BVDecide.Frontend.bvUnsat (g : Lean.MVarId) (cfg : Lean.Elab.Tactic.BVDecide.Frontend.TacticContext) :
              Lean.MetaM Lean.Elab.Tactic.BVDecide.Frontend.LratCert
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                structure Lean.Elab.Tactic.BVDecide.Frontend.Result :
                Type
                Instances For
                  source
                  def Lean.Elab.Tactic.BVDecide.Frontend.bvDecide (g : Lean.MVarId) (cfg : Lean.Elab.Tactic.BVDecide.Frontend.TacticContext) :
                  Lean.MetaM Lean.Elab.Tactic.BVDecide.Frontend.Result
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Lean.Elab.Tactic.BVDecide.Frontend.evalBvTrace :
                    Lean.Elab.Tactic.Tactic
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For