Documentation

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

This module contains the implementation of a bitblaster for BitVec.udiv. The implemented circuit is a shift subtractor.

source
structure Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput {α : Type} [Hashable α] [DecidableEq α] (aig : Sat.AIG α) (len : Nat) :
Type
  • lhs : aig.RefVec len
  • bit : aig.Ref
Instances For
    source
    def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (input : ShiftConcatInput aig w) :
    Sat.AIG.RefVecEntry α w
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.instLawfulVecOperatorShiftConcatInputBlastShiftConcat {α : Type} [Hashable α] [DecidableEq α] :
      Sat.AIG.LawfulVecOperator α ShiftConcatInput fun {len : Nat} => blastShiftConcat
      source
      structure Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput {α : Type} [Hashable α] [DecidableEq α] (old : Sat.AIG α) (w : Nat) :
      Type
      • aig : Sat.AIG α
      • wn : Nat
      • wr : Nat
      • q : self.aig.RefVec w
      • r : self.aig.RefVec w
      • hle : old.decls.size ≤ self.aig.decls.size
      Instances For
        source
        def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (falseRef trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) :
        BlastDivSubtractShiftOutput aig w
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (falseRef trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) :
          aig.decls.size ≤ (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls.size
          source
          theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (falseRef trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls.size) :
          (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls[idx] = aig.decls[idx]
          source
          structure Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput {α : Type} [Hashable α] [DecidableEq α] (old : Sat.AIG α) (w : Nat) :
          Type
          • aig : Sat.AIG α
          • q : self.aig.RefVec w
          • r : self.aig.RefVec w
          • hle : old.decls.size ≤ self.aig.decls.size
          Instances For
            source
            def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (curr : Nat) (falseRef trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) :
            BlastUdivOutput aig w
            Equations
            Instances For
              source
              @[irreducible]
              theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (curr : Nat) (falseRef trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) :
              aig.decls.size ≤ (go aig curr falseRef trueRef n d wn wr q r).aig.decls.size
              source
              @[irreducible]
              theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (curr : Nat) (falseRef trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig curr falseRef trueRef n d wn wr q r).aig.decls.size) :
              (go aig curr falseRef trueRef n d wn wr q r).aig.decls[idx] = aig.decls[idx]
              source
              def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (input : aig.BinaryRefVec w) :
              Sat.AIG.RefVecEntry α w
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastUdiv {α : Type} [Hashable α] [DecidableEq α] :
                Sat.AIG.LawfulVecOperator α Sat.AIG.BinaryRefVec fun {len : Nat} => blastUdiv