Documentation

Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec

structure BitVec.Literal :

A bit-vector literal

  • n : Nat

    Size.

  • value : BitVec self.n

    Actual value.

Instances For

    Try to convert OfNat.ofNat/BitVec.OfNat application into a bitvector literal.

    Equations
    Instances For
      @[inline]
      def BitVec.reduceUnary (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec nBitVec n) (e : Lean.Expr) :

      Helper function for reducing homogeneous unary bitvector operators.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[inline]
        def BitVec.reduceBin (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec nBitVec nBitVec n) (e : Lean.Expr) :

        Helper function for reducing homogeneous binary bitvector operators.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[inline]
          def BitVec.reduceExtend (declName : Lake.Name) (op : {n : Nat} → (m : Nat) → BitVec nBitVec m) (e : Lean.Expr) :

          Simplification procedure for setWidth, zeroExtend and signExtend on BitVecs.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[inline]
            def BitVec.reduceGetBit (declName : Lake.Name) (op : {n : Nat} → BitVec nNatBool) (e : Lean.Expr) :

            Helper function for reducing bitvector functions such as getLsb and getMsb.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[inline]
              def BitVec.reduceShift (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec nNatBitVec n) (e : Lean.Expr) :

              Helper function for reducing bitvector functions such as shiftLeft and rotateRight.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[inline]

                Helper function for reducing x <<< i and x >>> i where i is a bitvector literal, into one that is a natural number literal.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[inline]
                  def BitVec.reduceBinPred (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec nBitVec nBool) (e : Lean.Expr) :

                  Helper function for reducing bitvector predicates.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[inline]
                    def BitVec.reduceBoolPred (declName : Lake.Name) (arity : Nat) (op : {n : Nat} → BitVec nBitVec nBool) (e : Lean.Expr) :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Simplification procedure for negation of BitVecs.

                      Equations
                      Instances For

                        Simplification procedure for bitwise not of BitVecs.

                        Equations
                        Instances For

                          Simplification procedure for absolute value of BitVecs.

                          Equations
                          Instances For

                            Simplification procedure for bitwise and of BitVecs.

                            Equations
                            Instances For

                              Simplification procedure for bitwise or of BitVecs.

                              Equations
                              Instances For

                                Simplification procedure for bitwise xor of BitVecs.

                                Equations
                                Instances For

                                  Simplification procedure for addition of BitVecs.

                                  Equations
                                  Instances For

                                    Simplification procedure for multiplication of BitVecs.

                                    Equations
                                    Instances For

                                      Simplification procedure for subtraction of BitVecs.

                                      Equations
                                      Instances For

                                        Simplification procedure for division of BitVecs.

                                        Equations
                                        Instances For

                                          Simplification procedure for the modulo operation on BitVecs.

                                          Equations
                                          Instances For

                                            Simplification procedure for the unsigned modulo operation on BitVecs.

                                            Equations
                                            Instances For

                                              Simplification procedure for unsigned division of BitVecs.

                                              Equations
                                              Instances For

                                                Simplification procedure for division of BitVecs using the SMT-Lib conventions.

                                                Equations
                                                Instances For

                                                  Simplification procedure for the signed modulo operation on BitVecs.

                                                  Equations
                                                  Instances For

                                                    Simplification procedure for signed remainder of BitVecs.

                                                    Equations
                                                    Instances For

                                                      Simplification procedure for signed t-division of BitVecs.

                                                      Equations
                                                      Instances For

                                                        Simplification procedure for signed division of BitVecs using the SMT-Lib conventions.

                                                        Equations
                                                        Instances For

                                                          Simplification procedure for getLsb (lowest significant bit) on BitVec.

                                                          Equations
                                                          Instances For

                                                            Simplification procedure for getMsb (most significant bit) on BitVec.

                                                            Equations
                                                            Instances For

                                                              Simplification procedure for shift left on BitVec.

                                                              Equations
                                                              Instances For

                                                                Simplification procedure for unsigned shift right on BitVec.

                                                                Equations
                                                                Instances For

                                                                  Simplification procedure for signed shift right on BitVec.

                                                                  Equations
                                                                  Instances For

                                                                    Simplification procedure for shift left on BitVec.

                                                                    Equations
                                                                    Instances For

                                                                      Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.

                                                                      Equations
                                                                      Instances For

                                                                        Simplification procedure for shift right on BitVec.

                                                                        Equations
                                                                        Instances For

                                                                          Simplification procedure for converting a shift with a bit-vector literal into a natural number literal.

                                                                          Equations
                                                                          Instances For

                                                                            Simplification procedure for rotate left on BitVec.

                                                                            Equations
                                                                            Instances For

                                                                              Simplification procedure for rotate right on BitVec.

                                                                              Equations
                                                                              Instances For

                                                                                Simplification procedure for append on BitVec.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For

                                                                                  Simplification procedure for casting BitVecs along an equality of the size.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For

                                                                                    Simplification procedure for BitVec.toNat.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For

                                                                                      Simplification procedure for BitVec.toInt.

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For

                                                                                        Simplification procedure for BitVec.ofInt.

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For

                                                                                          Simplification procedure for ensuring BitVec.ofNat literals are normalized.

                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For

                                                                                            Simplification procedure for = on BitVecs.

                                                                                            Equations
                                                                                            Instances For

                                                                                              Simplification procedure for on BitVecs.

                                                                                              Equations
                                                                                              Instances For

                                                                                                Simplification procedure for == on BitVecs.

                                                                                                Equations
                                                                                                Instances For

                                                                                                  Simplification procedure for != on BitVecs.

                                                                                                  Equations
                                                                                                  Instances For

                                                                                                    Simplification procedure for < on BitVecs.

                                                                                                    Equations
                                                                                                    Instances For

                                                                                                      Simplification procedure for on BitVecs.

                                                                                                      Equations
                                                                                                      Instances For

                                                                                                        Simplification procedure for > on BitVecs.

                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          Simplification procedure for on BitVecs.

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            Simplification procedure for unsigned less than ult on BitVecs.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              Simplification procedure for unsigned less than or equal ule on BitVecs.

                                                                                                              Equations
                                                                                                              Instances For

                                                                                                                Simplification procedure for signed less than slt on BitVecs.

                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  Simplification procedure for signed less than or equal sle on BitVecs.

                                                                                                                  Equations
                                                                                                                  Instances For

                                                                                                                    Simplification procedure for setWidth' on BitVecs.

                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For

                                                                                                                      Simplification procedure for shiftLeftZeroExtend on BitVecs.

                                                                                                                      Equations
                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                      Instances For

                                                                                                                        Simplification procedure for extractLsb' on BitVecs.

                                                                                                                        Equations
                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                        Instances For

                                                                                                                          Simplification procedure for replicate on BitVecs.

                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For

                                                                                                                            Simplification procedure for setWidth on BitVecs.

                                                                                                                            Equations
                                                                                                                            Instances For

                                                                                                                              Simplification procedure for zeroExtend on BitVecs.

                                                                                                                              Equations
                                                                                                                              Instances For

                                                                                                                                Simplification procedure for signExtend on BitVecs.

                                                                                                                                Equations
                                                                                                                                Instances For

                                                                                                                                  Simplification procedure for allOnes

                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For
                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      Equations
                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                      Instances For
                                                                                                                                        @[inline]

                                                                                                                                        Helper function for reducing (x <<< i) <<< j (and (x >>> i) >>> j) where i and j are natural number literals.

                                                                                                                                        Equations
                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                        Instances For