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.

def Std.Tactic.BVDecide.BVExpr.Assignment.toAIGAssignment (assign : Assignment) : BVBit → Bool

Equations

• assign.toAIGAssignment bit = (assign.get bit.var).bv.getLsbD ↑bit.idx

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.Assignment.toAIGAssignment_apply (assign : Assignment) (bit : BVBit) : assign.toAIGAssignment bit = (assign.get bit.var).bv.getLsbD ↑bit.idx