1

以前の投稿で、Z3 SMT-LIB を使用した二面体群 D3 の 1 つの定理が証明されました。この投稿では、次の SMT-LIB コードを使用して、Z3 と CVC4 の両方を使用してそのような定理を証明しようとします。

(set-logic AUFNIRA)
(set-option :produce-models true)
(set-option :incremental true)
(declare-sort S 0)
(declare-fun f (S S) S)
(declare-fun g (S) S)
(declare-fun E () S)
(declare-fun R1 () S)
(declare-fun R2 () S)
(declare-fun R3 () S)
(declare-fun R4 () S)
(declare-fun R5 () S)
(assert (forall ((x S))
            (= (f x E) x)))
(assert (forall ((x S))
            (= (f E x) x)))               
(assert (= (f R1 R1) R2))
(assert (= (f R1 R2) E))
(assert (= (f R1 R3) R4))
(assert (= (f R1 R4) R5))
(assert (= (f R1 R5) R3))
(assert (= (f R2 R1) E))
(assert (= (f R2 R2) R1))
(assert (= (f R2 R3) R5))
(assert (= (f R2 R4) R3))
(assert (= (f R2 R5) R4))
(assert (= (f R3 R1) R5))
(assert (= (f R3 R2) R4))
(assert (= (f R3 R3) E))
(assert (= (f R3 R4) R2))
(assert (= (f R3 R5) R1))
(assert (= (f R4 R1) R3))
(assert (= (f R4 R2) R5))
(assert (= (f R4 R3) R1))
(assert (= (f R4 R4) E))
(assert (= (f R4 R5) R2))
(assert (= (f R5 R1) R4))
(assert (= (f R5 R2) R3))
(assert (= (f R5 R3) R2))
(assert (= (f R5 R4) R1))
(assert (= (f R5 R5) E))
(assert (= (g E) E))
(assert (= (g R1) R2))
(assert (= (g R2) R1))
(assert (= (g R3) R3))
(assert (= (g R4) R4))
(assert (= (g R5) R5))
(check-sat)
(get-model)
(get-value ((f (f R3 R1) (g R3))))
(get-value (R2))
(assert (not (= (f (f R3 R1) (g R3)) R2))) 
(check-sat)

Z3 または CVC4 を使用してこのコードを実行すると、正しい結果が得られます。Z3オンラインでこのコードをここで実行してください

質問は次のとおりです。

  1. Z3 の場合、メッセージunsupported ; :incrementalが生成されます。このメッセージは結果を変更しないようですが、なぜですか?

  2. CVC4 の場合、unknownZ3 が生成する間にメッセージが生成されますsat。繰り返しますが、このメッセージは結果を変更しないようです。なぜですか?

  3. Mathsat を使用して SMT-LIB コードを実行する方法。

4

2 に答える 2