无法使用 CVC4 C++ API 编译代码

Can't compile code with CVC4 C++ API

本文关键字：API 编译 代码 C++ CVC4      更新时间：2023-10-16

我只是想编译这个文件helloworld.cpp 

#include <iostream>
#include <cvc4/cvc4.h>
using namespace CVC4;
int main() {
        ExprManager em;
        Expr helloworld = em.mkVar("Hello World!", em.booleanType());
        SmtEngine smt(&em);
        std::cout << helloworld << " is " << smt.query(helloworld) << std::endl;
        return 0;
}

使用g++ helloworld.cpp -lcvc4 -o helloworld -lcvc4 -Wno-deprecated。但是它给了我这个错误

/tmp/cc9SFpL4.o: In function `main':
helloworld.cpp:(.text+0xac): undefined reference to `CVC4::ExprManager::mkVar(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, CVC4::Type, unsigned int)'
collect2: error: ld returned 1 exit status

帮助!

我已经安装了CVC4，在/etc/apt/sources.list中添加了repo链接，然后调用sudo apt-get install cvc4 libcvc4-dev libcvc4parser-dev。

编辑:我打错了g++ helloworld.cpp -lcvc4 ...，我用的是g++ helloworld.cpp -o helloworld -lcvc4 -Wno-deprecated。实际上我用了所有的组合和排列

这似乎是OP环境的问题。r4C9rAyrd6A1和我都能够在本地机器上编译示例。具体的问题可能是OP的编译器希望-lcvc4链接器标志在其他标志之后，例如评论中提到的g++ helloworld.cpp -Wno-deprecated -o helloworld -lcvc4。

相关文章：