回答情况：
提问时间：
问题标签：
我只是想编译这个文件helloworld.cpp#include <cvc4/cvc4.h>int main()但是它给了我这个错误helloworld.cpp:(.text+0xac): undefined reference to `CVC4ExprManager::mkVar(std::__cxx11::bas
浏览 7修改于2016-08-27得票数 0
回答已采纳
我目前正在使用CVC4来解决以下形式的公式：问题是，CVC4有很多处理量词的选项:有一堆cegqi，一堆fmf，还有mbqi等等。我知道CVC4是有可能的，因为他们在SMT比赛的上表现得很好，但是我找不到用于那场比赛的具体论据。
浏览 4提问于2017-11-26得票数 1
我正在尝试用CVC4做一些实验。not (= x y)))(get-value (x y))(check-sat)当我使用CVC4CVC4是否将x和y视为两个不同的“对象”，从而给出它所提供的输出？
浏览 5修改于2017-04-22得票数 0
回答已采纳
我尝试使用cvc4中的位向量旋转C++ API，但是当涉及到运算符表达式时，这个API有点混乱。使用以下代码(摘录)：#include <cvc4/cvc4.h>
using namespace CVC4;
what(): Illegal argument detected
CVC4::Expr CVC4::
浏览 4提问于2016-12-23得票数 0
回答已采纳
我根据他们的手动cvc4 从源代码中构建了。我运行了make check，它运行得很完美，然后是sudo make install。declare-const j Int)
(assert (= (+ i j) 9))
(get-value (i j))CVC4
浏览 0提问于2018-06-14得票数 0
回答已采纳
所以我是在花了一些时间学习cvc4之后才开始学习boolector的。有了它，只需使用boolector_print_model就可以打印模型。不幸的是，cvc4的文档页面目前已经关闭，我不明白如何在Java语言中对cvc4做同样的事情。 有谁能帮忙做这件事吗？ 例如，您可以帮助我查看this示例的模型。
浏览 23修改于2020-10-04得票数 1
我在摆弄 (用lang = cvc4)。
我使用的不是标准，而是，因为它要简单得多。然而，我不能证明我的发言非常直截了当和明显。为什么CVC4不能证明这样一个简单的谓词逻辑表达式？据我所知，SMT检查是不可判定的，因此，没有程序可以证明所有正确的语句。不过，这似乎是一个很简单的例子，所以我想我是误会了。
浏览 1提问于2021-12-07得票数 0
回答已采纳
文件如下所示：(declare-fun x () Int)(check-sat)CVC4 Error:这是不同的。
浏览 4提问于2020-03-25得票数 0
回答已采纳
我正在修改CVC4对集合和关系的支持，并希望能够使用product运算符来构建两个集合的笛卡尔乘积。然而，这个运算符只适用于关系。这是一个输入到CVC4的示例：(declare-sort S1 0)(declare-fun es1 ()es2)))(error " Relational operator operates on non-relations (sets of tuples)")
然后，我发现CVC
浏览 1提问于2019-05-02得票数 1
使用此代码：using namespace CVC4;
ExprManager使用带有github标签1.5的cvc4版本。
浏览 1提问于2017-09-01得票数 1
回答已采纳
我试图使用Z3和CVC4运行下面的unsat示例。如果我将"\x00"替换为(seq.unit #x00)，那么对于Z3来说这不是问题，但是CVC4抱怨说它不知道seq.unit。str.indexof (str.substr AB_serial_1_version_1 0 (- 16 0)) "\x00" 0) (- 0 1)))下面是命令行调用：下面是cvc4在使用seq.unit行时抱怨的地方：
(erro
浏览 1提问于2018-06-16得票数 2
回答已采纳
我在安德鲁·雷诺兹和co -authors的论文中发现了以下信息：“SMT中递归函数的模型发现”但我已经安装了目前版本的CVC4，-fmf-乐趣在CVC4 4中是不可用的?
浏览 4提问于2016-04-06得票数 0
回答已采纳
我有一个程序，可以动态生成SMT格式的表达式，我正在尝试将这些表达式连接到CVC4，以测试可满足性并得到模型。我想知道是否有一种通过CVC4 C++ API解析这些字符串的方便方法，或者最好将生成的SMT代码存储在一个文件中并将输入重定向到cvc4可执行文件。
浏览 2提问于2020-06-04得票数 0
回答已采纳
下面的文件通过了Z3约束求解，而CVC4标记了一个解析错误："Symbol 'None‘之前声明为一个变量“。我已经在windows上使用CVC4 1.4和CVC1.5进行了测试。
浏览 2提问于2017-08-22得票数 1
我正在尝试从FreeBSD上的源代码编译，但在配置时遇到了一个小问题- GMP找不到，尽管共享对象显然位于公共路径中：libgmp.alibgmp.solibgmp.so.10.1.3libgmpxx.lalibgmpxx.so.4/sbin:/bin:/usr/sbin:/usr/bin:/usr/games:/usr/local/sbin: \
/
浏览 4提问于2014-09-10得票数 1
我可以为如下查询获取多个模型吗？ (set-logic LIA)(assert (< x 20))(get-model) 而不是仅仅 sat(define-fun x () Int 0)
) 我想得到0，1，-1，2，...
浏览 38修改于2021-06-09得票数 0
回答已采纳
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号