Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry

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.

source

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

Type

w : Nat
vec : aig.BinaryRefVec self.w
cin : aig.Ref

Instances For

source

def Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput aig) :

Std.Sat.AIG.Entrypoint α

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

source

@[irreducible]

def Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (lhs : aig.RefVec w) (rhs : aig.RefVec w) (curr : Nat) (cin : aig.Ref) :

Std.Sat.AIG.Entrypoint α

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {curr : Nat} {aig : Std.Sat.AIG α} {cin : aig.Ref} {lhs : aig.RefVec w} {rhs : aig.RefVec w} :

aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs curr cin).aig.decls.size

source

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {curr : Nat} {aig : Std.Sat.AIG α} {cin : aig.Ref} {lhs : aig.RefVec w} {rhs : aig.RefVec w} (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs curr cin).aig.decls.size) :

(Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs curr cin).aig.decls[idx] = aig.decls[idx]

source

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

Std.Sat.AIG.LawfulOperator α Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit

Equations

Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.instLawfulOperatorOverflowInput = { le_size := ⋯, decl_eq := ⋯ }