如何测试用户理论插件中的不一致性？
我正在实现一个用户理论插件。我想测试用户理论中的不一致性，以修剪一些模型。
更具体地说，在我的理论中，x是用户类型集合的变量，f是返回集合大小的函数。我有两个断言：x = set1 OR x = set2和f x > 2。假设set1的大小为1，set2的大小为3。
在搜索中，Z3首先使用x = set1。所以我可以添加另一个断言f x = 1，这个断言在INT部分是不一致的。我想测试不一致性，这样我就可以否定当前的赋值，让Z3回溯并尝试其他选项。
我的问题是，我如何做到这一点。
我尝试了3种方法：
(1)直接使用Z3_theory_assert_axiom()添加断言f x = 1。然后搜索立即终止，返回UNSAT。
(2)我尝试使用带有f x = 1的Z3_check_assumptions()作为检查当前上下文的假设。但是Z3_check_assumptions()不允许这样的复合公式。因此，它不可能是解决方案。
(3)首先推送context，用Z3_assert_cnstr()添加断言f x = 1，用Z3_check_and_get_model()测试一致性，然后弹出刚刚推送的context。在测试中，如果不一致，我使用Z3_get_context_assignment(ctx)获取当前赋值，并断言被否定的赋值以触发回溯。我观察到的是，Z3确实发现了不一致之处，但当前赋值只包含关于(= 1 (f x))之类的大小部分的断言。或者换句话说，关于像(= x set1) and not (= x set2)这样的用户理论的断言是缺失的。因此，即使我否定了当前赋值，在回溯之后，Z3仍然尝试x = set1而不是另一个选项x = set2。
我哪里错了？谢谢!
回答 1
Stack Overflow用户
发布于 2012-08-30 00:15:16
您应该在回调中仅使用用户理论插件中的第一个选项Z3_theory_assert_axiom()。您还应该只断言重言式，即独立于当前赋值的真实公理。因此，与其断言
f x = 1你应该断言
x = set1 => f x = 1(假设我理解了)，因为这个公式无论如何都是正确的。您还可以断言：
f set1 = 1(假设，我再次理解)，这也会关闭y= set1 &f y>1的分支，对于其他一些变量成立。更广泛地说，您希望断言最强的理论公理，以修剪掉尽可能多的相关分支。但理论公理必须是真实的，而不仅仅是在搜索的局部分支中。
https://stackoverflow.com/questions/12185717
复制相似问题
腾讯云开发者
