问题标签 [smt]

我正在试验 Z3，我结合了算术、量词和相等的理论。这似乎不是很有效，事实上，在可能的情况下用所有实例化的地面实例替换量词似乎更有效。考虑以下示例，其中我为一个函数编码了唯一名称公理，该函数f接受两个 sort 参数Obj并返回一个解释的 sort S。这个公理表明每个唯一的参数列表都f返回一个唯一的对象：

尽管这是在逻辑中定义这样一个公理的标准方法，但像这样实现它在计算上是非常昂贵的。它包含 4 个量化变量，每个变量可以有 8 个值。这意味着这会导致8^4 = 4096平等。这需要 Z3 0.69s 和 2016 量词实例化来证明这一点。当我编写一个生成此公式实例的简单脚本时：

生成这些公理需要 0.002 秒，在 Z3 中证明它需要 0.01 秒（或更少）。当我们增加域中的对象或函数的参数数量时，f这种差异会迅速增加，量化的情况很快就会变得不可行。

这让我想知道：当我们有一个有界域时，为什么我们首先要在 Z3 中使用量词？我知道 SMT 使用启发式方法来寻找解决方案，但我觉得它仍然无法与一个简单的特定领域接地器在效率上竞争，后者将接地实例提供给 SMT，这只不过是 SAT 解决方案。我的直觉正确吗？

我正在尝试使用 Z3（Microsoft Research 开发的 SMT 求解器）检索某些一阶理论的所有可能模型。这是一个最小的工作示例：

在这个命题情况下，有两个令人满意的分配：f->true和f->false。因为 Z3（以及一般的 SMT 求解器）只会尝试找到一个令人满意的模型，所以不可能直接找到所有解决方案。在这里我找到了一个有用的命令叫做(next-sat)，但是Z3的最新版本似乎不再支持这个。这对我来说有点不幸，总的来说我认为该命令非常有用。还有另一种方法吗？

我目前正在研究通过 C 程序将“路径”转换为相应的 SMT 查询的代码，以测试该路径的可行性。我有创建 SMT-LIB v1.2 查询的工作代码，并使用 Z3 2.11 和 QF_AUFBV 逻辑来解决查询。我目前正在将此代码移植到 Z3 4.3，以利用从那时起可能发生的任何速度进步，特别是因为我以前的代码似乎需要很长时间（大约 22 分钟）处理仅分配 24 个值的查询一个三维数组并检查数组中某个位置的值。

但是，似乎 QF_AUFBV 逻辑（从 SMT-LIB v2.0 标准开始）不再支持多维数组，或者更确切地说，其值也是数组的数组（可能更深）。一旦我从查询中取出“(set-logic QF_AUFBV)”行，Z3 4.3 就能够处理查询，但仍然需要很长时间。

我想知道是否有人知道为什么在 SMT-LIB v2.0 标准中停止支持多维数组，以及我可以使用哪些替代逻辑。当我取出指定 QF_AUFBV 理论的那条线时，我还想知道 Z3 到底在使用什么逻辑。

谢谢！

我有兴趣测试 [1] 中讨论的决策/实例化过程（包括其实施）的“实际”影响。

我需要：

1) 一个“工具”，它采用 SMT 基准并返回它的（可能完整的）实例化版本，应用该策略。如果这是不可能的，

2) Z3 版本实现了这个策略和一个打开和关闭它的选项。

你能帮我吗？

[1] Satisfiabiliby Modulo Theories 中量化公式的完整实例化

我有简单的 Z3 python 代码，如下所示。我希望“打印”行将返回存储在其上方行中的“y”。相反，我得到了“A[x]”作为结果。

为什么不Select()返回存储的值Store()？

谢谢。

我在使用 SMTlib2 格式的排序时遇到了一些问题。例如，我将 Interval 定义为：

现在如何从函数返回一个新的间隔？例如：

这行不通。我的问题是：如何构造和实例化给定类型的对象，以及如何访问它们的字段？

现在我正在使用我创建的 2 个 UF 作为字段获取器，但我仍然不知道如何拥有一个构造函数：

谢谢，努诺

我正在尝试使用Skolemization删除我的理论中的存在量词。这意味着我用存在量词范围内的普遍量化变量参数化的函数替换存在量词。

在这里，我找到了如何在 Z3 中执行此操作的说明，但我仍然无法执行此操作。假设有以下两个函数：

我相信这f2应该是正确的，因为存在一个t这样的整数(f1 t)是正确的，即t=3。我通过为存在量化公式引入一个常数来应用 Skolemization：

然后将存在量词的公式改写为：

这不起作用，也就是说，常数c没有值 3。我怀疑这是因为我们没有对常数给出解释c，因为如果我们添加(assert (= c 3))它可以正常工作，但这会消除存在主义的整个想法量词。有没有一种方法可以让我给出一个不太明确的解释，c这样才能奏效？

我正在尝试使用 C API 生成 Craig 插值，但得到的结果不正确。但是，当我通过 Z3_write_interpolation_problem 将相同的问题转储到文件并调用 iZ3 时，我得到了预期的插值。

我附上代码以便能够重现相同的结果。我正在使用 z3 4.1

我使用以下命令生成可执行文件：

g++ -fopenmp -o 插值插值.c -I/home/jorge/Systems/z3/include -I/home/jorge/Systems/z3/iz3/include -L/home/jorge/Systems/z3/lib -L/主页/jorge/Systems/z3/iz3/lib -L/home/jorge/Systems/libfoci-1.1 -lz3 -liz3 -lfoci

请注意，约束基本上是：

A = (x=0 and x1 = x0+2 and x2 = x1 + 2),

和 B = (x2 > 10)

这显然是不满意的。此外，很容易看出唯一的公共变量是 x2。因此，任何有效的插值只能包括 x2。

如果我运行可执行文件 ./interpolation 我会得到无意义的插值：

但是，如果我运行“iz3 tmp.smt”（其中 tmp.smt 是使用 Z3_write_interpolation_problem 生成的文件），我将获得一个有效的插值：

未饱和插值：(<= x2 10)

这是一个错误吗？还是我在调用 Z3_interpolate 时遗漏了一些重要的先决条件？

PS 我找不到任何使用 iZ3 和 C API 的示例。

干杯，豪尔赫

我正在浏览 Z3py，并且对如何在几个特定情况下使用 API 有疑问。下面的代码是我最终想使用 Z3 的简化版本。我的一些问题是： 1. 有没有办法创建一个任意长的值数组，比如下面的变量“a”？2、可以通过Z3py循环访问数组的每个元素吗？3. 是否可以将结果分配回原始变量或是否需要新变量？转换为 CNF 会自动添加唯一的 id 吗？（即 a += b）

总的来说，我不知道如何将 Z3py API 应用于以下算法，其中解决方案取决于“b”。感谢您提供任何帮助或提示，谢谢。

在 Z3 教程的第 13.2.3 节中，有一个很好的例子，说明如何在处理内射性公理化时减少必须实例化的模式数量。在示例中，必须声明为单射的函数 f 将 A 类型的对象作为输入并返回 B 类型的对象。据我了解，A 和 B 是分离的。

我有一个 Z3 似乎没有终止的 SMT 问题 (FOL+EUF)，我正在尝试找出原因。我有一个函数 f:A->A 我断言它是单射的。问题可能是 f 的域和共域重合吗？

提前感谢您的任何建议。