Documentation

SSA.Projects.InstCombine.AliveHandwrittenLargeExamples

source
def AliveHandwritten.DivRemOfSelect.alive_DivRemOfSelect_src (w : ℕ) :
Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy <$> ((Ctxt.snoc [] (InstCombine.MTy.bitvec 1)).snoc (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))).snoc (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩)))

Name: SimplifyDivRemOfSelect precondition: true %sel = select %c, %Y, 0 %r = udiv %X, %sel => %r = udiv %X, %Y

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def AliveHandwritten.DivRemOfSelect.alive_DivRemOfSelect_tgt (w : ℕ) :
    Com InstCombine.LLVM ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy <$> ((Ctxt.snoc [] (InstCombine.MTy.bitvec 1)).snoc (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))).snoc (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩))) EffectKind.pure ((InstcombineTransformDialect.MOp.instantiateCom ⟨[w], ⋯⟩).mapTy (InstCombine.MTy.bitvec (MLIR.AST.Width.mvar ⟨0, ⋯⟩)))
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem AliveHandwritten.DivRemOfSelect.alive_DivRemOfSelect (w : ℕ) :
      (AliveHandwritten.DivRemOfSelect.alive_DivRemOfSelect_src w ⊑ AliveHandwritten.DivRemOfSelect.alive_DivRemOfSelect_tgt w) ⋯
      source
      def AliveHandwritten.MulDivRem.MulDivRem805_lhs (w : ℕ) :
      Com InstCombine.LLVM [InstCombine.Ty.bitvec w] EffectKind.pure (InstCombine.Ty.bitvec w)
      Equations
      Instances For
        source
        def AliveHandwritten.MulDivRem.MulDivRem805_rhs (w : ℕ) :
        Com InstCombine.LLVM [InstCombine.Ty.bitvec w] EffectKind.pure (InstCombine.Ty.bitvec w)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def AliveHandwritten.MulDivRem.alive_simplifyMulDivRem805 (w : ℕ) :
          (AliveHandwritten.MulDivRem.MulDivRem805_lhs w ⊑ AliveHandwritten.MulDivRem.MulDivRem805_rhs w) ⋯
          Equations
          • ⋯ = ⋯
          Instances For
            source
            def AliveHandwritten.MulDivRem.alive_simplifyMulDivRem805' (w : ℕ) :
            (AliveHandwritten.MulDivRem.MulDivRem805_lhs w ⊑ AliveHandwritten.MulDivRem.MulDivRem805_rhs w) ⋯
            Equations
            • ⋯ = ⋯
            Instances For
              source
              def AliveHandwritten.MulDivRem.MulDivRem290_lhs (w : ℕ) :
              Com InstCombine.LLVM [InstCombine.Ty.bitvec w, InstCombine.Ty.bitvec w] EffectKind.pure (InstCombine.Ty.bitvec w)
              Equations
              Instances For
                source
                def AliveHandwritten.MulDivRem.MulDivRem290_rhs (w : ℕ) :
                Com InstCombine.LLVM [InstCombine.Ty.bitvec w, InstCombine.Ty.bitvec w] EffectKind.pure (InstCombine.Ty.bitvec w)
                Equations
                Instances For
                  source
                  def AliveHandwritten.MulDivRem.alive_simplifyMulDivRem290 (w : ℕ) :
                  (AliveHandwritten.MulDivRem.MulDivRem290_lhs w ⊑ AliveHandwritten.MulDivRem.MulDivRem290_rhs w) ⋯
                  Equations
                  • ⋯ = ⋯
                  Instances For
                    source
                    def AliveHandwritten.AndOrXor.AndOrXor2515_lhs (w : ℕ) :
                    Com InstCombine.LLVM [InstCombine.Ty.bitvec w, InstCombine.Ty.bitvec w, InstCombine.Ty.bitvec w, InstCombine.Ty.bitvec w] EffectKind.pure (InstCombine.Ty.bitvec w)
                    Equations
                    Instances For
                      source
                      def AliveHandwritten.AndOrXor.AndOrXor2515_rhs (w : ℕ) :
                      Com InstCombine.LLVM [InstCombine.Ty.bitvec w, InstCombine.Ty.bitvec w, InstCombine.Ty.bitvec w, InstCombine.Ty.bitvec w] EffectKind.pure (InstCombine.Ty.bitvec w)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def AliveHandwritten.AndOrXor.alive_simplifyAndOrXor2515 (w : ℕ) :
                        (AliveHandwritten.AndOrXor.AndOrXor2515_lhs w ⊑ AliveHandwritten.AndOrXor.AndOrXor2515_rhs w) ⋯
                        Equations
                        • ⋯ = ⋯
                        Instances For
                          source
                          def AliveHandwritten.Select.Select746_lhs (w : ℕ) :
                          Com InstCombine.LLVM [InstCombine.Ty.bitvec w] EffectKind.pure (InstCombine.Ty.bitvec w)
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def AliveHandwritten.Select.Select746_rhs (w : ℕ) :
                            Com InstCombine.LLVM [InstCombine.Ty.bitvec w] EffectKind.pure (InstCombine.Ty.bitvec w)
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def AliveHandwritten.Select.alive_simplifySelect764 (w : ℕ) :
                              (AliveHandwritten.Select.Select746_lhs w ⊑ AliveHandwritten.Select.Select746_rhs w) ⋯
                              Equations
                              • ⋯ = ⋯
                              Instances For