做

总是意味着同样的事情

?

这两个表达式在我的模型中表现不同。虽然使用=>给了我UNSAT，但使用其他变体不会产生任何结果（timeout）。我会满足于拥有一个运算符列表及其含义。我知道 SMTLIB 标准，但文档没有明确讨论运算符的含义。具体来说，如果在三元表达式中使用，' => ' 似乎可以兼作 ' ite ' (if_then_else) 运算符的别名，我对此感到非常困惑。

如果相关，我设置了AUFLIA逻辑。

我正在寻找一个简单的是或否的答案。其次是关于 SMT2 的适当文档（可能是一本书）。

我有这个相当大的模型，这个模型是从 Daniel Jackson 的标记扫描模型生成的，用于那些愿意亲眼看看的人的合金 4。

模态认知逻辑（又名知识逻辑）是否有任何（类似 SMT 的）求解器？

我需要一阶（不仅仅是命题）案例。

有人可以帮助我指出使用一阶公式对以下方程进行最佳编码，以便将其作为 SMT 求解器的输入吗？

你知道除了Z3之外还有什么smt工具支持fixpoint吗？

我正在尝试在 Z3 中使用数组和量词来查找给定文本中的子字符串。

我的代码如下：

Z3 在不应该的时候说那是 SAT。我对 Z3 和 SMT 理论相当陌生，我无法弄清楚我的代码有什么问题。

我希望隐藏一些变量并获得简化的结果。

我想隐藏c1，c2如下d：

不过结果看似复杂，其实结果应该是v2>=5.0 & v1<= v2+5.0，我以前用(apply ctx-solver-simplify)的代码是

但是，当我添加 apply ....有错误时，脚本无法工作。有人可以帮我解决吗？

我找不到 .net api，因为(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))它是一种策略吗？有人可以帮助我使用 Z3 的 .net API 来实现以下脚本吗？

我正在尝试实现 String.Containts 函数。我写了一些简单的测试用例，但是下面的一个（应该返回 UNSAT）返回 SAT。

该测试尝试通过将所有可能的子字符串与想要的字符串（取自 Z3 输出的文本）进行比较来匹配字符串 'abcd' 中的子字符串 'bd'：

我尝试了各种实现，但没有任何成功。

我正在测试一些简化的一般性（主要是：有向部分量词实例化）。因此，我在 smtComp 的“AUFLIA-p”部分运行了一组基准测试，无论是否简化。为了尽可能减少副作用，我有兴趣在没有（用户提供）模式的情况下运行 Z3。

我在“AUFLIA-p”部分检查了一些基准，我想知道为什么这部分的基准包含模式。也许您已经为本节运行了 Z3，并带有禁用模式的选项。最近，我刚刚放弃了一些基准测试中的模式，并观察到性能的急剧下降。

问题：
“AUFLIA-p”和“AUFLIA+p”部分之间有什么区别吗？
我如何告诉 Z3 忽略（用户提供的）模式？

问候，
Aboubakr Achraf El Ghazi

在 SMT/SAT 求解中，是否有一些技术可以从公式中确定不相关的变量？即那些可以有任何值并且不影响公式可满足性的那些。