问题标签 [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.
z3 - 为什么 smtlib/z3/cvc4 允许多次声明同一个常量？
我有一个关于declare-constsmtlib 的问题。
例如，
在z3/cvc4中，以下程序不报错：
在 smt-lib-reference 中，它说
(declare-fun f (s1 ... sn) s) ... 如果当前签名中已经存在名称为 f 的函数符号，该命令将报告错误。
所以排序s包含在 的整个签名中x，对吗？
但为什么会这样呢？其背后的动机是什么？
在我的理解中，xis 是变量标识符，一般来说（例如在一些通用编程语言中）我们不允许用不同的类型声明同一个变量。所以我觉得上面的代码最好是报错。
我曾经认为也许z3/smtlib可以支持重新定义？，但不是......
那么上面的代码肯定是错的，为什么不早点报错呢？
PS。如果我使用相同的排序，那么它会报错（那太好了，我希望Bool案例也能报错）：
谢谢。
z3 - 是否可以在 smtlib 中声明函数排序？
例如，
还行吧。
但是，我想通过as?
我应该填写???什么？
它必须是一种排序，但我应该使用哪种排序？
我试过((Int Real) Int)or (-> (Int Real) Int)or (_ (Int Real) Int)，但没有一个是正确的。
是否可以在 smtlib 中声明函数排序？
如果无法声明函数排序，如何f在下面的程序中消歧：
请注意，如果我不使用函数，那没问题：
谢谢。
z3 - 如何调试具有量词的 SMT 脚本？
目前，我对 SMT 求解器的工作原理（E-matching、MBQI 和 CVC4/5 的归纳推理等算法的基础知识）有一些肤浅的了解。但是，通过反复试验进行调试非常令人沮丧。
是否有关于如何调试大量使用量词的 SMT 脚本的指导？
- 写得不好的脚本经常陷入无限循环，但我无法判断这是我的错误，还是响应时间太长。
- SMT 求解器倾向于对用户隐藏内部结构，因此很难弄清楚它为什么会卡住。有没有办法打印“解决上下文”？
或者也许我以错误的方式使用 SMT 求解器？我应该设计自己的验证算法，只使用 SMT 求解器进行本地决策？
任何帮助表示赞赏！
math - 为什么 CVC4 SMT 求解器返回未知（不完整）？
我正在摆弄CVC4 SMT 求解器在线版本（使用 lang = cvc4）。
我使用的不是标准的SMT-LIB 格式，而是CVC4 实现的本机语言，因为它要简单得多。但是，我无法证明非常直接和明显的陈述。例如，第一个 CHECKSAT 给我sat (satisfiable)，这是正确的，但第二个 CHECKSAT 给我unknow。
为什么 CVC4 不能证明这么简单的谓词逻辑表达式？据我了解，SMT 检查是不可判定的，因此，没有程序可以证明所有正确的陈述。但是，这似乎是一个非常简单的案例，所以我想我误解了一些东西。