これは何？ EUF(Equality Logic with Uninterpreted Function)用のSMTソルバを、SATソルバは既知のものとして作ってみた話です。 なんでやろうと思ったの？ 前からAlloy(https://alloytools.org/)のような、SATを利用して何かを作るということに興味があった…