由于这个问题有点难以描述,我将用一个小例子来描述我的问题.假设有一个命题公式集,其元素是布尔变量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指出的那样，可以为特定求解器设置相选择策略。有关更多详细信息，请参阅他的评论中提供的帖子。