1

我需要一个支持push和pop. SolverFor()所以我使用该函数生成一个。由于某些断言只是常量断言，例如a == 2，我想propagate-values在调用之前使用该策略进行简化solver.check()。所以我的问题是：

有没有办法在求解器上应用策略？

我知道我可以为Goal. 但在我看来，Goal不支持pushand pop。

任何评论表示赞赏。谢谢。

4

1 回答 1

2

战术对象仅支持非增量求解。他们也没有提供push和pop方法。它们主要用于解决不平凡的问题。为方便起见，我们提供了一个将策略对象包装为求解器对象的 API。wrapping 是非常基础的，wrapper 对象保留了一堆断言，每一个check都是使用 Wrapped 策略从头开始解决的。

Z3 中的默认Solver对象是通用求解器。默认情况下，它执行常量传播。我们可以控制这个求解器设置参数的行为。在未来的版本中，我们将为求解器对象提供额外的控制。我们将能够使用可用策略的子集来自定义求解器对象。

话虽如此，您是对的，该Goal对象不支持pushand pop。在内部，Goal对象支持以恒定时间运行的复制操作。在内部，共享数据结构用于节省内存。我将在未来的版本中明确公开此功能。请注意，此功能只是节省空间/内存。解决每个目标的努力不会被节省。我说“显式暴露”是因为可以使用以下技巧来模拟功能：

def copy_goal(g):
  return Tactic('skip')(g)[0]

x = Int('x')
g = Goal()
g.add(x < 10)
g.add(x > 0)
g1 = copy_goal(g)
g1.add(x != 5)
print g
print g1

上述示例可在以下网址获得：http ://rise4fun.com/Z3Py/O3RO

备注：该策略smt实现了我上面提到的通用求解器。

于 2012-09-17T20:51:32.317 回答