Documentation

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 : Sat.AIG α) :
Type
Instances For
    source
    def Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : Sat.AIG α} (val : FullAdderInput aig1) (h : aig1.decls.size ≤ aig2.decls.size) :
    FullAdderInput aig2
    Equations
      Instances For
        source
        @[simp]
        theorem Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.lhs_cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : Sat.AIG α} (s : 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 aig2 : Sat.AIG α} (s : 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 aig2 : Sat.AIG α} (s : 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 : Sat.AIG α) (input : FullAdderInput aig) :
        Sat.AIG.Entrypoint α
        Equations
          Instances For
            source
            instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulOperatorFullAdderInputMkFullAdderOut {α : Type} [Hashable α] [DecidableEq α] :
            Sat.AIG.LawfulOperator α FullAdderInput mkFullAdderOut
            source
            def Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderCarry {α : Type} [Hashable α] [DecidableEq α] (aig : Sat.AIG α) (input : FullAdderInput aig) :
            Sat.AIG.Entrypoint α
            Equations
              Instances For
                source
                instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulOperatorFullAdderInputMkFullAdderCarry {α : Type} [Hashable α] [DecidableEq α] :
                Sat.AIG.LawfulOperator α FullAdderInput mkFullAdderCarry
                source
                structure Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput {α : Type} [Hashable α] [DecidableEq α] (old : Sat.AIG α) :
                Type
                Instances For
                  source
                  def Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdder {α : Type} [Hashable α] [DecidableEq α] (aig : Sat.AIG α) (input : FullAdderInput aig) :
                  FullAdderOutput aig
                  Equations
                    Instances For
                      source
                      def Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (input : aig.BinaryRefVec w) :
                      Sat.AIG.RefVecEntry α w
                      Equations
                        Instances For
                          source
                          def Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.blast {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (input : aig.BinaryRefVec w) :
                          Sat.AIG.RefVecEntry α w
                          Equations
                            Instances For
                              source
                              @[irreducible]
                              def Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (lhs rhs : aig.RefVec w) (curr : Nat) (hcurr : curr ≤ w) (cin : aig.Ref) (s : aig.RefVec curr) :
                              Sat.AIG.RefVecEntry α w
                              Equations
                                Instances For
                                  source
                                  @[irreducible]
                                  theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w) :
                                  aig.decls.size ≤ (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 : Sat.AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs rhs curr hcurr cin s).aig.decls.size) :
                                  (go aig lhs rhs curr hcurr cin s).aig.decls[idx] = aig.decls[idx]
                                  source
                                  instance Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.instLawfulVecOperatorBinaryRefVecBlast {α : Type} [Hashable α] [DecidableEq α] :
                                  Sat.AIG.LawfulVecOperator α Sat.AIG.BinaryRefVec fun {len : Nat} => blast
                                  source
                                  instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastAdd {α : Type} [Hashable α] [DecidableEq α] :
                                  Sat.AIG.LawfulVecOperator α Sat.AIG.BinaryRefVec fun {len : Nat} => blastAdd