如何使用Z3 SMT-LIB獲得團體表示Z3和Z4

Question

集團Z3已經款項

使用下面的Z3 SMT-LIB代碼下表是可以得到Z3的表示：

(set-option :mbqi true) 
(declare-sort S) 
(declare-fun f (S S) S) 
(declare-const a S) 
(declare-const b S) 
(declare-const c S) 
(assert (forall ((x S) (y S)) 
      (= (f x y) (f y x)))) 
(assert (forall ((x S)) 
      (= (f x a) x))) 
(assert (= (f b b) c)) 
(assert (= (f b c) a)) 
(assert (= (f c c) b)) 
(check-sat) 
(get-model) 

相應的輸出是

sat 
(model 
;; universe for S: 
;; S!val!1 S!val!0 S!val!2 
;; ----------- 
;; definitions for universe elements: 
(declare-fun S!val!1() S) 
(declare-fun S!val!0() S) 
(declare-fun S!val!2() S) 
;; cardinality constraint: 
(forall ((x S)) (or (= x S!val!1) (= x S!val!0) (= x S!val!2))) 
;; ----------- 
(define-fun b() S S!val!0) 
(define-fun c() S S!val!1) 
(define-fun a() S S!val!2) 
(define-fun f ((x!1 S) (x!2 S)) S 
(ite (and (= x!1 S!val!0) (= x!2 S!val!0)) S!val!1 
(ite (and (= x!1 S!val!0) (= x!2 S!val!1)) S!val!2 
(ite (and (= x!1 S!val!1) (= x!2 S!val!1)) S!val!0 
(ite (and (= x!1 S!val!1) (= x!2 S!val!0)) S!val!2 
(ite (and (= x!1 S!val!0) (= x!2 S!val!2)) S!val!0 
(ite (and (= x!1 S!val!2) (= x!2 S!val!0)) S!val!0 
(ite (and (= x!1 S!val!2) (= x!2 S!val!1)) S!val!1 
(ite (and (= x!1 S!val!1) (= x!2 S!val!2)) S!val!1 
    x!1))))))))) 
) 

運行該代碼的在線here

組Z4具有和的下表：

採用下述Z3 SMT-LIB代碼可以獲得Z4的表示：

(set-option :mbqi true) 
(declare-sort S) 
(declare-fun f (S S) S) 
(declare-const a S) 
(declare-const b S) 
(declare-const c S) 
(declare-const d S) 
(assert (forall ((x S) (y S)) 
      (= (f x y) (f y x)))) 
(assert (forall ((x S)) 
      (= (f x a) x))) 
(assert (= (f b b) c)) 
(assert (= (f b c) d)) 
(assert (= (f b d) a)) 
(assert (= (f c c) a)) 
(assert (= (f c d) b)) 
(assert (= (f d d) c)) 
(check-sat) 
(get-model) 

相應的輸出是：

sat 
(model 
;; universe for S: ;; S!val!1 S!val!3 S!val!0 S!val!2 
;; ----------- 
;; definitions for universe elements: 
(declare-fun S!val!1() S) 
(declare-fun S!val!3() S) 
(declare-fun S!val!0() S) 
(declare-fun S!val!2() S) 
;; cardinality constraint: 
(forall ((x S)) (or (= x S!val!1) (= x S!val!3) (= x S!val!0) (= x S!val!2))) 
;; ----------- 
(define-fun b() S S!val!0) 
(define-fun c() S S!val!1) 
(define-fun d() S S!val!2) 
(define-fun a() S S!val!3) 
(define-fun f ((x!1 S) (x!2 S)) S 
    (ite (and (= x!1 S!val!0) (= x!2 S!val!0)) S!val!1 
    (ite (and (= x!1 S!val!0) (= x!2 S!val!1)) S!val!2 
    (ite (and (= x!1 S!val!0) (= x!2 S!val!2)) S!val!3 
    (ite (and (= x!1 S!val!1) (= x!2 S!val!1)) S!val!3 
    (ite (and (= x!1 S!val!1) (= x!2 S!val!2)) S!val!0 
    (ite (and (= x!1 S!val!2) (= x!2 S!val!2)) S!val!1 
    (ite (and (= x!1 S!val!1) (= x!2 S!val!0)) S!val!2 
    (ite (and (= x!1 S!val!2) (= x!2 S!val!0)) S!val!3 
    (ite (and (= x!1 S!val!2) (= x!2 S!val!1)) S!val!0 
    (ite (and (= x!1 S!val!2) (= x!2 S!val!3)) S!val!2 
    (ite (and (= x!1 S!val!3) (= x!2 S!val!2)) S!val!2 
    (ite (and (= x!1 S!val!3) (= x!2 S!val!1)) S!val!1 
    (ite (and (= x!1 S!val!1) (= x!2 S!val!3)) S!val!1 
    (ite (and (= x!1 S!val!3) (= x!2 S!val!0)) S!val!0 
    (ite (and (= x!1 S!val!0) (= x!2 S!val!3)) S!val!0 
    x!1)))))))))))))))) 
) 

運行這段代碼在線here

的問題是，如何在原有的代碼插入與Z3和Z4可以使組計算這樣的方式由Z3生成的函數f。非常感謝。

Answer 1

您可以使用命令eval來評估Z3生成的模型中的表達式。例如，可以在(get-model)之後添加以下命令。

(eval (f b b)) 
(eval c) 
(eval (f b (f c b))) 

如果你想通過Z3產生的定義轉換爲可以在另一個系統或語言來評價的功能，那麼我認爲你應該使用Z3編程API（例如，Python的）。這裏是z3.py的一個例子。

>>> f = Function('f', IntSort(), IntSort()) 
    >>> s = Solver() 
    >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 
    >>> s.check() 
    sat 
    >>> m = s.model() 
    >>> m[f] 
    [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 
    >>> m[f].num_entries() 
    3 
    >>> m[f].entry(0) 
    [0, 1] 
    >>> m[f].entry(1) 
    [1, 1] 
    >>> m[f].entry(2) 
    [2, 0]