Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const

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

@[irreducible]
def Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (val : BitVec w) (curr : Nat) (s : aig.RefVec curr) (hcurr : curr w) :
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[irreducible]
    theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {aig : Std.Sat.AIG α} (curr : Nat) (s : aig.RefVec curr) (val : BitVec w) (hcurr : curr w) :
    aig.decls.size (Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.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 : Std.Sat.AIG α} (i : Nat) (s : aig.RefVec i) (val : BitVec w) (hi : i w) (curr : Nat) (h1 : curr < aig.decls.size) (h2 : curr < (Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go aig val i s hi).aig.decls.size) :
    (Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go aig val i s hi).aig.decls[curr] = aig.decls[curr]
    instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBitVecBlastConst {α : Type} [Hashable α] [DecidableEq α] :
    Std.Sat.AIG.LawfulVecOperator α (fun (x : Std.Sat.AIG α) (w : Nat) => BitVec w) fun {len : Nat} => Std.Tactic.BVDecide.BVExpr.bitblast.blastConst
    Equations
    • =