c++ - 如何声明或检查一对一的函数？

Question

在 z3 的 C++ API 中，函数声明为：

func_decl f = function("f", I, I, I); 

这意味着一个函数接受输入(int, int)并返回int。

我可以声明一个一对一（双射）函数还是强制一个函数是一对一（双射）？

Answer 1

据我所知，没有内置的方法可以将函数声明为双射。但是，您可以自己公理化它：

(declare-sort X)
(declare-sort Y)

(declare-fun f (X) Y)

(assert (forall ((y Y))
  (exists ((x X))
    (and
      (= (f x) y)
      (forall ((z X))
        (implies
          (not (= x z))
          (not (= (f z) y))))))))

并按如下方式使用它：

(declare-const x1 X)
(declare-const x2 X)
(declare-const y1 Y)
(declare-const y2 Y)

(assert (= (f x1) y1))
(check-sat) ; sat

(push)
  (assert (= (f x2) y1))
  (check-sat) ; sat
(pop)

(assert (not (= x1 x2)))
(check-sat) ; sat

(push)
  (assert (= (f x2) y1))
  (check-sat) ; unsat
(pop)

在这里在线尝试。

我不确定这种编码的性能如何。交替量词经常在自动定理证明中引起问题，而上面的公理甚至没有模式/触发器。我的直觉是，只要您提供“足够”的信息，例如 、 和 ，公理x1就可以x2了。不过，我不确定模型查找在这里的效果如何。(= (f x1) y1)(not (= x1 x2))