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

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

Equations

• Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig val = Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go aig val 0 (Std.Sat.AIG.RefVec.emptyWithCapacity w) ⋯

@[irreducible]

def Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (val : BitVec w) (curr : Nat) (s : aig.RefVec curr) (hcurr : curr ≤ w) : Sat.AIG.RefVecEntry α w

Equations

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

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {aig : Sat.AIG α} (curr : Nat) (s : aig.RefVec curr) (val : BitVec w) (hcurr : curr ≤ w) : aig.decls.size ≤ (go aig val curr s hcurr).aig.decls.size

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {aig : Sat.AIG α} (i : Nat) (s : aig.RefVec i) (val : BitVec w) (hi : i ≤ w) (curr : Nat) (h1 : curr < aig.decls.size) (h2 : curr < (go aig val i s hi).aig.decls.size) : (go aig val i s hi).aig.decls[curr] = aig.decls[curr]

instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBitVecBlastConst {α : Type} [Hashable α] [DecidableEq α] : Sat.AIG.LawfulVecOperator α (fun (x : Sat.AIG α) (w : Nat) => BitVec w) fun {len : Nat} => blastConst