This module contains the implementation of a bitblaster for BitVec.append.

structure Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (combined : Nat) : Type

• lw : Nat
• rw : Nat
• lhs : aig.RefVec self.lw
• rhs : aig.RefVec self.rw
• h : combined = self.rw + self.lw

Instances For

• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorAppendTargetBlastAppend

theorem Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.h {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {combined : Nat} (self : Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig combined) : combined = self.rw + self.lw

def Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend {α : Type} [Hashable α] [DecidableEq α] {newWidth : Nat} (aig : Std.Sat.AIG α) (target : Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig newWidth) : Std.Sat.AIG.RefVecEntry α newWidth

Equations

• Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend aig (Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.mk lhs rhs h) = { aig := aig, vec := ⋯ ▸ rhs.append lhs }

instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorAppendTargetBlastAppend {α : Type} [Hashable α] [DecidableEq α] : Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget fun {len : Nat} => Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend

Equations

• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorAppendTargetBlastAppend = { le_size := ⋯, decl_eq := ⋯ }