使用另一个求解器（）作为输入答案

【问题标题】：Use another solver() as input使用另一个求解器（）作为输入
【发布时间】：2022-01-05 06:29:24
【问题描述】：

我想使用现有的solver() 作为输入。例如，我有三个求解器：

Tie, Shirt = Bools('Tie Shirt')
s_one = Solver()
s_one.add(Or(Tie, Shirt))
s_two = Solver()
s_two.add(Or(Not(Tie), Shirt))
s_three = Solver()
s_three.add(Or(Not(Tie), Not(Shirt)))

现在我想将所有求解器组合成这样的东西：（这个脚本不起作用，只是为了说明我的意思）

s_four = Solver()
s_four.add(s_one, Or(s_two, s_three))

我该怎么做？

【问题讨论】：

那么，告诉您如何将s_one 结果与Or(s_two, s_three) 结果结合起来的规则是什么？
@KarlKnechtel 这个问题对于 SMT 求解器来说确实有意义。告诉您如何组合它们的规则在某种意义上是每个求解器中断言的“元”合取和析取。对于最终用户程序来说，这是一件奇怪的事情，但我可以想象构建在 z3 之上的库可能需要这种工具。

标签： python z3

【解决方案1】：

这有点奇怪，因为您已经知道要添加的断言是什么。但我可以想象你有来自程序不同部分的求解器的场景，或者如果你正在 z3 本身之上构建一个库。

要实现您想要的，请使用assertions 方法：

from z3 import *

Tie, Shirt = Bools('Tie Shirt')
s_one = Solver()
s_one.add(Or(Tie, Shirt))

s_two = Solver()
s_two.add(Or(Not(Tie), Shirt))

s_three = Solver()
s_three.add(Or(Not(Tie), Not(Shirt)))

s_four = Solver()
s_four.add(s_one.assertions(), Or(list(s_two.assertions()) + list(s_three.assertions())))

print(s_four.sexpr())

打印出来：

(declare-fun Shirt () Bool)
(declare-fun Tie () Bool)
(assert (or Tie Shirt))
(assert (or (not Tie) Shirt (not Tie) (not Shirt)))

【讨论】：