问题标签 [z3-fixedpoint]

我尝试在定点中使用 ctx.mkExist ，但是出现错误说“包含递归谓词”，我不知道为什么？以及如何在定点中使用 ctx.MkExists？例如：存在 (lamda real) that lamb>=0 AND inv(c,i) AND phi(c+lamb,i) => phi(c，i)

有时，会出现错误提示“ AccessViolationException was unhandlered,Attempted to read or write protected memory. 这通常表明其他内存已损坏。” 当运行到 ctx.MkExists()

我希望得到像d>=0.0这样的定点phi中元素的约束，如何在Z3中实现呢？

我想得到定点phi中元素的约束，在下面的例子中，约束应该是c2<=c1+5.0, c1>=5.0 在Z3中应该如何实现呢？或者有什么办法不使用 Z3 中的定点

我正在使用 z3py API 来计算一组归纳注释。我将我的约束映射到广义 Horn 子句的结合。在这些约束中，有几个关系（l6 和 iwc1）需要推断。涉及的变量（incr1、t1 和 wc1）都是整数。我希望推断的谓词是区间关系。谓词 l6(incr, t1) 应该捕捉到 incr = 0 和 t1 >= 0 的事实。我将其构建为以下规则：

推断谓词 l6 是：

同样，iwc1 是一个涉及变量 wc1 的谓词，它试图捕捉wc1 == incr + t1incr 和 t1 的值被 l6 过度逼近的事实。换句话说，

由于wc1 == incr + t1和 l6 推断 incr = 0 和 t1>=0，我预计 iwc1 为 wc1>=0。相反，推断的谓词是True。为什么 iwc1 变得如此弱？

此在线 z3py 代码中提供了完整的程序。

相反，如果我将 iwc1 的规则修改如下：

然后，我收到以下错误：

iwc1 规则已更改的程序可在此处获得。Z3Py 抱怨变量 incr 没有界限。我在哪里犯错？

当我尝试将定点引擎设置为 PDR 并尝试设置 pdr_use_farkas 选项时，我收到了 unknown_parameter 错误。

特别是，我在定点对象上使用以下选项：

这会导致错误：

使用 set_option 也无济于事。我试过了

我得到“未知选项”。

我在哪里犯错？

我正在使用 Z3 4.3.1 64 位。

我正在使用 Z3 中的定点引擎来编码几个通用号角公式。查询结果是不满意的。在 Z3Py 中，使用 get_answer() 将估值返回给未解释的关系。但是，在 SMTLIB2 格式中，get-answer 返回unsupported. 这是我的程序：

我使用 Z3 得到的输出version 4.3.2是：

在 Z3Py 中，创建一个定点上下文，fp=Fixedpoint()然后执行print fp.get_answer()会将估值返回到I和。有没有办法以 SMTLIB2 格式获得相同的内容？谢谢。I1err

有没有办法在 muZ3 关系规范中不确定地执行递归调用？具体来说，我想翻译如下函数：

到 muZ3 规则格式。

运行片段时

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

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

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

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

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

query尝试使用关键字进行定点查询时出现“未知排序”错误。例如，定点教程中的以下示例，在 Z3 的在线版本中运行良好，

返回：

当我从命令行运行它时。我在 Linux 上使用从 github 存储库编译的 Z3 版本 4.4.2。我的命令行是：z3 -smt2 example.smt

是否需要设置一些编译标志才能启用此功能？

我在z3定点教程中修改了边缘和路径示例

这运行良好，没有任何问题。

但是，如果我将其更改为具有 ite 表达式的功能等效脚本，则会返回错误。

这是使用 ite 更新的脚本：

我得到以下错误：

我试图创建一个新的关系iteRel来模拟ite表达式的效果，但没有任何成功。

这将使第三季度不满意。

是否有任何解决方法可以在 z3 定点中使用 ite 表达式？我需要在我的动态符号执行引擎中一起使用它们。非常感谢您！