1

ユーザー理論プラグインを実装しています。一部のモデルを整理するために、ユーザー理論の不整合をテストしたいと思います。

より具体的には、私の理論でxは、はユーザーの種類のセットの変数でありf、セットのサイズを返す関数です。私には2つのアサーションがあります：x = set1 OR x = set2とf x > 2。のサイズset1が1で、のサイズset2が3であるとします。

検索では、Z3がx = set1最初になります。f x = 1したがって、INT部分で矛盾する別のアサーションを追加できます。現在の割り当てを無効にし、Z3をバックトラックさせて他のオプションを試すことができるように、不整合をテストしたいと思います。

私の質問は、どうすればそれができるかということです。

私は3つのアプローチを試しました：

（1）を使用してアサーションf x = 1を直接追加しZ3_theory_assert_axiom()ます。その後、検索はすぐに終了し、UNSATを返します。

（2）現在の状況を確認するための前提としてZ3_check_assumptions()withを使用してみました。f x = 1しかしZ3_check_assumptions()、そのような複合式は許可されていません。だから、それは解決策になることはできません。

（3）最初にコンテキストをプッシュし、でアサーションf x = 1を追加しZ3_assert_cnstr()、で整合性をテストしてから、Z3_check_and_get_model()プッシュしたばかりのコンテキストをポップします。テストでは、一貫性がない場合は、で現在の割り当てを取得Z3_get_context_assignment(ctx)し、否定された割り当てをアサートしてバックトラックをトリガーします。私が観察しているのは、Z3は不整合を検出しますが、現在の割り当てには、のようなサイズ部分に関するアサーションのみが含まれているということ(= 1 (f x))です。言い換えれば、のようなユーザー理論に関するアサーション(= x set1) and not (= x set2)が欠落しています。したがって、現在の割り当てを無効にしても、バックトラック後、Z3x = set1は他のオプションの代わりに試行しますx = set2。

どこが間違っていたの？ありがとう！

4

1 に答える 1

2

最初のオプションは、コールバックのユーザー理論プラグインのZ3_theory_assert_axiom（）のみを使用する必要があります。また、トートロジー、つまり現在の割り当てとは無関係に真である公理のみを主張する必要があります。だから主張する代わりに

f x = 1

あなたは主張する必要があります

x = set1 => f x = 1

（私が理解したと仮定して）この式は関係なく真であるため。次のように主張することもできます。

f set1 = 1

（仮定すると、もう一度理解しました）、これは、他の変数が保持されている場合、y = set1＆fy>1のブランチも閉じます。より一般的には、最も強力な理論公理を主張して、関連する多くのブランチを削除する必要があります。しかし、理論の公理は真実でなければならず、検索のローカルブランチ内にとどまるだけではありません。

于 2012-08-30T00:15:15.840 に答える