Documentation

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

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

Instances For
    @[irreducible]
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[irreducible]
      theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go_le_size {w : Nat} {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (curr : Nat) (s : aig.RefVec curr) (a : Nat) (hcurr : curr w) :
      aig.decls.size (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).aig.decls.size
      @[irreducible]
      theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go_decl_eq {w : Nat} {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (curr : Nat) (s : aig.RefVec curr) (a : Nat) (hcurr : curr w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).aig.decls.size) :
      (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).aig.decls[idx] = aig.decls[idx]