如何聲明或檢查一對一的功能？

Question

在Z3的C++ API，一個功能被delared爲：

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

這意味着函數採取輸入(int, int)並返回int。

我可以聲明一對一（雙射）函數還是可以強制函數是一對一（雙射）？

Answer 1

據我所知，沒有內建的方式來聲明函數是雙射。但是，您可以自己axiomatise它：

(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)和(not (= x1 x2))。不過，我不確定在這裏可以找到好的模型。