这是我使用 z3 执行的 SMT-LIB 2.0 基准测试:
(set-logic AUFLIA)
(declare-sort PZ 0)
(declare-fun MS (Int PZ) Bool)
(assert (forall ((x Int)) (exists ((X PZ))
(and (MS x X)
(forall ((y Int)) (=> (MS y X) (= y x)))))))
(check-sat)
我预计结果是sat
,至少有一个模型,其中ZPZ
的幂集(整数)是一个谓词,用于测试整数在Z的子集(排序的元素)中的成员资格。MS
PZ
但是z3回答了unsat
。
你能帮我理解这个结果吗?具体来说,z3 如何解释 sort Int
?它真的被认为是无限的吗?那么动态声明的排序(这里是排序PZ
)呢?