排序參數包裝函數

Question

假設使用多個內置和用戶定義的Z3排序（例如， Int，Bool，S1，S2，...有沒有一種方法可以編寫一個通用的排序包裝和-wraping函數，這種函數可以從排序A轉換到排序B並返回？例如

(declare-const a S1) 
(declare-const b S2) 
(declare-const c Int) 

(WRAP[S1] b) ; Expression is of sort S1 
(WRAP[S1] c) ; Expression is of sort S1 
(WRAP[Int] (WRAP[S1] c)) ; Expression is of sort Int 

我目前手動覆蓋每個案例，例如，

(declare-fun $boolToInt (Bool) Int) 
(declare-fun $intToBool (Int) Bool) 

(assert (forall ((x Int)) 
    (= x ($boolToInt($intToBool x))))) 

(assert (forall ((x Bool)) 
    (= x ($intToBool($boolToInt x))))) 

這樣的包裝可以自動從一組給定各種各樣的創建，但我寧願可能的一個通用的解決方案。

Answer 1

您可以使用數據類型對「聯合類型」進行編碼。 下面是一個例子：

(declare-sort S1) 
(declare-sort S2) 

(declare-datatypes() ((S1-S2-Int (WRAP-S1 (S1-Value S1)) 
            (WRAP-S2 (S2-Value S2)) 
            (WRAP-Int (Int-Value Int))))) 

(declare-const a S1) 
(declare-const b S2) 
(declare-const c Int) 

(simplify (WRAP-S1 a)) 
(simplify (= (WRAP-S1 a) (WRAP-Int 10))) 
(simplify (S1-Value (WRAP-S1 a))) 
(simplify (is-WRAP-S2 (WRAP-S1 a))) 
(simplify (is-WRAP-S1 (WRAP-S1 a))) 
(simplify (is-WRAP-Int (WRAP-Int c))) 
(simplify (S1-Value (WRAP-S2 b))) 

您可以找到有關在Z3 guide數據類型的詳細信息。數據類型S1-S2-Int有三個構造函數：WRAP-S1,WRAP-S2和WRAP-Int。 Z3自動生成識別器謂詞：is-WRAP-S1，is-WRAP-S2和is-WRAP-Int。訪問器S1-Value,S2-Value和Int-Value用於「解構」S1-S2-Int值。例如，全部爲a,(S1-Value (WRAP-S1 a)) = a。 (S1-Value (WRAP-S2 b))的值未指定。在這種情況下，Z3將S1-Value視爲未解釋的功能。

順便說一句，公理

(assert (forall ((x Int)) 
    (= x ($boolToInt($intToBool x))))) 

相當於假。它本質上是試圖將整數注入到布爾值中。