z3 - 我如何为 Z3py 中的函数分配（断言）值？

Question

我想问一下，如何将以下 Z3 约束转换为 Z3py（Python API）。

        (declare-datatypes () ((S a b c d e f g)))

        (declare-fun fun1 ( S ) Bool)
        (declare-fun fun2 ( S   S ) Bool)


        (assert (forall ((x S)) (= (fun1 x)
        (or
        (= x  a)
        (= x  b)
        (= x  c)
        (= x  d)
        (= x  e)
        (= x  f)
        (= x g)
        ))))

       (assert (forall ((y1 S) (y2 S)) (= (fun2  y1  y2)
       (or
       (and (= y1  a) (= y2  b))
       (and (= y1  c) (= y2  d))
       (and (= y2  e) (= y2  f))
       ))))

Answer 1

您可以通过以下方式对其进行编码：

from z3 import *

S, (a, b, c, d, e, f, g) = EnumSort('S', ['a', 'b', 'c', 'd', 'e', 'f', 'g'])

fun1 = Function('fun1', S, BoolSort())
fun2 = Function('fun2', S, S, BoolSort())

s = Solver()

x = Const('x', S)
s.add(ForAll([x], fun1(x) == Or(x == a, x == b, x == c, x == d, x == e, x == f, x == g, x == e)))

y1, y2 = Consts('y1 y2', S)
s.add(ForAll([y1, y2], fun2(y1, y2) == Or(And(y1 == a, y2 == b), And(y1 == c, y2 == d), And(y1 == e, y2 == f))))

print(s.check())
print(s.model())

请注意，fun1andfun2本质上是宏。因此，我们可以避免使用量词并将它们定义为：

def fun1(x):
    return Or(x == a, x == b, x == c, x == d, x == e, x == f, x == g, x == e)

def fun2(y1, y2):
    return Or(And(y1 == a, y2 == b), And(y1 == c, y2 == d), And(y1 == e, y2 == f))