描いた線から関数を作りたかった

# 始めに
みなさん、中学生の時に数学の授業でグラフを描いたことありますよね？
例えば$y=x^2$のグラフは放物線になります。そしてこんなことも考えたはずです。

> 適当に線を描いたら、それを表す関数が作れるんじゃないの？

と。つまり数式からグラフを導き出すのではなく、グラフから数式を導き出そうということです。
そんな夢のようなことをしてみた**かったなぁ**、という記事です。


# 方針
Pythonで実装します。主に使用するライブラリは以下の2つです。
<table>
  <thead>
    <tr>
      <th>ライブラリ</th> <th>用途</th>
    </tr>
  </thead>
  <tr>
    <td> Tkinter </td> <td>線を描くためのキャンバスを生成するために使用します。</td>
  </tr>
  <tr>
    <td> Z3 </td> <td>与えられた数学的条件を満たす解を得るために用いる、Microsoft製のライブラリです。</td>
  </tr>
</table>
Tkinterで描いた線の通った座標$(x, y)$を満たすべき条件に使用し、Z3で解を求めます。


# 実装
<table>
  <thead>
    <tr>
      <th>クラス名</th> <th>役割</th>
    </tr>
  </thead>
  <tr>
    <td> Main </td> <td>エントリーポイントです。</td>
  </tr>
  <tr>
    <td> IPaintListener </td> <td>描画時に呼ばれる関数を宣言したインターフェースです。</td>
  </tr>
  <tr>
    <td> Paint </td> <td>ペイントツールのようなキャンバスを生成し、ここに線を描いていきます。キャンバスを操作した時にIPaintListenerへ通知を送ります。</td>
  </tr>
  <tr>
    <td> SMT </td> <td>解となる数式を求めます。</td>
  </tr>
</table>

ソースコードは以下の通りです。折り畳んでいます。
なお、Paintクラスを実装するにあたって、[Tkinterでペイントもどきを作る](https://qiita.com/kuwabatake/items/482e72c429d6274d7b76)を参考にしました。

<details><summary>折り畳んでいます</summary>

```python:Main.py
from Paint import Paint
from SMT import SMT

if __name__ == '__main__':
    # インスタンスを生成
    paint = Paint()
    smt = SMT()

    # マウス操作のリスナーを登録
    paint.set_listener(smt)
    
    # メイン処理開始
    paint.start()
```

```py:IPaintListener.py
from abc import ABCMeta, abstractmethod

class IPaintListener(metaclass = ABCMeta):
    # 左クリック時に呼ばれる
    def on_click(self, x, y):
        return

    # ドラッグ実行時に呼ばれる
    def on_drag(self, x, y):
        return

    # リセット時に呼ばれる
    def on_reset(self):
        return

    # 完成時に呼ばれる
    def on_complete(self):
        return
```

```python:Paint.py
import tkinter
from IPaintListener import IPaintListener

class Paint:
    def __init__(self):
        # 描画中の線のIDを初期化
        self.current_id = -1

        # メインウインドウを作成
        self.root = tkinter.Tk()
        self.root.title("Paint")

        # リセットボタンを作成
        reset_button = tkinter.Button(self.root)
        reset_button.config(text = "リセット", command = self.on_reset)
        reset_button.pack()

        # 完成ボタンを作成
        complete_button = tkinter.Button(self.root)
        complete_button.config(text = "完成", command = self.on_complete)
        complete_button.pack()

        # キャンバスを作成
        self.width = 200
        self.height = 200
        self.canvas = tkinter.Canvas(
            self.root, width = self.width, height = self.height, bg = "white")
        self.canvas.pack(expand = True, fill = tkinter.BOTH)

        # 描画処理を登録
        self.canvas.bind("<ButtonPress-1>", self.on_click)
        self.canvas.bind("<B1-Motion>", self.on_drag)

        # リスナーを初期化
        self.listener = None

    # メインループ開始
    def start(self):
        self.root.mainloop()

    # リスナーを登録
    def set_listener(self, listener: IPaintListener):
        self.listener = listener

    # 左クリック時に呼ばれる
    def on_click(self, event):
        self.current_id = self.canvas.create_line(
            event.x, event.y, event.x, event.y, fill = "black", width = 1, tag = "line")
        if self.listener is not None:
            self.listener.on_click(event.x, event.y)

    # ドラッグ実行時に呼ばれる
    def on_drag(self, event):
        points = self.canvas.coords(self.current_id)
        points.extend([event.x, event.y])
        self.canvas.coords(self.current_id, points)
        if self.listener is not None:
            self.listener.on_drag(event.x, event.y)

    # リセット時に呼ばれる
    def on_reset(self):
        self.canvas.delete("line")
        if self.listener is not None:
            self.listener.on_reset()

    # 完成時に呼ばれる
    def on_complete(self):
        if self.listener is not None:
            self.listener.on_complete()
```

```python:SMT.py
from z3 import *
from IPaintListener import IPaintListener

class SMT(IPaintListener):
    def __init__(self):
        self.f = Function("f", RealSort(), RealSort())
        self.s = Solver()

    # 制約を追加
    def add_constraint(self, x, y):
        self.s.add(self.f(x) == y)

    # 解を求める
    def solve(self):
        result = self.s.check()
        print(result)
        if result == sat:
            print(self.s.model())

    # 左クリック時に呼ばれる
    def on_click(self, x, y):
        self.add_constraint(x, y)

    # ドラッグ実行時に呼ばれる
    def on_drag(self, x, y):
        self.add_constraint(x, y)

    # リセット時に呼ばれる
    def on_reset(self):
        self.s.reset()

    # 完成時に呼ばれる
    def on_complete(self):
        self.solve()
```

</details>

# 結果
こんな感じのツールが出来上がりました。完成ボタンを押すことで数式を求めます。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/501246/340ea572-989c-9b9f-9679-e81945635e4d.png)

しかしタイトルを読んで察しているかと思いますが、全然上手くいきませんでした。
適当な線を描いてみたら充足不可能になるか、充足可能でも単に条件の数だけ分岐のある関数ができるだけで、中学生の時に勉強した多項式はできませんでした。
座標$(x, y)$から上手く制約条件を設定できればいいんですけど、まだまだ勉強不足です。

# 最後に
お盆休みの間に勉強していたらSMTソルバやZ3の存在を知って、昔感じた疑問を検証してみようと思ったのですが、現実は甘くありませんでした。
もっと便利なツールがあるのかな？