问题标签 [cvc4]
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.
smt - 使用 SMT 求解器求解 dimacs 实例似乎很慢（SMT2 格式）
我正在将我的问题转换为 SMT，并且我注意到 SMT 求解器（MathSat5 和 CVC4）在求解 sat 实例时速度很慢。我的暂停是我的翻译中有一些东西让它变慢了。
我附上了一个示例 cnf 实例和 smt2 翻译以供参考，下面我提供了较大实例的求解器时间（不包括翻译时间）以比较 MathSat5、CVC4 和 MiniSat。
那么有没有人知道为什么这些时代截然不同？PS。cvc4 说它花费了 5.862 秒：theory uf Symmetry_breaker
谢谢
smt - 在 SMT-LIBv2 中访问复合排序（数据类型）的成员
根据秒。SMT-LIBv2 Language and Tools: A Tutorial 的3.9.3 可以在 SMT-LIBv2中声明这样的复合排序：
我正在使用 CVC4，它似乎接受这种语法。但是我如何访问这些元素？我尝试了以下方法（以及我在网上找到的各种变体）：
但看起来这些运算符只适用于向量和数组。我找不到任何使用这种复合排序的示例，也找不到有关在教程或语言标准中访问这些元素的任何内容。它是如何完成的？还是我完全误解了这个功能的用途？
我的应用程序：我想对一个时间问题进行编码，并希望以将旧状态转换为新状态的状态转换函数的形式进行编码，因此我可以在试验系统时编写如下内容：
z3 - z3 是否支持其输入约束的有理算术？
事实上，SMT-LIB 标准是否有理性的（不仅仅是真实的）排序？通过它的网站，它没有。
如果 x 是有理数并且我们有一个约束 x^2 = 2，那么我们应该返回“不可满足”。最接近编码该约束的方法如下：
z3 返回一个解，因为实数中有一个解（无理数）。我确实了解 z3 有自己的有理库，例如，在使用 Simplex 算法的改编解决 QF_LRA 约束时，它会使用它。在相关说明中，是否有支持输入级别有理数的 SMT 求解器？
cvc4 - CVC4 最多期望运算符“ITE”的 3 个参数，找到 5 个
将以下文件输入到 cvc4 时，出现以下错误：
该文件test.txt是：
命令行：
smt - 为了在 CVC4 中处理递归函数定义，需要为递归函数启用有限模型查找模式
我在 Andrew Reynolds 和合著者“SMT 中递归函数的模型查找”的论文中找到了以下信息
“如果启用了 CVC4 的递归函数的有限模型查找模式（使用命令行选项 --fmf-fun）”
但是我已经安装了当前版本的 CVC4，--fmf-fun 在 CVC4 中不可用？你能指导我吗？
optimization - CVC4 最小化/最大化模型优化
CVC4 是否可以像 Z3 那样最大化或最小化位向量的结果模型？
谢谢。
z3 - y=1/x, x=0 实数可满足？
在 SMT-LIB 中：
这个模型应该是 SAT 还是 UNSAT？
z3 - 在 SMT 中使用 define-fun-rec
我目前正在尝试使用define-fun-rec 编写SMT 脚本。我已经使用 Z3 4.4.2 版和 CVC4 1.4 版进行了测试。据我所知，这些是两者的最新版本，并且都支持该功能*。但是，两者似乎都不认识该命令。
（我根据 Nikolaj 的回复对此进行了一些更改。它仍然给出错误消息。）具体来说，给定：
Z3 输出：
CVC4 输出：
我最好的猜测是我需要设置某种标志，或者我需要使用一些特定的逻辑，但是我在使用 define-fun-rec 找到任何类型的详细说明或示例时遇到了很多麻烦。任何意见，将不胜感激。谢谢！
*Z3 支持：Z3 中如何处理递归函数？
c++ - 无法使用 CVC4 C++ API 编译代码
我只是想编译这个文件helloworld.cpp
使用g++ helloworld.cpp -lcvc4 -o helloworld -lcvc4 -Wno-deprecated. 但它给了我这个错误
帮助！
我已经安装了CVC4添加 repo 链接/etc/apt/sources.list，然后调用sudo apt-get install cvc4 libcvc4-dev libcvc4parser-dev.
编辑：我打错了g++ helloworld.cpp -lcvc4 ...我用过g++ helloworld.cpp -o helloworld -lcvc4 -Wno-deprecated的 . 实际上我使用了所有的组合、排列。
z3 - (_ bv0 32), (_ bv1 16) ... 在 SMT2 基准测试中的含义
我注意到这是一些 SMT2 基准，像(_ bv0 32), (_ bv16 32), ... 这样的符号被使用，例如，在：
QF_FP/schanda/spark/zeros_consistent_2.smt2
但是，这不是在理论声明中对此类符号的引用：
http://smtlib.cs.uiowa.edu/theories.shtml
对此有何评论？它们的含义是什么？
谢谢 ！