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.

structure Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput {α : Type} [Hashable α] [DecidableEq α] (aig : Sat.AIG α) (len : Nat) :

lhs : aig.RefVec len
bit : aig.Ref

Instances For

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

Instances For

instance Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.instLawfulVecOperatorShiftConcatInputBlastShiftConcat {α : Type} [Hashable α] [DecidableEq α] :

Sat.AIG.LawfulVecOperator α ShiftConcatInput fun {len : Nat} => blastShiftConcat

structure Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput {α : Type} [Hashable α] [DecidableEq α] (old : Sat.AIG α) (w : Nat) :

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

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

Instances For

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

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]

structure Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput {α : Type} [Hashable α] [DecidableEq α] (old : Sat.AIG α) (w : Nat) :

aig : Sat.AIG α
q : self.aig.RefVec w
r : self.aig.RefVec w
hle : old.decls.size ≤ self.aig.decls.size

Instances For

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

@[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

@[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]

def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (input : aig.BinaryRefVec w) :

Sat.AIG.RefVecEntry α w

Equations

Instances For

instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastUdiv {α : Type} [Hashable α] [DecidableEq α] :

Sat.AIG.LawfulVecOperator α Sat.AIG.BinaryRefVec fun {len : Nat} => blastUdiv