1

我正在实现一个用户理论插件。我想测试用户理论中的不一致性来修剪一些模型。

更具体地说，在我的理论中，x它是用户类型集合的变量，并且f是返回集合大小的函数。我有两个断言：x = set1 OR x = set2和f x > 2. 假设 的大小set1为 1， 的大小set2为 3。

在搜索中，Z3x = set1先行。所以我可以添加另一个 assertion f x = 1，这将在 INT 部分不一致。我想测试不一致，以便我可以否定当前分配，让 Z3 回溯并尝试其他选项。

我的问题是我该怎么做。

我尝试了 3 种方法：

f x = 1(1)直接使用添加断言Z3_theory_assert_axiom()。然后搜索立即终止并返回 UNSAT。

(2) 我尝试使用Z3_check_assumptions()withf 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)是缺失的。所以即使我否定了当前的分配，在回溯之后，Z3 仍然尝试 thex = set1而不是 other option 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 回答