Z3 中的排序名称问题

Question

在上一篇文章中，Z3群使用名为S的排序来表示群，证明了一些群公理。请使用名为 S 的排序运行代码代码，但现在当排序名称更改为 G 时，代码不起作用。请在名为 G 的排序的行代码上查看问题 有必要使用名称 S 进行排序，还是 Z3 的问题？请让我知道。

Answer 1

问题的

简化版本。

$ 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

Answer 2

请让 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

请在此处在线运行此代码