z3 - 如何在 Z3 Fixedpoint 中获得多个约束？

Question

运行片段时

(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 可以实现吗？我怎样才能做到这一点？ (我已经看到多个问题得到约束，但我无法找出确切的符号<->值匹配)

Answer 1

关于您提出的内容，有两点要说:

• 您在 rise4fun 上使用的 Z3 版本在类似您提供的案例中提供了非信息性答案。 checkin 不稳定分支(在不同平台上自动构建)的版本产生答案:

  星期六

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

  星期六

  (mypred 3 2)

• 我没有一个令人满意的解决方案来显示形式 A |-> 3. 抱歉。