回路の結線パターンをHaskellで表す．

chalmers-lava2000 のインストール

現時点で手に入れやすい Lava のパッケージは Hackage に登録されている chalmers-lava2000 である．これを cabal コマンドを使ってインストールする．

$ cabal update
$ cabal install chalmers-lava2000

通常はこれで，$HOME/.cabal/ 以下に必要なものがインストールされる．

chalmers-lava2000 で外部定理証明器を使う方法（Linux）

chalmers-lava2000 では回路の性質を検証する関数 verify が使えない．これは verify に対応する外部定理証明器へのラッパーが提供されていないためである．その代りに satzoo あるいは smv へのラッパーが用意されているのでこれを使う．

satzoo を使う

定理証明器 satzoo はすでに DEPRICATED! とのことで，代りに MiniSat を使う．まず，

minisat のインストール

minisat を /usr/local/bin/ にインストールし，これに satzoo という別名を付けておく．

$ wget http://minisat.se/downloads/minisat2-070721.zip
$ unzip minisat2-070721.zip
$ cd minisat
$ cd simp
$ make rs
$ sudo cp minisat_static /usr/local/bin/minisat
$ sudo ln -s /usr/local/bin/minisat /usr/local/bin/satzoo

ラッパーを設定

利用時に環境変数 Lava2000_Satzoo が /usr/local/bin/satzoo を指すようにしておく．シェルとして bash を使っているなら，$HOME/.bashrc に

export Lava2000_Satzoo=/usr/local/bin/satzoo

を書いておけばよいでしょう．ラッパースクリプトに実行パーミッションを立てる．chalmers-lava2000 を前述のようにインストールしたのなら，ラッパースクリプトは $HOME/.cabal/share/chalmers-lava2000-/Scripts に置かれているはず.

$ chmod +x $HOME/.cabal/share/chalmers-lava2000-1.1.1/Scripts/satzoo.wrapper
翻訳書バグ報告