z3 - z3.prove 比求解器和检查快得多

Question

我正在使用来自 Codeplex 的最新 z3 主代码，标记为 v4.3.1。

我想要一个这样的函数prove，它有一个有用的返回值并且不打印。所以，我写了看起来很明显的东西：

def prove2(claim):
    s = Solver()
    s.add(Not(claim))
    if s.check() == unsat:
        return True, []
    return False, s.model()

但是，此代码的运行速度比默认prove函数慢得多。

prove（瘦身）的代码src/api/python/z3.py是：

def prove(claim, **keywords):
    s = Solver()
    s.set(**keywords)
    s.add(Not(claim))
    if keywords.get('show', False):
        print s
    r = s.check()
    if r == unsat:
        print "proved"
    elif r == unknown:
        print "failed to prove"
        print s.model()
    else:
        print "counterexample"
        print s.model()

当我添加s.set()到我的代码中时，它很快并且找到了相同的反例。

这里发生了什么？

• 这个空洞的电话是否以s.set()某种方式清除了一些通常不好的选项？
• ..对我的特定测试不利？
• 还有什么？

我试图找出默认的求解器选项是什么，但是str(s) repr(s),s.__dict__和 google 并没有真正帮助。

任何建议表示赞赏！

Answer 1

最好的猜测是默认选项在我的特定情况下表现不佳，可能是因为随机数差异或其他一些不确定的内部状态。