3

运行片段时

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

4

1 回答 1

0

关于你提出的问题，有两件事要说：

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

    坐

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

    坐

    (mypred 3 2)

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

于 2014-06-10T12:08:58.553 回答