4

Z3 の Python API を使用して量指定子の削除を実行するにはどうすればよいですか? チュートリアルとAPIを確認しましたが、どうにかできませんでした。

存在量指定子を含む式があり、この量指定子が削除されるように、Z3 に新しい式を提供してもらいたいです。私は本質的にこれと同じことをしたい:

Z3で変数を非表示にする方法

ただし、Python インターフェイスを使用します。また、私の式は線形演算です。

ありがとう！

追加: 量指定子の削除を行った後、量指定子のない式を別の式に「追加」します。したがって、戦術を利用する場合、サブゴール (戦術の出力) を線形演算の式に変換する方法はありますか?

4

3 に答える 3

5

これには量指定子の削除タクティックを使用できます (Tactic.apply docstring を参照してください)。

from z3 import Ints, Tactic, Exists, And
x, t1, t2 = Ints('x t1 t2')
t = Tactic('qe')
print t(Exists(x, And(t1 < x, x < t2)))
于 2013-07-29T08:09:42.400 に答える
0

reduce の Redlog を使用した可能な解決策:

ここに画像の説明を入力

于 2013-07-29T19:42:42.367 に答える