如何使用 c++ 在 z3 中为现有声明的函数添加新约束？

【问题标题】：How to add new constraint for existing declared function in z3 using c++?如何使用 c++ 在 z3 中为现有声明的函数添加新约束？
【发布时间】：2019-07-08 11:59:56
【问题描述】：

我想知道有没有什么方法可以在求解器中为现有声明的变量添加一些新的约束而不获取模型。

例如，如果我有 2 个声明函数：

(declare-fun k!648 () (_ BitVec 8))
(declare-fun k!647 () (_ BitVec 8))

还有一些限制。

我一般如何才能获得他们的声明名称？

情况是我想为现有的“变量”添加更多约束？在约束中并一起求解它们。但我对如何获得现有的“变量”感到困惑？然后形成对求解器也正确的新约束。

【问题讨论】：

标签： z3

【解决方案1】：

不清楚你在问什么。请注意，您的示例中的 k!648 和 k!647 实际上并不是函数，它们只是 8 位向量。（诚然，declare-fun 这个名字令人困惑。）

首先要了解的是，这些名称是从哪里来的？它在您提供给 z3 的脚本中吗？那么你在这里问错了人：你应该问生成这个基准的程序/系统。 z3 可以生成这样的名称，但仅限于模型中。

尝试提供 MCVE：https://stackoverflow.com/help/minimal-reproducible-example

【讨论】：

其实我是从符号执行中生成约束的。情况是我想为现有的“变量”添加更多约束？在约束中并一起求解它们。但我对如何获得现有的“变量”感到困惑？然后形成对求解器也正确的新约束。