Z3 中记录数据类型的所有可能值？答案

【问题标题】：All possible values for a record datatype in Z3?Z3 中记录数据类型的所有可能值？
【发布时间】：2013-08-20 15:54:48
【问题描述】：

我试图在 z3 中定义一个记录数据类型，由六个不同类型的元素组成。我是这样做的： (declare-datatypes () ((S (mk-pair (p1 (P1type))) (p2 (P2type)) (p3 (P3type)) (m1 (bool)) (m2 (bool)) (m3 (bool)) ) ))) 但是当我使用 (forall (x1 S)) 时，求解器似乎没有考虑我的数据类型的所有可能的估值组合。如果您让我知道我是否做错了什么，我将不胜感激，或者我不应该期望 z3 考虑 S 的所有估值组合。非常感谢，法蒂耶

【问题讨论】：

如果没有其他信息，很难回答这个问题。您能否提供一个出现问题的完整示例？
感谢您的关注。这是我的例子： (declare-datatypes () ((P1type pp12))) (declare-datatypes () ((P2type pp21 pp23 pp20))) (declare-datatypes () ((P3type pp32 pp30)))
(declare-datatypes () ((P1type p12))) (declare-datatypes () ((P2type p21 p23 p20))) (declare-datatypes () ((P3type p32 p30))) (declare-datatypes () ((S (mk-pair (p1 (P1type))) (p2 (P2type)) (p3 (P3type)) (m1 (bool)) (m2 (bool)) (m3 (bool)) ) ))) (declare-fun lambda1n (S) Int) (declare-fun LS (S) Bool) (declare-fun thau (S S) Bool) (assert (forall ((x1 S)) (= (LS x1) (非（和（非（和（=（p1 x1）p12）（=（p2 x1）p21）））（非（和（=（p1 x1）p12）（=（p2 x1）p21）））））） )) (assert (forall ((x1 S)) (=> (not (LS x1)) (exists ((x2 S)) (and (not (= x2 x1)) (thau x1 x2)) ) )) (check-sat) (get-model)
z3 返回的模型不包含所有可能的估值记录。

标签： z3 smt

【解决方案1】：

这是您示例的永久链接：http://rise4fun.com/Z3/0sl11

该模型生成函数 LS 和 thau 的解释。这两个函数都将值从 S 映射到布尔值。所以它们是谓词。该模型说明了满足公式的这些谓词的可能值是多少。它不必通过明确列出每个案例来制定谓词。这些谓词通常写成一个大的 if-then-else 表达式。最后一个 else 分支包含 if 分支中未显式处理的值的默认情况。

【讨论】：

我明白了。我的问题是理解解释。非常感谢:)