simplification コマンドに --prepare オプションを追加した

[cedretaber]

修正内容: https://hackmd.io/n7zyyweESjap8K8Qxk3kfA

概要

simplification コマンドに --prepare オプションを付けることで、 view がある場合に、その view と同名のΔ述語が存在しているかのように処理される。
詳しくはサンプルコードを見てみてください。

サンプルコード

source x('A':int).
view v('A':int).

+x(A) :- x(A), v(A), A <> 42.
-x(A) :- +x(A), -v(A).

❯ dune exec bin/simplification.exe -- examples/simplification_prepare1.dl
source x('A':int).                     
view v('A':int).
+x(A) :- v(A) , x(A) , not A = 42.

❯ dune exec bin/simplification.exe -- examples/simplification_prepare1.dl --prepare
source x('A':int).                     
view v('A':int).
-x(A) :- -v(A) , +x(A).
+x(A) :- v(A) , x(A) , not A = 42.

-v(A) は存在しないため、 simplification コマンドを使うと -x(A) :- +x(A), -v(A). は偽とみなされて消されてしまう。
しかし、 --prepare オプションを付けると、 view である v から +v(A) と -v(A) が存在するとみなされるので、 -x(A) も残る。

delta insert の場合も同様。

source x('A':int).
view v('A':int).

+x(A) :- x(A), v(A), A <> 42.
-x(A) :- +x(A), +v(A).

❯ dune exec bin/simplification.exe -- examples/simplification_prepare2.dl 
source x('A':int).                     
view v('A':int).
+x(A) :- v(A) , x(A) , not A = 42.

❯ dune exec bin/simplification.exe -- examples/simplification_prepare2.dl --prepare
source x('A':int).                     
view v('A':int).
-x(A) :- +v(A) , +x(A).
+x(A) :- v(A) , x(A) , not A = 42.

[hiroyukikato]

Thank you! LGTM