Z3中的排序名稱問題

Question

在之前的帖子中Z3 group使用名爲S的排序來證明某些組公理集。請運行代碼code with sort named S但現在，當排序的名稱更改爲G時，代碼不起作用。請在線上查找問題code with sort named G有必要使用名稱S進行排序，或者這是Z3的問題？請告訴我。

Answer 1

請讓ne知道以下代碼與名爲G的排序是否正確。非常感謝

(declare-sort G) 
(declare-fun f (G G) G) 
(declare-const a G) 
(declare-const b G) 
(declare-const c G) 
(assert (forall ((x G) (y G)) 
      (= (f x y) (f y x)))) 
(assert (forall ((x G)) 
      (= (f x a) x))) 
(assert (= (f b b) c)) 
(assert (= (f b c) a)) 
(assert (= (f c c) b)) 
(check-sat) 
(get-model) 

(push) 
;; prove the left-module axiom 
(assert (not (forall ((x G)) (= (f a x) x)))) 
(check-sat) 
(pop) 

(push) 
;; prove the right-module axiom 
(assert (not (forall ((x G)) (= (f x a) x)))) 
(check-sat) 
(pop) 


(declare-fun x() G) 
(declare-fun y() G) 
(declare-fun z() G) 

(push) 
;; prove the right-inverse axiom 
(assert (not (=> (and (or (= x a) (= x b) (= x c))) (exists ((y G)) (= (f x y) a))))) 
(check-sat)     
(pop) 

(push) 
;; prove the left-inverse axiom 
(assert (not (=> (and (or (= x a) (= x b) (= x c))) (exists ((y G)) (= (f y x ) a))))) 
(check-sat)     
(pop) 

(push) 
;; prove the associativity axiom 
(assert (not (=> (and (or (= x a) (= x b) (= x c)) (or (= y a) (= y b) (= y c)) 
        (or (= z a) (= z b) (= z c))) 
      (= (f x (f y z)) (f (f x y) z))))) 

(check-sat) 
(pop)  

(push) 
;; prove the commutative property 
(assert (not (=> (and (or (= x a) (= x b) (= x c)) (or (= y a) (= y b) (= y c))) 

      (= (f x y) (f y x))))) 

(check-sat) 
(pop) 

和相應的輸出是預期

sat unsat unsat unsat unsat unsat unsat 

請運行該代碼在線here

Answer 2

問題的簡化版本。

$ z3 -version 
Z3 version 4.3.1 

使用名稱S：

$ cat S.smt 
(declare-sort S) 
(declare-fun f (S S) S) 
(declare-const a S) 
(declare-const b S) 
(assert (= (f a a) a)) 
(assert (= (f a b) b)) 
(assert (= (f b a) b)) 
(assert (= (f b b) a)) 
(check-sat) 

;; Restrict the search to models of size at most 2. 
(assert (forall ((x S)) (or (= x a) (= x b)))) 

;; Associativity 
(assert (not (forall ((x S) (y S) (z S)) (= (f x (f y z)) (f (f x y) z))))) 
(check-sat) 

$ z3 -smt2 S.smt 
sat 
unsat 

使用名稱G：

$ cat G.smt 
(declare-sort G) 
(declare-fun f (G G) G) 
(declare-const a G) 
(declare-const b G) 
(assert (= (f a a) a)) 
(assert (= (f a b) b)) 
(assert (= (f b a) b)) 
(assert (= (f b b) a)) 
(check-sat) 

;; Restrict the search to models of size at most 2 
(assert (forall ((x G)) (or (= x a) (= x b)))) 

;; Associativity 
(assert (not (forall ((x G) (y G) (z G)) (= (f x (f y z)) (f (f x y) z))))) 
(check-sat) 

$ z3 -smt2 G.smt 
sat 
unknown