问题标签 [smt-lib]

我知道我可以用 simple 断言不等式(not (= a b))，但我想知道是否有直接执行此操作的运算符。我已经尝试了所有想到的东西，包括!=, <>, \=（这不会解析），/=, =/=，neq但它们都不起作用。

是否有专门的功能，或者我需要用否定组成相等吗？

我有一些使用 PySMT API 编码的问题。PySMT 的 GitHub 页面显示了一个关于将任何符合 SMTLib 的求解器与 PySMT 一起使用的示例。它说 PySMT 会将问题交给标准输入中的求解器。但我找不到任何直接将其打印到标准输出或文件的方法。

我很确定应该可以使用 SMT-lib 语法来描述元组，尤其是对于 Z3 求解器。但是，我真的找不到这样做的方法。我唯一找到的是这个文档页面，但我不知道如何在z3 -in.

到目前为止我的挣扎：

我试图找出一个正则表达式，它可以匹配以 smtlib 格式输出的程序的结果。基本上，我的数据采用以下形式：

是否可以编写匹配的表达式：

我目前的方法是使用 查找单个事件\(define-fun[\w\s]+\)，然后对于每个事件，删除(define-fun、、和Int，然后读取数据，因为剩下的就是 ，())1 28171 104

我只是想知道是否有更优雅的方式来做到这一点？

我目前正在为一小部分 Python 构建一个符号执行引擎。该子集支持的最复杂的数据结构是任意嵌套的元组，即，您可以编写类似x = (1, 2, (3, 4), 5). 在我的 SE 引擎中，所有值都表示为 z3 对象。昨天，我尝试在 z3 中为这些嵌套元组建模时遇到了很大的困难。

我尝试了什么：

• 数组。问题：数组就是数组，也就是说，它们跨越一个矩形空间，这不适合我的元组。
• 序列。我喜欢序列数据类型；但是，它不支持嵌套。例如，你不能写z3.Concat(z3.Unit(z3.IntVal(1)), z3.Unit(z3.Concat(z3.Unit(z3.IntVal(2)), z3.Unit(z3.IntVal(3)))))，这会引发z3.z3types.Z3Exception: b"Sort of function 'seq.++' does not match the declared type. Given domain: (Seq Int) (Seq (Seq Int))"
• 列表。但是，列表只有一个类型T，我只能将其实例化为List 或，例如Int。据我所知，z3 中没有联合类型或通用超级排序之类的东西。
• 未解释的函数。我认为应该可以引入一个tuple带有 sort的函数Tuple，甚至为不同的参数长度和排序重载它。但是，我不知道如何提取 a 的元素tuple(1, 2, 3)，因为该表达式不是递归定义的。

我将感谢 z3 / SMT 专家的帮助！

提前非常感谢！

元组数据类型：“抽象”索引和元组的问题

我还尝试了@alias 提出的想法，为元组定义数据类型。这工作得很好，但是有一个问题：如果元组或索引不是具体的，即（表达式包含）变量，我如何模拟对元组元素的访问？

例如，我可以将整数的 2 元组定义为：

没关系。我还可以通过嵌入 Tup_II 数据类型在顶部定义嵌套元组：

但是要访问一个元素，我需要知道索引是 0 还是 1 才能选择正确的访问器( fst, snd)。

我试图从序列类型的行为中获得灵感：

所以一个想法是定义一个Tuple_II.nth函数。但是，如果我们有一个像 Tup_IT 这样由不同类型的元素组成的元组，我该如何定义这个函数的目标域？例如，

因此，为此，我需要某种超级类型的int和Tup_II：与列表相同的问题。

有任何想法吗？:)

我想要的：用于创建元组类型的实用函数

假设我可以解决 getter 函数的排序问题；然后我写了一个很好的实用函数，创建了在存在抽象索引的情况下处理元组所需的所有东西：

问题在于注释的target_sort声明# ??? <-- What to do here?。

假设我有以下问题（我已经简化了我的问题）

如果第一次SAT检查是未饱和/饱和，我想做的是跳过第二次SAT检查。是否有可能做到这一点？我相信如果我将 Z3 与 python 一起使用（运行 sat 检查，获取结果，并在结果上使用 python if 语句来确定是否运行第二次检查），我可以做到这一点，但我想用 smt 做到这一点-lib。这（很容易）可能吗？

我有一个关于declare-constsmtlib 的问题。

例如，

在z3/cvc4中，以下程序不报错：

在 smt-lib-reference 中，它说

(declare-fun f (s1 ... sn) s) ... 如果当前签名中已经存在名称为 f 的函数符号，该命令将报告错误。

所以排序s包含在 的整个签名中x，对吗？

但为什么会这样呢？其背后的动机是什么？

在我的理解中，xis 是变量标识符，一般来说（例如在一些通用编程语言中）我们不允许用不同的类型声明同一个变量。所以我觉得上面的代码最好是报错。

我曾经认为也许z3/smtlib可以支持重新定义？，但不是......

那么上面的代码肯定是错的，为什么不早点报错呢？

PS。如果我使用相同的排序，那么它会报错（那太好了，我希望Bool案例也能报错）：

谢谢。

例如，

还行吧。

但是，我想通过as?

我应该填写???什么？

它必须是一种排序，但我应该使用哪种排序？

我试过((Int Real) Int)or (-> (Int Real) Int)or (_ (Int Real) Int)，但没有一个是正确的。

是否可以在 smtlib 中声明函数排序？

如果无法声明函数排序，如何f在下面的程序中消歧：

请注意，如果我不使用函数，那没问题：

谢谢。

我知道有一种方法可以在 SMTLIB 中声明参数数据类型。有没有办法定义一个接受这种类型的函数？例如标准文档有：

现在如何声明一个接受参数Pair类型的函数？

我想知道是否有任何方法可以将 smtlib2 公式表示为模板。例如：

可以表示为（比如使用 jinja2 样式的模板）

然后可以渲染模板来表示一个实际的 smtlib 公式：

除了使用 jinja2 之类的东西并为每个公式创建我自己的模板之外，还有什么自然的方法可以做到这一点？

或者，考虑到我已经有一个代表 SMT 公式的 z3::expr_vector，有没有办法“模板化”它？我的最终目标是我想为每个调用“调用”具有唯一位向量名称的模板化版本。z3 C++ API 是否有任何方法可以自然地实现这一目标？