我想构建一个 z3 解算器来打印范围而不是打印所有可能的值

Question

假设我有一个整数表达式

x

。因此，如果我不应用任何约束，该整数的最小值和最大值将是

INT_MIN

和

INT_MAX

。但假设我应用一个约束 a，使得 a 暗示

!(m>=0 && m<=10)

，这样我的模型就会生成诸如

INT_MIN

到 99 和 501 到

INT_MAX

的答案。它会给出它的所有可能的值。但它不是打印所有可能的值，而是打印有效范围，并且可以适用于多个约束。

考虑代码。

#include <iostream>
#include <z3++.h>

using namespace z3;
using namespace std;

int main() {

    context c;
    solver s(c);

    expr x = c.int_const("x");
    expr a = c.bool_const("a");

    expr range_constraint = (x >= -100 && x <= 100);


    expr constraint = implies(a, (x >= 0 && x <= 10));

    s.add(range_constraint);
    s.add(!constraint);

    while (s.check() == sat) {
       
        model m = s.get_model();

    
        cout << m.eval(x) << endl;

   
        expr current_solution = (x == m.eval(x));

        
        s.add(!current_solution);
    }

    return 0;
}

我希望输出为 [-100,-1][11,100]

Answer 1

相关：https://stackoverflow.com/a/63380049/936310

长话短说，不，一般来说你不能这样做。 SMT 求解器找到一个特定的令人满意的解决方案（或许多解决方案，如果您对其进行编程来这样做），但它不会为您提供解决方案可能所在的符号“范围”。一般来说，这样做远远超出了 SMT 求解器的能力范围。 （也就是说，这是一个更难的问题。）

我还应该补充一点，SMT 中的

int

值是无界的。它不是机器整数：它是数学整数。如果您想要机器整数，您应该使用位向量。

话虽如此，如果您对这些范围有先验知识，您就可以获得范围。例如，如果您以某种方式知道某些常量 x <= c0

 和 

x >= c1

 的 

c0

 和 

c1

，那么您可以要求 SMT 求解器使用量词找到这些常量。 （这是否具有性能完全取决于特定问题：添加量词使逻辑半可判定；因此 z3 可能会响应 

unknown

 或无法终止。）但重要的一点是，这必须是先验的：即，您必须拥有有关求解器之外的问题的附加信息（也许通过其他一些数学/符号分析），并且您应该有一个范围的框架。然后您可以要求 SMT 求解器找到相关常数。

但是你描述问题的方式，听起来像是你希望 z3 “自动”给你这些范围；这不是它能为你做的事情。没有自动方法来确定此类范围。