[all-commits] [llvm/llvm-project] de6729: [mlir][SMT] upstream `SMT` dialect (#131480)

Maksim Levental via All-commits all-commits at lists.llvm.org
Fri Apr 11 14:10:31 PDT 2025


  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: de67293c093efddb9f9444b3a614695ad243355d
      https://github.com/llvm/llvm-project/commit/de67293c093efddb9f9444b3a614695ad243355d
  Author: Maksim Levental <maksim.levental at gmail.com>
  Date:   2025-04-11 (Fri, 11 Apr 2025)

  Changed paths:
    M mlir/include/mlir/Dialect/CMakeLists.txt
    A mlir/include/mlir/Dialect/SMT/CMakeLists.txt
    A mlir/include/mlir/Dialect/SMT/IR/CMakeLists.txt
    A mlir/include/mlir/Dialect/SMT/IR/SMT.td
    A mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
    A mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h
    A mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
    A mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
    A mlir/include/mlir/Dialect/SMT/IR/SMTDialect.h
    A mlir/include/mlir/Dialect/SMT/IR/SMTDialect.td
    A mlir/include/mlir/Dialect/SMT/IR/SMTIntOps.td
    A mlir/include/mlir/Dialect/SMT/IR/SMTOps.h
    A mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
    A mlir/include/mlir/Dialect/SMT/IR/SMTTypes.h
    A mlir/include/mlir/Dialect/SMT/IR/SMTTypes.td
    A mlir/include/mlir/Dialect/SMT/IR/SMTVisitors.h
    M mlir/include/mlir/InitAllDialects.h
    M mlir/lib/Dialect/CMakeLists.txt
    A mlir/lib/Dialect/SMT/CMakeLists.txt
    A mlir/lib/Dialect/SMT/IR/CMakeLists.txt
    A mlir/lib/Dialect/SMT/IR/SMTAttributes.cpp
    A mlir/lib/Dialect/SMT/IR/SMTDialect.cpp
    A mlir/lib/Dialect/SMT/IR/SMTOps.cpp
    A mlir/lib/Dialect/SMT/IR/SMTTypes.cpp
    A mlir/test/Dialect/SMT/array-errors.mlir
    A mlir/test/Dialect/SMT/array.mlir
    A mlir/test/Dialect/SMT/basic.mlir
    A mlir/test/Dialect/SMT/bitvector-errors.mlir
    A mlir/test/Dialect/SMT/bitvectors.mlir
    A mlir/test/Dialect/SMT/core-errors.mlir
    A mlir/test/Dialect/SMT/cse-test.mlir
    A mlir/test/Dialect/SMT/integers.mlir
    M mlir/unittests/Dialect/CMakeLists.txt
    A mlir/unittests/Dialect/SMT/AttributeTest.cpp
    A mlir/unittests/Dialect/SMT/CMakeLists.txt
    A mlir/unittests/Dialect/SMT/QuantifierTest.cpp
    A mlir/unittests/Dialect/SMT/TypeTest.cpp

  Log Message:
  -----------
  [mlir][SMT] upstream `SMT` dialect (#131480)

This PR upstreams the `SMT` dialect from the CIRCT project. Here we only
check in the dialect/op/types/attributes and lit tests. Follow up PRs
will add conversions in and out and etc.

Co-authored-by: Bea Healy <beahealy22 at gmail.com>
Co-authored-by: Martin Erhart <maerhart at outlook.com>
Co-authored-by: Mike Urbach <mikeurbach at gmail.com>
Co-authored-by: Will Dietz <will.dietz at sifive.com>
Co-authored-by: fzi-hielscher <hielscher at fzi.de>
Co-authored-by: Fehr Mathieu <mathieu.fehr at gmail.com>



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications


More information about the All-commits mailing list