Определение функций в Z3Py, которые возвращают true для одних входов и false для других

Question

Я пытаюсь определить функцию, которая будет возвращать true, если два объекта связаны, и false в противном случае. В примере (см. Рисунок), где узел a подключен к узлу b и c, но нет соединения между b и c Я хочу, чтобы функция вела себя так:

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

Таким образом, мой вопрос можно разделить на два подвопроса:

a) Как бы я определил такую ​​функцию в целом с помощью python API Z3 (z3py), учитывая, что я предоставлю все возможные назначения для функция upfront.

b) можно ли определить функцию таким образом, чтобы я приводил только случаи, когда функция оценивается как true (т.е. только для связанных узлов), а затем как-то говорю, что эта функция должна принимать значение false во всех остальных случаях.

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]

, но обратите внимание, что это назначение никогда не будет содержать пару b, c в соответствии с запросом.

Answer 2

псевдоним правильно, вы можете просто объявить сигнатуру функции и реализацию , как вам угодно. Другими словами, оценка функции зависит от вас.