问题标签 [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.
c# - Z3 .NET API 中的设置逻辑
使用 Z3 版本 3.1 时如何使用 .NET API 函数 .parseSmtlib2String(String) 时使用 set-logic？
我总是以 Z3Error-Exception 告终。
这种情况下不需要吗？
z3 - 获得量化布尔变量问题的模型
我正在使用 Z3 来检查具有线性整数算术、未解释函数和布尔变量上的量词的逻辑中的可满足性。Z3 没有提供可满足问题的模型，我想这是因为量词（或我选择的逻辑：AUFLIA）。
除了自己实例化所有布尔变量之外，有没有办法让 Z3 为我提供此类问题的模型？
z3 - Z3 QBVF 问题
继续前面的讨论：Z3：提取存在模型值
有没有区别：
和
就Z3而言？也就是说，我还会自动获得后者的 QBVF 求解器吗？
此外，经过实验，我发现如果我发出：
通话后(check-sat)，它工作正常（这很棒）。如果我也可以说：
唉，对于那个查询，Z3 抱怨它是一个invalid function application. 有没有办法以这种方式使用该eval功能？
谢谢！
z3 - 调用“eval”超时
莱昂纳多：感谢您的快速回复！非常感激。
如果我将以下脚本提供给 Z3：
Z3 成功构建了模型，其中s1给出了恒等函数。但是，对 eval 的调用会导致 Z3 超时。我需要设置一个特定的选项吗？
另外，我注意到如果我删除该行：
然后 Z3 回应unknown。由于 QBVF 是可判定的，所以我需要设置一个选项有点令人惊讶。是不是我们应该true在所有 QBVF 问题中设置 MBQI，还是这个实例有什么特别之处？
谢谢..
scala - 在 Windows 上编译 Scala^Z3
我尝试使用 Cygwin 和 JDK 1.7.0 在 Win XP 上编译 Scala^Z3，但没有按预期工作。
我做了以下事情： - 使用 SBT 0.7.4 - 使用来自 github 的当前 Scala^Z3 修订版 - 使用 Cygwin 及其 gcc - 使用 JDK 1.7.0 (javac)
“sbt update”成功了。“sbt package”最终会出现几个错误，说明未定义的引用，如下所示：
\psuter-ScalaZ3-35cb691\src\c/z3_Z3Wrapper.c:10: 未定义引用`_Z3_mk_config'
为了使它工作，我将 ....\PSuterScalaZ3\psuter-ScalaZ3-35cb691\project\build\scalaz3.scala 第 74 行更改为：
惰性 val gcc : ManagedTask = if(isUnix || is32bit) {
在主页上声明它也应该适用于 Windows。有吗？是否有预编译的 jar 可用？
我在这里看到了一个 z3.jar：http://lara.epfl.ch/~psuter/jniz3/z3.jar这 也是一个 Linux 版本，我猜？因为它对我也不起作用...
Scala^Z3 是一段非常好的代码（如果我能让它工作的话；））
z3 - 支持 AUFBV？
Z3 会支持 AUFBV 吗？
对于以下脚本：
在线 Z3 演示似乎对通话感到满意set-logic，但随后它抱怨各种BitVec和Array. （顺便说一句，无论逻辑名称如何，在线演示似乎都对调用感到满意set-logic，即使是假名，例如(set-logic blarg)。）
SMT-Lib 网站既没有提到 UFBV 也没有提到 AUFBV，但是考虑到它们的无量词对应物（QF_UFBV 和 QF_AUFBV），我希望 Z3 也能支持 AUFBV。
不用说，数组在实践中起着非常重要的作用。鉴于有限性论点，我认为 AUFBV 逻辑应该保持可判定性。很高兴看到 Z3 支持它。
谢谢！
z3 - => 的关联性和 = 的可链接性
Leonardo：根据http://goedel.cs.uiowa.edu/smtlib/papers/smt-lib-reference-v2.0-r10 .12.21.pdf 的第 3.7.1 节，=>是右关联的并且=是可链接的。不过Z3的网络版好像不支持这样的用途。我需要设置一个选项来获得这种行为吗？
谢谢..
z3 - 如何声明一条记录，使其其中一个字段是函数
我对Z3很陌生，很抱歉问了一些愚蠢的问题。
我正在尝试定义一条记录，使其某些字段是函数。我试过这个：
(declare-datatypes (DOM RAN) ((PFun (mk-pfun (dom (DOM) Bool) (law (DOM) RAN)))))
意图是 dom 和 ran 是两个类型为函数的字段（dom 是从 DOM 到 Bool 的函数，而 law 是从 DOM 到 RAN 的函数）。我还尝试将函数类型括在括号中：
(declare-datatypes (DOM RAN) ((PFun (mk-pfun (dom ((DOM) Bool)) (law ((DOM) RAN))))))
bun 这些都不起作用。
我搜索了教程，但没有这方面的例子。
你能帮助我吗？
提前感谢您的回答。
一切顺利，马克西
z3 - Z3：更好的建模方式？
我有两个 SMT 问题实例。第一个在这里：
Z3 在我不太好的机器上大约 2 分钟后返回了一个模型，这很棒。我也有这个：
我已经在这个问题上运行了 z3 一夜之间，没有 Z3 完成。如果您检查这些文件的内容，您会发现第二个与第一个相同，只是它有一个额外的断言来“拒绝”第一个实例返回的模型。（你可以在它们之间做一个“差异”来了解我的意思。）我碰巧知道这个问题有多个令人满意的模型，我正在尝试使用 z3 来找到所有令人满意的模型。
我知道这可能完全在意料之中，但我很想知道为什么与第一个相比，第二个对 Z3 来说是一个更棘手的问题。有没有更好的方法来制定第二个问题，这样 Z3 会更轻松？
谢谢..
z3 - Z3_ast 引用计数是否对 Z3 之外的引用进行计数？
Z3有2种模式：自动引用计数和手动。
我了解手动引用计数的工作原理。感谢示例。
但是在自动引用计数的情况下，Z3 是如何知道何时删除 AST 节点的呢？ 由于 Z3_ast 是来自 C 语言的结构 => 不可能在 Z3 之外跟踪 Z3_ast 在创建后的所有分配和使用。
还是仅 Z3 内部的 Z3 轨道参考？如果您这样做，则不会对 ref 计数器进行更新：ast1 = ast2。