Documentation

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

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

source
structure Std.Tactic.BVDecide.BVExpr.bitblast.BVVar (width : Nat) :
Type
Instances For
    source
    def Std.Tactic.BVDecide.BVExpr.bitblast.blastVar {w : Nat} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (var : Std.Tactic.BVDecide.BVExpr.bitblast.BVVar w) :
    Std.Sat.AIG.RefVecEntry Std.Tactic.BVDecide.BVBit w
    Equations
    Instances For
      source
      @[irreducible]
      def Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (w a curr : Nat) (s : aig.RefVec curr) (hcurr : curr ≤ w) :
      Std.Sat.AIG.RefVecEntry Std.Tactic.BVDecide.BVBit w
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[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
        source
        @[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]
        source
        theorem Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBVBitBVVarBlastVar :
        Std.Sat.AIG.LawfulVecOperator Std.Tactic.BVDecide.BVBit (fun (x : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (w : Nat) => Std.Tactic.BVDecide.BVExpr.bitblast.BVVar w) fun {len : Nat} => Std.Tactic.BVDecide.BVExpr.bitblast.blastVar