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