mathic 0.2.0

A compiler with builtin support of symbolic operations, built with LLVM/MLIR
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108

# Symbolic Dialect

## Overview

The `symbolic` dialect is a custom MLIR dialect for representing symbolic
algebraic expressions as a dataflow DAG. Expressions are built from named
symbolic variables (`symbolic.sym`) and arithmetic operations (`add`, `sub`,
`mul`, `div`). A `symbolic.eval` operation substitutes a variable with a
concrete value (e.g. `i32`).

The dialect is lowered to standard MLIR dialects (`arith`, `func`) through a
two-phase pipeline: extract evaluation functions, then convert operations
(see [SymbolicPasses.md](SymbolicPasses.md)).

## Type System

| MLIR Type | Mnemonic | Description |
|-----------|----------|-------------|
| `!symbolic.expr` | `expr` | A symbolic expression handle |

## Operations

### `symbolic.sym`

Introduces a symbolic variable with a name string:

```mlir
%0 = symbolic.sym "x" : !symbolic.expr
%1 = symbolic.sym "y" : !symbolic.expr
```

### `symbolic.add` / `sub` / `mul` / `div`

Binary arithmetic. Both operands accept either symbolic expressions or
concrete integers:

```mlir
%r = symbolic.add %lhs, %rhs : !symbolic.expr
%r = symbolic.sub %lhs, %rhs : !symbolic.expr
%r = symbolic.mul %lhs, %rhs : !symbolic.expr
%r = symbolic.div %lhs, %rhs : !symbolic.expr
```

### `symbolic.eval`

Evaluates a symbolic expression by substituting a named variable with a
concrete value:

```mlir
%result = symbolic.eval %expr, "x", %value : i32 -> i32
```

### Example

MLIR IR for `x * x + x`:

```mlir
%x = symbolic.sym "x" : !symbolic.expr
%xx = symbolic.mul %x, %x : !symbolic.expr
%r = symbolic.add %xx, %x : !symbolic.expr
```

## Project Structure

```
Dialects/
├── CMakeLists.txt
├── Makefile
├── include/
│   ├── Dialect/
│   │   ├── capi.h
│   │   └── Symbolic/
│   │       ├── Conversions/SymbolicToArith/
│   │       │   ├── SymbolicToArith.h
│   │       │   └── SymbolicToArith.td
│   │       ├── IR/
│   │       │   ├── SymbolicDialect.h
│   │       │   ├── SymbolicDialect.td
│   │       │   ├── SymbolicOps.h
│   │       │   ├── SymbolicOps.td
│   │       │   ├── SymbolicTypes.h
│   │       │   └── SymbolicTypes.td
│   │       └── Transforms/
│   │           ├── Passes.h
│   │           ├── Passes.td
│   │           └── SymbolicExtractEval.h
├── lib/
│   └── Dialect/
│       ├── capi.cpp
│       └── Symbolic/
│           ├── Conversions/SymbolicToArith/
│           │   └── SymbolicToArith.cpp
│           ├── IR/
│           │   ├── SymbolicDialect.cpp
│           │   ├── SymbolicOps.cpp
│           │   └── SymbolicTypes.cpp
│           └── Transforms/
│               └── SymbolicExtractEval.cpp
├── tools/
│   └── dialect-driver.cpp
└── tests/
    ├── CMakeLists.txt
    ├── Dialect/
    │   └── Symbolic/
    │       └── (lit tests)
    ├── lit.cfg.py
    └── lit.site.cfg.py.in
```