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 of blastMul ensures that the value with more known bits 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
    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.
    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) (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) (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
        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