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

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

• start : Nat
• x : aig.RefVec w

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

Extract a single bit in position start in target and extend it to have width w

Equations

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

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

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

• w : Nat
• x : aig.RefVec self.w
• h : outWidth = self.w * self.w

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

Extract one bit at a time from the initial vector, zero-extend it to width w, and append it the result to acc, which eventually will have size outWidth = w * w

Equations

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

@[irreducible]

def Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go {α : Type} [Hashable α] [DecidableEq α] {outWidth : Nat} {aig : Sat.AIG α} {w : Nat} (idx : Nat) (x : aig.RefVec w) (acc : aig.RefVec (w * idx)) (h : idx ≤ w) (h' : outWidth = w * w) : Sat.AIG.RefVecEntry α outWidth

Equations

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

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w outWidth : Nat} (aig : Sat.AIG α) (idx : Nat) (x : aig.RefVec w) (acc : aig.RefVec (w * idx)) (h : idx ≤ w) (h' : outWidth = w * w) : aig.decls.size ≤ (go idx x acc h h').aig.decls.size

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w outWidth : Nat} (aig : Sat.AIG α) (idx' : Nat) (x : aig.RefVec w) (acc : aig.RefVec (w * idx')) (h : idx' ≤ w) (h' : outWidth = w * w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go idx' x acc h h').aig.decls.size) : (go idx' x acc h h').aig.decls[idx] = aig.decls[idx]

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

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

• w : Nat
• len : Nat
• oldLayer : aig.RefVec (self.len * self.w)
• h : outWidth = (self.len + 1) / 2 * self.w
• hlen : 0 < self.len

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

Given a vector of references oldLayer, add the iterNum-th couple of elements and append the result of the addition to newLayer

Equations

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

@[irreducible]

def Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go {α : Type} [Hashable α] [DecidableEq α] {outWidth : Nat} {aig : Sat.AIG α} {w len : Nat} (iterNum : Nat) (oldLayer : aig.RefVec (len * w)) (newLayer : aig.RefVec (iterNum * w)) (hold : 2 * (iterNum - 1) < len) (hout : outWidth = (len + 1) / 2 * w) : Sat.AIG.RefVecEntry α outWidth

Equations

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

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go_le_size {α : Type} [Hashable α] [DecidableEq α] {len w outWidth : Nat} (aig : Sat.AIG α) (iterNum : Nat) (oldLayer : aig.RefVec (len * w)) (newLayer : aig.RefVec (iterNum * w)) (hold : 2 * (iterNum - 1) < len) (hout : outWidth = (len + 1) / 2 * w) : aig.decls.size ≤ (go iterNum oldLayer newLayer hold hout).aig.decls.size

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len w outWidth : Nat} (aig : Sat.AIG α) (iterNum : Nat) (oldLayer : aig.RefVec (len * w)) (newLayer : aig.RefVec (iterNum * w)) (hold : 2 * (iterNum - 1) < len) (hout : outWidth = (len + 1) / 2 * w) (idx : Nat) (h1 : idx < (go iterNum oldLayer newLayer hold hout).aig.decls.size) (h2 : idx < aig.decls.size) : (go iterNum oldLayer newLayer hold hout).aig.decls[idx] = aig.decls[idx]

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

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

• len : Nat
• x : aig.RefVec (self.len * w)
• h : 0 < self.len

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

Construct a parallel-prefix-sum circuit, invoking blastCpopLayer for each layer, until a single addition node is left.

Equations

• Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree aig { len := len, x := x, h := h } = Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go x h

@[irreducible]

def Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {aig : Sat.AIG α} {len : Nat} (x : aig.RefVec (len * w)) (h : 0 < len) : Sat.AIG.RefVecEntry α w

Equations

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

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go_le_size {α : Type} [Hashable α] [DecidableEq α] {len w : Nat} (aig : Sat.AIG α) (oldLayer : aig.RefVec (len * w)) (h : 0 < len) : aig.decls.size ≤ (go oldLayer h).aig.decls.size

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len w : Nat} (aig : Sat.AIG α) (oldLayer : aig.RefVec (len * w)) (h : 0 < len) (idx : Nat) (h1 : idx < (go oldLayer h).aig.decls.size) (h2 : idx < aig.decls.size) : (go oldLayer h).aig.decls[idx] = aig.decls[idx]

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

def Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (x : aig.RefVec w) : Sat.AIG.RefVecEntry α w

Extend all the bits in the input BitVec w x to have width w, then construct the parallel-prefix-sum circuit.

Equations

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

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (input : aig.RefVec w) : aig.decls.size ≤ (blastCpop aig input).aig.decls.size

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (input : aig.RefVec w) (idx : Nat) (h1 : idx < (blastCpop aig input).aig.decls.size) (h2 : idx < aig.decls.size) : (blastCpop aig input).aig.decls[idx] = aig.decls[idx]

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