1

pushとをサポートする特定のロジックのソルバーが必要popです。そのため、関数を使用して生成しSolverFor()ます。一部のアサーションは のように単なる定数アサーションであるため、を呼び出す前に単純化するためa == 2の戦術を使用したいと思います。だから私の質問は：propagate-valuessolver.check()

ソルバーに戦術を適用する方法はありますか?

私はそれができることを知っていGoalます。しかし、それは私にはサポートされていGoalないようです。pushpop

どんなコメントでも大歓迎です。ありがとう。

4

1 に答える 1

2

戦術オブジェクトは非増分解決のみをサポートします。pushまた、popメソッドも提供していません。それらは主に、重要な問題を解決することを目的としています。便宜上、戦術オブジェクトをソルバー オブジェクトとしてラップする API を提供します。ラッピングは非常に基本的なもので、ラッパー オブジェクトはアサーションのスタックを保持し、すべてcheckがラップされた戦術を使用してゼロから解決されます。

Z3のデフォルトSolverオブジェクトは汎用ソルバーです。デフォルトでは、一定の伝播を実行します。このソルバー設定パラメーターの動作を制御できます。将来のバージョンでは、ソルバー オブジェクトに追加のコントロールを提供する予定です。利用可能な戦術のサブセットを使用して、ソルバー オブジェクトをカスタマイズできます。

そうは言っても、あなたは正しいです。オブジェクトはand をGoalサポートしていません。内部的には、オブジェクトは一定時間で実行されるコピー操作をサポートしています。内部的には、メモリを節約するために共有データ構造が使用されます。この機能は、将来のバージョンで明示的に公開します。この機能はスペース/メモリを節約するだけであることに注意してください。それぞれの目標を解決するための努力は節約されません。「明示的に公開する」と言ったのは、次のトリックで機能をシミュレートできるためです。pushpopGoal

def copy_goal(g):
  return Tactic('skip')(g)[0]

x = Int('x')
g = Goal()
g.add(x < 10)
g.add(x > 0)
g1 = copy_goal(g)
g1.add(x != 5)
print g
print g1

上記の例は、http: //rise4fun.com/Z3Py/O3ROで入手できます。

注意: このタクティックはsmt、前述の汎用ソルバーを実装しています。

于 2012-09-17T20:51:32.317 に答える