问题标签 [z3]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
scala - Scala^Z3（Z3 版本 3.2）和 parsesmtlib2string(...) 不工作
在尝试使用 parsesmtlib2string 实现测试时，我遇到了一个错误：
取消注释“Check-sat”时，我得到“未知”。取消注释“模型”时，我得到“不受支持”。
在 Z3 3.2 中使用 F# 只会给我一个 Term，但在 Scala 中，返回类型是 Unit。我查看了 Z3-C API，但没有找到关于如何使用 ist 的好例子。
那么，使用 smtlib2string 获取模型的最佳方法是什么？
顺便说一句：使用 Scala^Z3 和构建 Z3AST 工作得很好，我可以使用 .checkAndGetModel() 获得模型。上面的 SMT-LIB2 代码适用于 F# .NET parsesmtlib2string 方法。
使用“getSMTLIBFormulas、getSMTLIBAssumptions、getSMTLIBDecls、getSMTLIBSorts”之一会产生“错误：解析器（数据）不可用”。
使用“getSMTLIBError.size”产生“0”。
z3 - 如何在 Z3 中获得“更强”的连词简化？
使用 Z3 2.18 版，我试图简化公式，例如：
- (和 (> (- (- x 1) 1) 0) (> x 0))
- (或 (> (- (- x 1) 1) 0) (> x 0))
希望得到类似的东西：（> x 2）和（> x 0）。
我正在使用以下输入文件运行 Z3，其中 F 是上述公式之一：
它适用于我得到以下输出的析取：
但是，通过结合，我得到：
有没有办法强制 Z3 进一步简化上述公式？我希望能够得到(not (<= x 2))。
PS：有没有办法强制 Z3 内联其输出（即有(not (<= x 0))而不是(let (($x35 (<= x 0))) (not $x35))）
谢谢，格斯
z3 - Z3 INI 选项的详细文档
有没有关于 Z3 的 INI 选项的详细文档。我必须进行反复试验，才能找出解决 QF_BV 问题的最佳选择。我仍然不确定是否有更多选项可以让我的 z3 运行得更快。如果有人可以指出任何现有的 INI 选项的详细说明，那就太好了。
谢谢。
z3 - Z3 命名让 API 中的绑定
我正在使用 API 中的 Z3，并且正在寻找一种方法来调试我的约束。我的代码编译并且 Z3 在我的约束上运行，但是我的约束有问题。我希望查看我给 Z3 的约束以确定什么是错误或缺失的，但我不确定如何以一种非常易读的方式执行此操作。问题是使用 SMTLIB_DUMP_ASSERTIONS 之类的工具不会在任何 let 绑定变量中提供有意义的名称。由于我多次重复使用相同的表达式，因此几乎所有内容都与生成的变量绑定。
有没有办法转储输入约束的文件，其中让绑定变量具有我指定的名称？我并不特别关心格式是什么，但 SMTLIB 1 或 2 会很好。
z3 - 为什么 Microsoft.Z3 程序集没有签名？
我想将 Z3 (V3.2) 程序集放入 GAC，但未签名。这有什么原因吗？
z3 - 是否可以克隆 Z3_context？
我需要它在符号执行（Klee）的上下文中进行增量求解。在符号执行路径的分支点，有必要将求解器上下文分成两部分：具有真假条件。当然，有一个昂贵的解决方法 - 创建空上下文并重放所有约束。
有没有办法拆分 Z3_context？你打算添加这样的功能吗？
笔记
如果使用深度优先的符号探索，可以避免上下文的分裂，即探索当前的执行路径直到它到达“结束”，因此将来不会再探索这条路径。在这种情况下，弹出直到到达分支点并继续探索另一个条件分支就足够了。但是在 Klee 的情况下，许多符号路径是“同时”探索的（对真假分支的探索是交错的），因此您需要求解器上下文求解器切换（每个方法中有 Z3_context 参数）和分支（没有用于此的方法，这就是我需要的）。
谢谢！
api - 相当于 Z3 API 中的 define-fun
使用带有文本格式的 Z3，我可以define-fun用来定义函数以供以后重用。例如：
我想知道如何define-fun使用 Z3 API（我使用 F#）来创建，而不是到处重复函数体。我想用它来避免重复和更容易调试公式。我试过了Context.MkFuncDecl，但它似乎只生成未解释的函数。
labels - z3 中 SMT-LIB 2.0 断言上的标签
你能告诉我如何在 z3 SMT-LIB 2.0 基准测试中命名断言吗？我更喜欢使用 SMT-LIB 的标准语法，但由于 z3 似乎不理解它，我只是在寻找一个使用 z3 的语法。需要获得带有标签的未饱和核心。
这是我测试的基准测试示例：
由于矛盾（x < y 和 y <= x），我期待 unsat 核心 {hyp4, hyp5}，但 z3 返回：
我知道 z3 不理解这种命名方式，但我在 z3 文档中找不到另一种方式。
请问你能帮帮我吗？
z3 - Z3 的 Linux 版本：对旧 libgmp.so.3 的依赖
Z3对libgmp.so.3的依赖在linux包中没有解决，留给用户提供这个库。但是，这个库很旧，不容易获得。
有谁知道解决这个问题的方法？我目前正在运行 x86_64，并且没有很多麻烦就无法解决这个缺失的依赖项。
是否可以修复 linux 软件包，使其在发行版中包含预期的库？