Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul

This module contains the implementation of a bitblaster for BitVec.mul. The implemented circuit mirrors the behavior of BitVec.mulRec.

Note that the implementation performs a symbolic branch over the bits of the right hand side. Thus if the right hand side is (partially) known through constant propagation etc. the symbolic branches will be (partially) constant folded away by the AIG optimizer. The preprocessing simp set of bv_decide ensures that constants always end up on the right hand side for this reason.

source
def Std.Tactic.BVDecide.BVExpr.bitblast.blastMul {w : Nat} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (input : aig.BinaryRefVec 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]
    def Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go {w : Nat} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (lhs : aig.RefVec w) (rhs : aig.RefVec w) (curr : Nat) (hcurr : curr ≤ w) (acc : aig.RefVec 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.blastMul.go_le_size {w : Nat} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (curr : Nat) (hcurr : curr ≤ w) (acc : aig.RefVec w) (lhs : aig.RefVec w) (rhs : aig.RefVec w) :
      aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go aig lhs rhs curr hcurr acc).aig.decls.size
      source
      @[irreducible]
      theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go_decl_eq {w : Nat} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (curr : Nat) (hcurr : curr ≤ w) (acc : aig.RefVec w) (lhs : aig.RefVec w) (rhs : aig.RefVec w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go aig lhs rhs curr hcurr acc).aig.decls.size) :
      (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go aig lhs rhs curr hcurr acc).aig.decls[idx] = aig.decls[idx]
      source
      instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBVBitBinaryRefVecBlastMul :
      Std.Sat.AIG.LawfulVecOperator Std.Tactic.BVDecide.BVBit Std.Sat.AIG.BinaryRefVec fun {len : Nat} => Std.Tactic.BVDecide.BVExpr.bitblast.blastMul
      Equations
      • One or more equations did not get rendered due to their size.