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)

试一试 online here .

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