Documentation

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

This module contains the implementation of a bitblaster for BitVec.shiftRight. It distinguishes two cases:

  1. Shifting by a constant distance (trivial)
  2. Shifting by a symbolic BitVec distance (requires symbolic branches over the distance).
Equations
    Instances For
      @[irreducible]
      def Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (input : aig.RefVec w) (distance curr : Nat) (hcurr : curr w) (s : aig.RefVec curr) :
      Equations
        Instances For
          @[irreducible]
          theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (distance : Nat) (input : aig.RefVec w) (curr : Nat) (hcurr : curr w) (s : aig.RefVec curr) :
          aig.decls.size (go aig input distance curr hcurr s).aig.decls.size
          @[irreducible]
          theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (distance : Nat) (input : aig.RefVec w) (curr : Nat) (hcurr : curr w) (s : aig.RefVec curr) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig input distance curr hcurr s).aig.decls.size) :
          (go aig input distance curr hcurr s).aig.decls[idx] = aig.decls[idx]
          Equations
            Instances For
              @[irreducible]
              def Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {aig : Sat.AIG α} (input : aig.RefVec w) (distance curr : Nat) (hcurr : curr w) (s : aig.RefVec curr) :
              aig.RefVec w
              Equations
                Instances For
                  Instances For
                    Equations
                      Instances For
                        @[irreducible]
                        def Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go {α : Type} [Hashable α] [DecidableEq α] {w n : Nat} (aig : Sat.AIG α) (distance : aig.RefVec n) (curr : Nat) (acc : aig.RefVec w) :
                        Equations
                          Instances For
                            @[irreducible]
                            theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go_le_size {α : Type} [Hashable α] [DecidableEq α] {n w : Nat} (aig : Sat.AIG α) (distance : aig.RefVec n) (curr : Nat) (acc : aig.RefVec w) :
                            aig.decls.size (go aig distance curr acc).aig.decls.size
                            @[irreducible]
                            theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {n w : Nat} (aig : Sat.AIG α) (distance : aig.RefVec n) (curr : Nat) (acc : aig.RefVec w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig distance curr acc).aig.decls.size) :
                            (go aig distance curr acc).aig.decls[idx] = aig.decls[idx]
                            Equations
                              Instances For
                                @[irreducible]
                                def Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go {α : Type} [Hashable α] [DecidableEq α] {w n : Nat} (aig : Sat.AIG α) (distance : aig.RefVec n) (curr : Nat) (acc : aig.RefVec w) :
                                Equations
                                  Instances For
                                    @[irreducible]
                                    theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go_le_size {α : Type} [Hashable α] [DecidableEq α] {n w : Nat} (aig : Sat.AIG α) (distance : aig.RefVec n) (curr : Nat) (acc : aig.RefVec w) :
                                    aig.decls.size (go aig distance curr acc).aig.decls.size
                                    @[irreducible]
                                    theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {n w : Nat} (aig : Sat.AIG α) (distance : aig.RefVec n) (curr : Nat) (acc : aig.RefVec w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig distance curr acc).aig.decls.size) :
                                    (go aig distance curr acc).aig.decls[idx] = aig.decls[idx]