3

unsat クエリでアサーションの順序を変更すると、sat になります。

クエリ構造は次のとおりです。

definitions1
assertions1
definitions2
bad_assertions
check-sat

Python の sorted 関数で bad_assertions をソートすると、Unsat クエリが Sat になります。

Z3 バージョン 4.0、4.1; Ubuntu 12.04

残念ながら、クエリは非常に大きく、デバッグが難しいため、その他の追加情報があれば提供できます。

これは、混合用にマークされた行を含む元の unsatクエリと、クエリ内の行を混合するための単純な pythonスクリプトです。

4

2 に答える 2

4

あなたの質問で報告された問題を再現することができました。どちらの例も満足です。生成するスクリプトunsatは、データ型理論のバグを明らかにしています。バグを修正しました。修正は Z3 4.2 で利用可能になります。これは健全性のバグであるため、まもなくバージョン 4.2 をリリースします。RELEVANCY=0当面は、コマンド ラインでオプションを使用してバグを回避できます。

于 2012-09-06T00:54:10.587 に答える
1

あなたの説明から、それはバグのように聞こえます。もちろん、sat/unsat は順序に依存すべきではありません。再現をパッケージ化するのが難しい場合、問題をデバッグするのに役立つ 1 つの方法は、バグの原因に確信が持てたら、「open_log()」を使用して Z3 とのすべてのやり取りのトレースをダンプすることです。Z3 への他の呼び出しの前に「open_log」を使用する必要があります。その後、ソースなしでログを再生できます。

于 2012-09-05T13:33:14.880 に答える