UNSATクエリのデバッグ中に、クエリステータスに興味深い違いがあることに気付きました。クエリ構造は次のとおりです。
assert(...)
(push) ; commenting any of these two calls
(check-sat) ; makes the whole query UNSAT, otherwise it is SAT
assert(...)
(check-sat) ; SAT or UNSAT depending on existence of previous call
(exit)
popクエリに呼び出しはありません。この動作をトリガーするクエリはここにあります。
なぜアイデア？
注：実際には増分は必要ありません。デバッグのみを目的としています。Z3バージョンは3.2です。
これは、数量化推論エンジンの 1 つのバグです。このバグは修正される予定です。当面は、解釈されない並べ替え + カーディナリティ制約の代わりにデータ型を使用することで、バグを回避できます。つまり、 and を次のように宣言QしますT。
(declare-datatypes () ((Q q_accept_S13 q_T0_init q_accept_S7 q_accept_S6 q_accept_S5 q_accept_S4 q_T0_S3 q_accept_S12 q_accept_S10 q_accept_S9 q_accept_all)))
(宣言-データ型 () ((T t_0 t_1 t_2 t_3 t_4 t_5 t_6 t_7)))
上記の宣言は、基本的に 2 つの「列挙」型を定義しています。これらの宣言により、2 番目のクエリに対して一貫した回答が得られます。