This module contains the implementation of a bitblaster for symbolic BitVec values.

structure Std.Tactic.BVDecide.BVExpr.bitblast.BVVar (width : Nat) : Type

• ident : Nat

def Std.Tactic.BVDecide.BVExpr.bitblast.blastVar {w : Nat} (aig : Sat.AIG BVBit) (var : BVVar w) : Sat.AIG.RefVecEntry BVBit w

Equations

• Std.Tactic.BVDecide.BVExpr.bitblast.blastVar aig var = Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w var.ident 0 (Std.Sat.AIG.RefVec.emptyWithCapacity w) ⋯

@[irreducible]

def Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go (aig : Sat.AIG BVBit) (w a curr : Nat) (s : aig.RefVec curr) (hcurr : curr ≤ w) : Sat.AIG.RefVecEntry BVBit w

Equations

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

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go_le_size {w : Nat} {aig : Sat.AIG BVBit} (curr : Nat) (s : aig.RefVec curr) (a : Nat) (hcurr : curr ≤ w) : aig.decls.size ≤ (go aig w a curr s hcurr).aig.decls.size

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go_decl_eq {w : Nat} {aig : Sat.AIG BVBit} (curr : Nat) (s : aig.RefVec curr) (a : Nat) (hcurr : curr ≤ w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig w a curr s hcurr).aig.decls.size) : (go aig w a curr s hcurr).aig.decls[idx] = aig.decls[idx]

instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBVBitBVVarBlastVar : Sat.AIG.LawfulVecOperator BVBit (fun (x : Sat.AIG BVBit) (w : Nat) => BVVar w) fun {len : Nat} => blastVar