問題タブ [z3py]

私が書いている調査ツールにPythonAPIのサポートを含めるために、Z3のPythonAPIを使用しています。Pythonインターフェースを使用して満足できないコアを抽出することに関して質問があります。

次の簡単なクエリがあります。

このクエリをz3実行可能ファイル（Z3 4.1の場合）で実行すると、期待どおりの結果が得られます。

Z3 4.3の場合、セグメンテーション違反が発生します。

それは興味深い観察でしたが、それは主な質問ではありません。次に、クエリを（ファイル内で）次のように変更しました

ファイルハンドラーを使用して、このファイルの内容を（変数 `queryStr'で）次のPythonコードに渡しました。

`unsat_core'関数から空のリストを受け取ります：[]。この機能を間違って使用していますか？関数のdocstringは、代わりに次のようなことを行う必要があることを示しています

ただし、SMT-LIB v2.0標準に準拠しているため（私は信じています）、クエリをそのまま使用できるかどうか、そして明らかな何かが欠けているかどうか疑問に思いました。

g = And(ForAll([i, j, k], Implies(And(k <= 0, A * i + B * j + C * k + D <= 0), k + i - j <= 0)),Not(And(A==0,B==0,C==0))) を使用して式を満たす A、B、C、D の値を見つけようとしますsolve(g) 。これには多くの可能な解決策があります.1つはA=1,B=-1,C=D=0Z3がこれを行うことができないようです（solve(g)終了しません）.

Z3 はこの種の非線形 (しかし単純な) 式を実行できますか? おそらく、これに対していくつかのQE戦略または何かを指定できますか？

私はそれを証明しようとしています

4*n^3*m+4*n*m^3 <= n^4+6*n^2*m^2+m^4

すべてのn、m実数。Z3Py をオンラインで使用します。

私はコードを使用しています：

出力は : unknownです。

Z3が入手できない理由を教えてください "sat"。

Mac で z3py に奇妙な問題が発生しています。

x の値がモデルにありません。マスター ブランチと不安定ブランチの両方を試してみましたが、結果は同じでした。ただし、同様の .smt2 ファイルで実行すると、z3 自体は正しいモデルを提供します。私の構成は Mac OSX 10.6.8、Python 2.7.4 です。

z3py API (4.3.0) を使用しています。exprを使用して、式をデフォルトのコンテキストから新しいコンテキストtarget_ctxに簡単に変換できますexpr.translate(target_ctx)。ctxしかし、特定のコンテキストからデフォルトの Z3 コンテキストに変換するにはどうすればよいでしょうか? ContextPython API からデフォルトを取得する方法はありますか?

a1 == a + bの場合、 との 2 つの式a1 == bは等価ですa == 0。a == 0この必須条件( )をZ3 pythonで見つけたい。以下のコードを書きました。

ただし、上記のコードは常に"Not Equ"出力として返されます。それから明らかに、モデル ( a === 0) を条件として取得することも、同等にする"f"こともできません。"g"

コードのどこが間違っているのか、それを修正する方法について何か考えはありますか? 本当にありがとう！