1

随后在不同的变量和公式上调用 Z3py 的 Exists 函数时，我得到完全相同的结果。这是某种Python问题还是Z3在这里坏了？怎么修？以下最小示例说明了该问题：

from z3 import *
a, a0, a1, b, b0, b1 = Ints('a a0 a1 b b0 b1')
x, y = Bools('x y')
s = Solver()
formula = Implies(x, And(a>0,b1<0))
substitution1 = substitute(formula,(a1,a0),(b1,b0))
substitution2 = substitute(formula,(a1,a0),(b1,b0),(a,a1),(b,b1))
print substitution1
print substitution2
exist1 = Exists([a,b],substitution1)
exist2 = Exists([a1,b1],substitution2)
print exist1
print exist2

输出：

Implies(x, And(a > 0, b0 < 0))
Implies(x, And(a1 > 0, b0 < 0))
Exists([a, b], Implies(x, And(a > 0, b0 < 0)))
Exists([a, b], Implies(x, And(a > 0, b0 < 0)))
4

1 回答 1

0

感谢您报告。Z3 实际上对此是正确的，但输出令人困惑。在内部，Z3 使用 deBrujin 索引，绑定变量的名称并不重要。当创建具有相同主体（和模式、no_patterns 等）的量词时，将使用之前看到的完全相同的表达式，以避免必须解决与之前相同的量化约束。这造成了令人困惑的情况，因为突然绑定变量的名称似乎发生了变化。

在此处给出的示例中，两个量词的主体确实相同，变量的名称无关紧要。Z3 可以为这些变量使用任何名称，但它选择使用第一次创建量词时使用的名称。我们可以禁用它，例如，通过添加

compare_arrays(to_quantifier(n1)->get_decl_names(),
               to_quantifier(n2)->get_decl_names(),
               to_quantifier(n1)->get_num_decls()) &&

在 src/ast/ast.cpp:470。然而，这可能会对 Z3 在某些基准测试中的性能产生负面影响，因此我不会进行此更改。如果您想使用它，当然可以将其添加到 Z3 的本地副本中。

于 2014-05-29T13:43:17.883 回答