问题标签 [z3-fixedpoint]

我使用数组作为 z3 定点求解器中关系的参数。我正在尝试在满足我的查询的证书中获取数组值。当我在 z3 上运行它时，它会抛出一个错误，指出Uninterpreted 'a1' in A(#1,#0,#3)。

为什么数组被视为未解释？这是否意味着未解释的函数不能用作定点求解器中关系的参数？

当我尝试通过 python api 在 z3 的定点求解器上使用推送和弹出操作进行回溯时，求解器抛出“引擎不支持操作”异常。

z3py 在定点求解器上是否不支持 push 和 pop 操作？

我试图找出为什么交换查询订单可能会修改 Z3 定点引擎的答案：

第一个查询q1是一个虚拟查询，只是向引擎询问一些事情。第二个查询q2与推断的不变量相矛盾，即斐波那契数始终为正。

如果查询的顺序是

一切正常，给出了正确的答案。但是在查询时交换它们会产生下一个错误q2：

有人可以解释原因吗？是 Z3 问题还是我做错了什么？如果首先，任何有关工作的建议（我正在使用.NET API）将不胜感激。谢谢！

我刚刚开始深入研究 Z3 的定点求解器，并且编写了一个示例，该示例在使用乘法时挂起，但在将乘法定义为一系列加法时完成。由于我是使用 Horn 子句的新手，因此可能有些东西我没有在这里理解。“本机”乘法如此缓慢，而定义为一系列加法的乘法在合理的时间范围内产生令人满意的结果是否有原因？谢谢！

我可以解释任何必要的深度，但长话短说，我的项目使用 Z3 的优化器来找到有效解决与布尔变量相关的权重的 SAT 问题的最大解决方案。除此之外，我项目的另一部分有效地实现了基于规则的饱和引擎，我最近一直在考虑使用定点求解器对其进行重写。我以为我可以分别考虑问题的两个部分，但事实证明存在先有鸡还是先有蛋的问题，规则引擎需要解决 SAT 实例才能使其输入和输出正确且有意义，并且 SAT 实例本身来自规则引擎的输出。因此，我想我可能会尝试结合Fixedpoint和Optimize. 这可能吗？它甚至有意义吗？

我正在使用 Z3 来解决我的角子句。在 Horn 子句的主体中，未解释的谓词应该是肯定的。但是，我需要否定一些未解释的谓词。

我已经看到了一些否定工作正常的例子。例如 Z3 将返回sat以下示例：

但我的示例如下所示，Z3 返回unknown.

我想知道是否有办法将我的子句重写为 Z3 的 Horn 子句片段。

我正在使用 Z3 和扩展的 SMT-LIB2 语法来解决我的角子句。我知道 horn 子句的 head 应该是一个未解释的谓词；但是，我想知道如何将以下子句重写为一组喇叭子句。

Z3 抱怨(> a 0)不能成为喇叭子句的头。我可以将最后一个子句改写如下：

但是，子句变得如此弱，以至于我没有得到不变量的预期模型inv。我想知道是否有更好的方法来做到这一点。

我正在使用 z3 进行等价检查。我尝试使用 z3 horn solver 来加速 z3 求解时间，我遇到了以下问题：

我想检查两个程序是否相同。两个程序的逻辑是 P1：a2 = a1 + 2，其中 a1 是输入，a2 是输出 P2：b2 = b1 + 2，其中 b1 是输入，b2 是输出 a1、a2、b1 的类型， b2 是位向量 64。公式是 forall (a1, b1), (a1 == b1) && (a2 == a1 + 2) && (b2 == b1 + 2) => (a2 == b2)

如果我使用 bv 求解器，结果是sat. 但是，如果我使用喇叭求解器，求解结果是unknown，原因是

为什么这两个求解器有不同的结果？以及为什么喇叭求解器的结果是未知的？

这是源代码：

我很确定它与 python API 有关。即使状态为 ，有没有办法从 z3 取回部分模型unknown？

即使状态返回unknown结果，我也试图从 z3 中获取模型。提高exceptionfor失败model not available。有什么建议可以做什么？

sexpr()我使用接口中的方法将断言转换为 smt-lib 格式z3 Solver，即使状态为unknown. 我在下面附上了示例。

SMMT-LIB 格式

我正在从命令行（终端）运行这个文件

输出 ：

有关如何直接通过 python 接口获取此模型的任何建议？

model()z3 在调用unknown状态后引发的异常。

谢谢

I'm trying to make assertions about program equivalence using z3's Fixedpoints, and I'm finding that any sort of recursion, even trivially decidable recursion, makes z3 totally choke. This z3py tutorial specifically calls out program simulation as a use case for Fixedpoints, with programs being represented by recursive data types. I feel like I must be doing something wrong.

Here's a simple example:

RightLL is a unary relation for trees that only extend to the right. nil only extends to the right, and if you do cons(nil, a) on a list a that only extends to the right, it continues to extend to the right. Seems like it should be trivial.

But on a modestly deep tree, the code spins indefinitely. Here's the stats after interrupting a few minutes in:

I honestly have no idea what z3 might be trying here... Smaller lists, and lists that don't match the predicate (when the cons-on-the-left is near the top of the tree) complete quickly.

Am I doing it wrong? Or is z3 just incapable of handling recursively defined predicates over algebraic data types?