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 : Sat.AIG BVBit) (var : BVVar w) :
    Sat.AIG.RefVecEntry BVBit w
    Equations
    Instances For
      source
      @[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.
      Instances For
        source
        @[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
        source
        @[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]
        source
        instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBVBitBVVarBlastVar :
        Sat.AIG.LawfulVecOperator BVBit (fun (x : Sat.AIG BVBit) (w : Nat) => BVVar w) fun {len : Nat} => blastVar