In a previous post one theorem for the dihedral group D3 using Z3 SMT-LIB was proved. In this post we try to prove such theorem using both Z3 and CVC4 using the following SMT-LIB code:
(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)
When this code is executed using Z3 or CVC4 the correct results are obtained. Run this code with Z3 online here
The questions are :
In the case of Z3 a message unsupported ; :incremental is produced. This message seems does not to alter the results, why?
In the case of CVC4 a message unknown is produced while Z3 produces sat. Again, this message seems does not to alter the results, why?
How to execute the SMT-LIB code using Mathsat.
Regarding question 1, the option :incremental is not part of the SMT-LIB 2.0 standard. The standard defines/suggests a small set of options that should be supported by all solvers, and :incremental is not one of them. This is probably a CVC4 specific option. Z3 just ignores this command. Moreover, Z3 does not need the user to enable incremental solving.
Regarding question 2, the SMT-LIB 2.0 standard says there are 3 possible outputs for the check-sat: unsat, sat and unknown. The unknown result is used when a solver did not manage to establish whether the set of assertions is satisfiable or not. Some solvers produce a "candidate model" even when they produce unknown.
As far as I know, MathSAT 5 does not support quantifiers yet. However, this should change in the future.