Z3:使用比较运算符(<，<=，.)关于z3::expr

Question

我将数字存储为z3::expr，并希望对它们进行比较。我尝试了以下几点：

z3::context c;
z3::expr a = c.real_val("0");
z3::expr b = c.real_val("1");
z3::expr comp = (a < b);
std::cout << comp.is_bool() << std::endl;
std::cout << comp.bool_value() << std::endl;

我有点困惑，为什么comp.bool_value()是假的？

如果我使用的是一个求解器，那么所有的事情都会像预期的那样工作：

z3::solver s(c);
s.add(comp);
std::cout << s.check() << std::endl;

我不得不比较一下z3::expr的相对频率，有什么快速的方法可以这样做呢？在我看来，使用一个解算器是一种很大的开销。

Answer 1

<运算符(以及几乎所有其他操作符)简单地将决策推送给求解者:也就是说，它是一个符号表达式，它在运行时不进行“计算”，而是创建一个表达式，在调用求解程序时，该表达式将对任意表达式进行比较。

话虽如此，在某些情况下，您可以使用简化器来实现您想要的目标。如果你尝试：

  z3::expr simpComp = comp.simplify();
  std::cout << simpComp.bool_value() << std::endl;

你会看到它会为你打印1。但是，您不应该指望这个简化器能够减少这样的任意表达式。对于最简单的情况，它可以完成工作，但如果你有更复杂的表达式，它就会放弃。

通常，一旦构造了表达式，就必须等到调用了求解器，并检查结果模型(如果有的话)。

请注意，在某些情况下，您可以构建自己的函数来做一些固定的折叠。例如，对于Bool值(因为它们可以完全用C++表示)、各种大小的位向量(直到机器字大小)、浮动等等，这都是可能的。但对于reals (因为z3 reals是无限精度的，不能直接用C++表示)和整数(因为它们是无界的)，这是可能的。但是这不是一件小事，除非您非常熟悉z3的内部结构，否则我建议您不要沿着这条路走下去。

底线:如果你有很多这样的常量，可以折叠:看看你是否能重新架构你的程序，这样你一开始就不会创建real_val；并且把它们作为常量保存，并且只在你不再能保持它们的时候将它们转换成Z3-表达式。在某些情况下，您可以依赖simplify，但也不要期望它具有很强的性能。