cvc4 mkconst from std::string in C++ api

本文关键字：in C++ api string cvc4 from std mkconst 更新时间：2023-10-16

我需要在 c++ 中将 "123" 更改为常量我编码为什么

ExprManager em;
Rational i = Rational("123",10);
Expr expri = em.mkConst(i);

或

Integer i = Integer("123", 10);
Expr epri = em.mkConst(Rational(i,1));

但我遇到了一些错误

建筑的未定义符号x86_64： "___gmpq_canonicalize"，引用自： __gmp_expr<__mpq_struct [1]， __mpq_struct [1]>：：canonicalize() 在 ex1-4f9d4d.o 中 "___gmpq_clear"，引用自： __gmp_expr<__mpq_struct [1]， __mpq_struct [1]>：：~__gmp_expr() 在 ex1-4f9d4d.o 中 "___gmpz_clear"，引用自： __gmp_expr<__mpz_struct [1]， __mpz_struct [1]>：：~__gmp_expr() 在 ex1-4f9d4d.o 中 "___gmpz_init_set"，引用自： __gmp_expr<__mpq_struct [1]， __mpq_struct [1]>：：__gmp_expr(__gmp_expr<__mpz_struct [1]， __mpz_struct [1]> const&， __gmp_expr<__mpz_struct [1]， __mpz_struct [1]> const&) 在 ex1-4f9d4d.o 中 "___gmpz_init_set_si"，引用自： __gmp_expr<__mpz_struct [1]， __mpz_struct [1]>：：init_si(long) 在 ex1-4f9d4d.o 中 LD：在建筑x86_64中找不到符号

上述问题是由缺少 GMP 库引起的。在 Mac 上安装了带有"brew install gmp"的 GMP。使用"-LGMP"标志编译程序

问题解决了。