我试图在 z3 中定义一个记录数据类型，它由六个不同类型的元素组成。我就是这样做的： (declare-datatypes () ((S (mk-pair (p1 (P1type)) (p2 (P2type)) (p3 (P3type))) (m1 (bool)) (m2 (bool)) (m3 (bool)) )))) 但是当我使用 (forall (x1 S)) 时，求解器似乎没有考虑我的数据类型的所有可能的估值组合。如果您让我知道我是否做错了什么，我将不胜感激，或者我不应该期望 z3 考虑 S 的所有估值组合。非常感谢，Fathiyeh
问问题
621 次
1 回答
1
这是您示例的永久链接：http ://rise4fun.com/Z3/0sl11
该模型产生函数 LS 和 tau 的解释。这两个函数都将值从 S 映射到布尔值。所以它们是谓词。该模型说明了满足公式的这些谓词的可能值是多少。它不必通过明确列出每个案例来制定谓词。这些谓词通常写成一个大的 if-then-else 表达式。最后一个 else 分支包含在 if 分支中未明确处理的值的默认情况。
于 2013-08-21T16:12:48.090 回答