由于这个问题很难描述，因此我将使用一个小例子来描述我的问题。
假设有一个命题公式集，其元素是 bool 变量a，b和c。
当使用z3获取此公式集的真值分配时，是否存在某种方法来设置变量的优先级？我的意思是，如果优先级是a> b> c，则在搜索过程中z3首先假定a为真，如果a不可能为真，则假定b为真，依此类推。换句话说，如果z3给出了真值分配:不是在上述优先级下的a，b，c，则意味着a不可能为真，因为a与b相比具有较高的优先级。希望我能清楚地描述这个问题。
最佳答案
在当前版本(v4.3.1)中，没有简单的方法可以做到这一点。我看到的唯一方法是修改/修改Z3源代码(http://z3.codeplex.com)。我们同意，设置优先级对于某些应用程序是有用的功能，但是存在一些问题。
首先，Z3在解决问题之前应用了几种转换(也称为预处理步骤)。变量被创建和消除。因此，对于原始问题的案例分割优先级对于由Z3解决的实际问题(应用所有转换后生成的问题)可能没有意义。
一个引人注目的例子是仅包含位向量的公式。默认情况下，Z3会将这个公式简化为命题逻辑，并调用命题SAT解算器。通过这种减少，消除了所有位向量变量。
Z3是求解器和预处理器的集合。默认情况下，Z3将自动为用户选择一个求解器。其中一些求解器使用完全不同的算法。因此，所提供的优先级对于正在使用的求解器可能没有用。
正如GManNickG所指出的，可以为特定求解器设置相位选择策略。有关其他详细信息，请参见他的评论中提供的帖子。
关于z3 - 我可以在z3中设置 bool 变量的优先级吗？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/14234826/