HepLean Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Basic

This module contains basic infrastructure for converting between variable assignments of BVExpr and AIG. This is necessary because BVExpr needs to use a list and indices into said list instead of a function due to the way that it is used in bv_decide.

source
def Std.Tactic.BVDecide.BVExpr.Assignment.toAIGAssignment (assign : Std.Tactic.BVDecide.BVExpr.Assignment) :
Std.Tactic.BVDecide.BVBit → Bool
Equations
  • assign.toAIGAssignment bit = (assign.getD bit.var).bv.getLsbD ↑bit.idx
Instances For
    source
    @[simp]
    theorem Std.Tactic.BVDecide.BVExpr.Assignment.toAIGAssignment_apply (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (bit : Std.Tactic.BVDecide.BVBit) :
    assign.toAIGAssignment bit = (assign.getD bit.var).bv.getLsbD ↑bit.idx