python - 在 Z3Py 中定义对某些输入返回 true 对其他输入返回 false 的函数

Question

我正在尝试定义一个函数，如果两个对象连接，则返回 true，否则返回 false。在示例（参见图片）中，节点 a 连接到节点 b 和 c，但 b 和 c 之间没有连接，我希望函数的行为如下：

connected(a, b) = true
connected(a, c) = true
connected(b, c) = false

所以我的问题可以分为两个子问题：

a) 考虑到我会预先为函数提供所有可能的分配，我将如何使用 Z3 (z3py) 的 python api 通常定义这样的函数。

b) 是否有可能以某种方式定义一个函数，我只提供函数评估为真（即仅适用于连接的节点）的情况，然后以某种方式说，该函数在所有其他情况下应该评估为假.

标签： pythonz3z3py

Answer 1

当然：

from z3 import *

Object, (a, b, c) = EnumSort('Object', ('a', 'b', 'c'))

connections = [(a, b), (a, c)]

def isConnected(x, y):
    return Or([And(x == i, y == j) for (i, j) in connections])

s = Solver()
s.add(isConnected(a, b))
s.add(isConnected(a, c))
print(s.check())

s.add(isConnected(b, c))
print(s.check())

第一个print会说sat，第二个会说unsat，因为b和c没有连接。

您可以轻松地将其推广到任意数量的对象。甚至可以执行以下操作：

s = Solver()
p = Const('p', Object)
q = Const('q', Object)
s.add(isConnected(p, q))
print(s.check())
print(s.model())

这将打印：

sat
[q = b, p = a]

但请注意，此分配将永远不会按照要求包含bpair c。