This module contains the implementation of a circuit to determine whether a certain addition would overflow. This is provided separately from the addition circuit for two reasons:
- Determining whether an overflow will occur does not require to build a full ripple carry adder.
- Other operations such as unsigned less than may be implemented in terms of overflow detection.
structure
Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput
{α : Type}
[Hashable α]
[DecidableEq α]
(aig : Sat.AIG α)
:
- w : Nat
- vec : aig.BinaryRefVec self.w
- cin : aig.Ref
Instances For
def
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit
{α : Type}
[Hashable α]
[DecidableEq α]
(aig : Sat.AIG α)
(input : OverflowInput aig)
:
Equations
- Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit aig { w := w, vec := { lhs := lhs, rhs := rhs }, cin := cin } = Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs 0 cin
Instances For
@[irreducible]
def
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Sat.AIG α)
(lhs rhs : aig.RefVec w)
(curr : Nat)
(cin : aig.Ref)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[irreducible]
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go_le_size
{α : Type}
[Hashable α]
[DecidableEq α]
{w curr : Nat}
{aig : Sat.AIG α}
{cin : aig.Ref}
{lhs rhs : aig.RefVec w}
:
@[irreducible]
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go_decl_eq
{α : Type}
[Hashable α]
[DecidableEq α]
{w curr : Nat}
{aig : Sat.AIG α}
{cin : aig.Ref}
{lhs rhs : aig.RefVec w}
(idx : Nat)
(h1 : idx < aig.decls.size)
(h2 : idx < (go aig lhs rhs curr cin).aig.decls.size)
: