問題タブ [z3py]

ForAllで数量詞を使用しようとしているので、すべてbの式で結果が得られます。以下のコードでこれを実装しました（Z3 python）：a * b == bba == 1

a = 1Z3 が出力で提供してくれると思っていましたが、そうではありませんでしたUnsat。問題がどこにあるかについて何か考えはありますか？

(ForAll を適切に使用していないと思われますが、修正方法がわかりません)

問題例:

嘘つきは常に偽りを話し、真実を語る者は常に真実を話すと仮定します。さらに、エイミー、ボブ、カル、ダン、アーニー、フランシスがそれぞれうそつきか正直者であるとします。

これらの人々のうち、真実を語る人は誰ですか?

解決：

解釈:

コード：

出力：

解釈:

ここでこの例をオンラインで実行します

Z3-SMT-LIB を使用してこの問題を解決できるかどうか、ご意見をお聞かせください。どうもありがとう。

私はまだa値を見つける問題に苦労しているのでa * b == b、b. 期待される結果はa == 1です。以下に2つの解決策があります。

(A) 以下のコードで量指定子を使用してこれを実装しましたForAll(量指定子を使用せずに解決策がある場合は修正してください)。アイデアは証明することfでありg、同等です。

ただし、この単純なコードは、結果を返さずに永久に実行されます。のせいだと思いますForAll。問題を解決する方法について何か考えはありますか?

(B) 別のバージョンで再試行しました。今回は、2 つの式が等しいことを証明しませんが、すべてを 1 つの式にまとめますf。論理的には、これは正しいと思いますが、ここで間違っている場合は修正してください。

今回はコードはハングしませんが、すぐに「Unsat」を返します。これを修正する方法について何か考えはありますか?

どうもありがとう。

z3pyを使用して、アクションと事後条件が与えられたときに最も弱い前提条件を見つけたいです。

アクションN = N + 1と事後条件を考えるとN == 5、最も弱い前提条件は N == 4 になります。

Tactic を使用すると、solve-eqsこのアプローチは一部の投稿条件では機能しますが、他の条件では機能しません。投稿条件N < 5を使用すると、 [[Not(4 <= N)]].

しかし、N == 5私が使用[[]]するとき、私が望むときN == 4。

これは、最も弱い前提条件を見つける最良のアプローチですか?

いくつかの方法を試しましたが、Z3 は初めてで、どのアプローチを採用するか、どのように実装するかがわかりません。

z3py 式のデフォルトの出力は中置表記です。出力形式をポーランド語表記に設定するオプションはありますか?

に似たオプションがあるかもしれないとset_option(html_mode=False)思いますが、設定できるオプションの詳細を説明するサポートドキュメントを見つけることができませんでした。

現在.sexpr()、式の内部表現を取得するために使用しています。ただし、これにはフィルタリングする必要がある追加情報が含まれているため、解析時にオーバーヘッドが発生します。

これは私が現在http://rise4fun.com/Z3Py/BNn2で取り組んでいる例です

[[N ≤ 4, N ≥ 2]]

として印刷したい <= N 4, >= N 2

印刷の出力を変更するために設定できるオプションはありますか? または、表現を使用するための最良のアプローチはあり.sexpr()ますか?

次のコードを使用して、量指定子のない数式を取得しようとしています。

しかし、私は出力を取得しています:

私のコードで何が起こるか教えてください。どうもありがとう。

与えられた 2 つの方程式c == a + 4とt == c + b、if a == -4、 then t == b。私は反対のことをt == bしようとしていますa.

ForAllとImpliesでこれを行うコードを以下に示します。

ただし、上記のコードを実行するとUnsatが返されます。これは -4 (または 0xfffffffc) を返すと予想されるので、かなり混乱しています。

私が間違っている場所はありますか？

ありがとう！