z3 - 我们可以在 Z3 中定义关系吗？

Question

我是 z3 SMT 求解器的新手。我需要定义一个关系，而不是一个函数。我的意思是一个可以返回多个值的函数。我查了教程，找不到任何东西。如果您能在这方面帮助我，我将不胜感激。

谢谢你。

Answer 1

使用支持ArrayEx理论的逻辑之一，它提供了数组排序和关联函数来操作数组。然后，您可以让您的函数返回数组值，该数组值可以包含任意多个 Ints 或 Bool 或其他任何内容。

本 SMT 教程是一个很好的资源，可将许多 SMT 详细信息集中到一个地方。

Answer 2

我认为以下示例可能是您要寻找的：

(define-fun sqrt ((a Int) (b Int)) Bool
    (= (* b b) a)
)
(declare-const a  Int)
(declare-const b1 Int)
(declare-const b2 Int)
(assert (sqrt a b1))
(assert (sqrt a b2))
(assert (not (= b1 b2)))
(check-sat)
(get-model)

当我调用 z3 时，我得到：

$ z3 -smt2 rel.smt
sat
(model 
  (define-fun b2 () Int
    2)
  (define-fun a () Int
    4)
  (define-fun b1 () Int
    (- 2))
)

该sqrt关系只是一组有序对：{(a,b) | a == b*b}. 并且两者都(4,2)属于(4,-2)这种关系。在 SMT 措辞中，这意味着两者sqrt(4,2)和sqrt(4,-2)都是true。这对应于您的问题的措辞，其中4可以有多个值。不幸的是，其他答案（例如使用的答案）foo 并不能真正处理关系，而是要求求解器在两个函数之间进行选择。

Answer 3

从某种意义上说，SMT“自然地”支持关系编程。您可以简单地分离参数的可能值，从而获得所需的结果。就像是：

(declare-fun foo ((Int)) Int)
(assert (or (= (foo 3) 4) (= (foo 3) 5)))
(check-sat)
(eval (foo 3))   ; might produce 4 of 5
(assert (distinct (foo 3) 4))
(check-sat)
(eval (foo 3))   ; will produce 5
(assert (distinct (foo 3) 5))
(check-sat)      ; will declare unsat 

这就是你说的foo当应用于 时3，可以产生4或5。然后你可以断言“进一步”的事实来根据需要限制空间；或者让它免费。您可以使用此技巧将本质上建模foo为关系；使 SMT 求解器表现为关系编程语言。

当然，您真正想要如何建模关系实际上取决于手头的问题。以上可能不是您问题的最佳选择。