問題タブ [z3py]

この z3py コード (オンライン コード) を標準の SMTLib 形式に変換したいと考えています。set options プロパティ " (set-option :produce-models true) (set-option :timeout 4000)"を除いて、すべてが SMTLib 形式に変換されます。なぜ機能しないのですか？変換コードは Leonardo de Moura によって提案されました。

出力を次のようにしたい-

ありがとう

私は約 20,000 の制約を作成し、私のマシンではそれらを解決するのに約 3 分かかります。さまざまな種類の制約があり、以下に例を挙げて説明します。アサーションをhttp://filebin.ca/vKcV1gvuGG3にアップロードしました。

より大きな制約システムを解決することに興味があるため、プロセスをスピードアップしたいと考えています。適切な戦術を使用するなどして、それらをより迅速に解決する方法について提案があるかどうかを尋ねたいと思います. 戦略のチュートリアルから、私は戦術を知っていますが、戦術を適用することによってプラスの違いが得られないようです...

liツリーのラベルです。1 番目のタイプは、ラベルの値に制限を加えます。通常、ラベル値は 10 ～ 20 の異なる値の範囲です。

2 番目のタイプは、異なるラベルを相互に関連付けます。

3 番目のタイプは、関数f: Int --> Int(f: BitVector --> BitVector完全性を欠く場合は ) を定義して関連付けます。ここで、bound_{s, v}は単なる関数名であり、nはノードの ID です。目標は、関数への満足のいく割り当てを見つけることboundです。

最後のタイプは、境界が必要か ( >= 0)、不要か ( == -1, )を決定します。

また、一部の初期状態では境界が必要であるという要件もあります。

実行可能ファイルの説明:最初の 2 ～ 3 行で、スクリプトはソルバーを開始し、z3 をインポートし、最後の行で呼び出しますprint s.check()

Z3 と python を使用して、関数のコドメインを取得する必要があります。それは可能ですか？具体的には、f(var) = (var + 1) << 1 のような式があり、式が想定する値の範囲を知りたいとします。何か案は？

リンク:
Z3 定理証明者
picosat と pyhton バインディング

Z3 を SAT ソルバーとして使用しました。より大きな数式ではパフォーマンスの問題があるように思われるため、ピコサットをチェックして、それがより高速な代替手段であるかどうかを確認したかったのです. 私の既存の python コードは、z3 構文で命題式を生成します。

出力/結果

ただし、Picosat は、次の例に示すように、数値のリスト/配列を使用します (「clauses1」: 6 は変数 P を参照し、-6 は「非 P」を意味するなど)。

CNF の式を表す Z3 変数 (コード例の変数 "f" など) を、picosat が CNF の式を表すために使用する前述の形式に変換するための簡単なソリューションとして何をお勧めしますか? Z3 の python API を実際に使用してみましたが、ドキュメントが不十分で、自分で問題を解決することはできませんでした。

(上記の例は単に概念を示しているだけであることに注意してください。変数 C で表される式は動的に生成され、z3 で直接効率的に処理するには複雑すぎます)