z3 - 使用 z3 消除表达式中的“not”

Question

我尝试使用脚本http://rise4fun.com/Z3/XwGt消除表达式中的“not”但是，它不起作用，结果仍然没有，有人可以帮我吗？

Answer 1

您示例中的输出目标采用简化公式。任何目标都没有多余的断言。Z3 简化形式总是使用非严格不等式，例如t1 <= t2和t1 >= t2。严格的不等式，例如t1 < 0使用否定编码。也就是说，t1 < 0被编码为not t1 >= 0。这个想法是减少用于编码大公式的原子数量。

了解为什么需要消除not输出中的 s 会很有用。如果有一个有用的应用程序，我们将包括一个执行转换的新策略（在下一个版本中）。