如何在 Z3 Fixedpoint 中获得多个约束？答案

【问题标题】：How to get multiple constraints in Z3 Fixedpoint?如何在 Z3 Fixedpoint 中获得多个约束？
【发布时间】：2014-05-29 06:45:46
【问题描述】：

运行片段时

(declare-rel mypred (Int Int))
(declare-var A Int)
(declare-var B Int)
(declare-var C Int)
(rule (mypred 1 0))
(rule (mypred 2 1))
(rule (mypred 3 2))
(rule (mypred 4 3))
(rule (mypred 5 4))
(rule (=> (and (mypred C B) (mypred A C)) (mypred A B)))

(query (and (mypred C 2) (mypred 2 B) (mypred B A))
  :print-answer true
)
(query (mypred A 2)
  :print-answer true
)

在 z3 中（例如在rise4fun http://rise4fun.com/Z3/ 上），我得到了答案：

sat
(and (query!0 1 1 3) (mypred 2 1) (mypred 3 2) (mypred 1 0))
sat
(and query!16!slice!18 (mypred!slice!17 2))

正如预期的那样，两个查询都可以得到满足，并且 Z3 正确地报告了这一点，但我也想找出它们满足 A、B、C 的哪些值，但答案并没有提供直接的答案。

“query!0”的参数似乎与原始查询中使用的参数不同，并且答案的第二部分仅在重新排序后才与原始查询匹配。我实际上是使用 .NET API 对此进行编码，因此我可以检查 AST，但我想避免尝试将原始查询的每个元素与答案中的每个元素进行匹配（例如，如果有办法保持秩序，我会很高兴的）。

可以通过多种方式满足第二个查询。我目前对找到其中一个不感兴趣（尽管这也可能很有用），但我想知道一种方法可以自动将其与查询具有唯一解决方案的情况区分开来。

这可以通过 Z3 Fixedpoints 实现吗？我怎样才能做到这一点？（我已经看到多个问题得到约束，但我无法找出确切的符号值匹配）

【问题讨论】：

标签： z3 z3-fixedpoint

【解决方案1】：

关于你提出的问题有两点要说：

您在rise4fun 上使用的Z3 版本在您提供的情况下提供了非信息性答案。签入不稳定分支的版本（在不同平台上自动构建）会产生答案：

坐

(和 (mypred 3 2) (mypred 1 0) (mypred 2 1))

坐

(mypred 3 2)
我没有令人满意的解决方案来显示表单 A |-> 3. 抱歉。

【讨论】：