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

This module contains the implementation of a bitblaster for BitVec.add. The implemented circuit is a ripple carry adder.

source

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

Type

lhs : aig.Ref
rhs : aig.Ref
cin : aig.Ref

Instances For

source

def Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (val : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1) (h : aig1.decls.size ≤ aig2.decls.size) :

Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig2

Equations

{ lhs := lhs, rhs := rhs, cin := cin }.cast h = { lhs := lhs.cast h, rhs := rhs.cast h, cin := cin.cast h }

Instances For

source

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.lhs_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (s : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1) (hcast : aig1.decls.size ≤ aig2.decls.size) :

(s.cast hcast).lhs = s.lhs.cast hcast

source

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.rhs_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (s : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1) (hcast : aig1.decls.size ≤ aig2.decls.size) :

(s.cast hcast).rhs = s.rhs.cast hcast

source

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.cin_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (s : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1) (hcast : aig1.decls.size ≤ aig2.decls.size) :

(s.cast hcast).cin = s.cin.cast hcast

source

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

Std.Sat.AIG.Entrypoint α

Equations

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

Instances For

source

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

Std.Sat.AIG.LawfulOperator α Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderOut

Equations

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

source

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

Std.Sat.AIG.Entrypoint α

Equations

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

Instances For

source

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

Std.Sat.AIG.LawfulOperator α Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderCarry

Equations

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

source

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

Type

aig : Std.Sat.AIG α
out : self.aig.Ref
cout : self.aig.Ref
hle : old.decls.size ≤ self.aig.decls.size

Instances For

source

theorem Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput.hle {α : Type} [Hashable α] [DecidableEq α] {old : Std.Sat.AIG α} (self : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput old) :

old.decls.size ≤ self.aig.decls.size

source

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

Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput aig

Equations

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

Instances For

source

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

Std.Sat.AIG.RefVecEntry α w

Equations

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

Instances For

source

@[irreducible]

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

Std.Sat.AIG.RefVecEntry α w

Equations

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

Instances For

source

@[irreducible]

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

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

source

@[irreducible]

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

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

source

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

Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.BinaryRefVec fun {len : Nat} => Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd

Equations

Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.instLawfulVecOperatorBinaryRefVec = { le_size := ⋯, decl_eq := ⋯ }