问题标签 [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.
z3 - Z3 可以检查有界数据结构上的递归函数的可满足性吗？
我知道Z3 无法检查包含递归函数的公式的可满足性。但是，我想知道Z3是否可以在有界数据结构上处理此类公式。例如，我在Z3 程序中定义了一个长度最多为 2 的列表和一个名为 的函数，last用于返回列表的最后一个元素。但是，当要求检查包含 的公式的可满足性时，Z3 不会终止last。
有没有办法在 Z3 的有界列表上使用递归函数？
z3 - Z3 可以用来推理子串吗？
我正在尝试使用 Z3 来推理子字符串，并且遇到了一些不直观的行为。当被问及“xy”是否出现在“xy”中时，Z3 返回“sat”，但当被问及“x”是否在“x”中或“x”是否在“xy”中时，它返回“未知”。
我评论了以下代码来说明这种行为：
现在问题已经成立，我们尝试找到子字符串：
如果我们改为搜索findMeXYin xy，求解器会按预期返回“sat”。看起来，由于求解器可以处理“xy”的查询，它应该能够处理“x”的查询。此外，如果搜索findMeX='x'in 'xy='xy'，它会返回“未知”。
任何人都可以提出解释，或者在 SMT 求解器中表达这个问题的替代模型吗？
z3 - 为位向量（SMTLIB2，Z3）赋值？
我正在使用 Z3 3.0 版。我想为位向量变量赋值，如下所示。但是 Z3 报告错误“无效的函数应用程序，第 3 行位置 2 的参数排序不匹配”。
我的常量#x0a 似乎有问题？我怎样才能解决这个问题？
谢谢
silverlight - 在 Silverlight 应用程序中使用 Microsoft Z3？
有没有人设法让 Silverlight 4 应用程序使用 Microsoft Z3？
我认为它似乎不起作用，因为它似乎使用本机 Windows dll。
silverlight - 在 Azure 中托管的 WCF RIA 服务应用程序的 Web 应用程序中引用 64 位 dll
我有一个使用 WCF RIA 服务并托管在 Azure 中的 Silverlight 应用程序。
Web 应用程序引用 Microsoft Z3 dll：
如果我引用此 dll 的 32 位版本，Azure 无法托管它，因为它需要 64 位版本。如果我引用 64 位版本，RIA 服务将无法编译。
我需要找到一种在 Azure 中使用 32 位 dll 的方法，或者我需要找到一种为 RIA 服务引用 63 位 dll 的方法。
关于哪个是最好的方法以及如何做的任何提示？
谢谢
山姆
z3 - Z3：提取存在模型值
我正在使用 Z3 的 QBVF 求解器，想知道是否可以从存在断言中提取值。也就是说，假设我有以下内容：
这基本上说有一个“最少”的 16 位无符号值。那么，我可以说：
Z3-3.0 愉快地回应：
这真的很酷。但我想做的是能够通过 get-value 提取该模型的各个部分。不出所料，以下似乎都不起作用
在每种情况下，Z3 都正确地抱怨没有这样的常数。(check-sat)显然，Z3 拥有该信息，正如对呼叫的响应所证明的那样。有没有办法通过get-value或其他机制自动访问存在值？
谢谢..
z3 - Z3 使用什么方法来求解无量词位向量公式（QF_BV）？
特别是，它是否使用 DPLL(T)？它是否使用低于/高于近似值？它是否处理单词级别的线性算术？非线性算术呢？
我在论文 Efficiently Solveving Quantiified Bit-Vector Formulas中只发现了“类似于 MathSAT/Boolector 中的简化”的肤浅提及。
什么方法帮助 Z3 在 smtcomp 的 QF_BV 部分获得第一名非常有趣。
binding - z3 ocaml 绑定不起作用（Windows 7）
我没有让 z3 ocaml 绑定在 Windows 7 上工作。这是我遵循的过程。
- 已安装 Objective Caml 版本 3.11.0（Microsoft 工具链）
- 安装了 camlidl-1.05（使用 Microsoft Visual Studio 2008 + cygwin 构建）
- 安装 z3-3.0
- 通过运行“build.cmd”构建z3 ocaml绑定。构建成功。
- 将“build.cmd”生成的文件从 z3/ocaml 复制到 ObjectiveCaml/lib
启动 ocaml 交互并加载“z3.cma”
/li>
有人可以给我一些提示吗？
编辑 1： 在“Z3-3.0\examples\ocaml”中构建示例：
摘自build.cmd
在Visual Studio 2008 命令提示符中执行build.cmd时出现以下错误
在删除-ccopt "%XCFLAGS%"，它工作正常。生成的exe也按预期执行。（请注意，我在 PATH 中有 flexdll）。知道为什么会发生这种情况吗？
scope - 声明在其范围之外仍然有效的符号
Z3 2.x 具有符号声明没有弹出的特性（好吧，可能是错误），例如 Z3 2.x 接受以下代码：
Z3 3.x 不再接受此代码（“未知常量”）。
有没有办法恢复旧的行为？或者另一种方式，如何在范围内声明符号，使得声明（并且只有声明，而不是假设）是全局的，即不弹出？
z3 - Z3 统计：时间衡量什么？
使用 -st 命令选项运行 Z3 3.1 时，我得到了奇怪的统计结果。如果按 Ctrl-C，Z3 报告 total_time < time。否则，如果您等到 Z3 完成：total_time > time。
- “总时间”和“时间”衡量什么？
- 它是一个错误（虽然很小）（上面描述的差异）？
谢谢！