在先前的post中,使用Z3 SMT-LIB证明了二面体组D3的一个定理。在本文中,我们尝试使用以下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在线here
运行此代码问题是:
对于Z3,将生成消息unsupported ; :incremental
。此消息似乎并没有改变结果,为什么?
对于CVC4,将生成消息unknown
,而Z3将生成sat
。同样,此消息似乎并没有改变结果,为什么?
如何使用Mathsat执行SMT-LIB代码。
关于问题1,选项:incremental
不属于SMT-LIB 2.0标准。该标准定义/建议了所有求解程序应支持的一小部分选项,:incremental
不是其中之一。这可能是特定于CVC4的选项。 Z3只是忽略此命令。而且,Z3不需要用户启用增量求解。
关于问题2,SMT-LIB 2.0标准说check-sat
有3种可能的输出:unsat
,sat
和unknown
。当求解器无法确定断言集是否可满足时,将使用unknown
结果。一些求解器即使生成unknown
,也会生成“候选模型”。
据我所知,MathSAT 5还不支持量词。但是,将来这会改变。
Mathsat似乎产生了正确的结果,但它生成了消息:
<< img src =“ https://image.soinside.com/eyJ1cmwiOiAiaHR0cHM6Ly9pLnN0YWNrLmltZ3VyLmNvbS9TZXdCaC5qcGcifQ==” alt =“在此处输入图像说明”>