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

Question

I need to change "123" into a const in c++ what I coded as

ExprManager em;

Rational i = Rational("123",10);

Expr expri = em.mkConst(i);

or

Integer i = Integer("123", 10);

Expr epri = em.mkConst(Rational(i,1));

but I got some error

Undefined symbols for architecture x86_64: "___gmpq_canonicalize", referenced from: __gmp_expr<__mpq_struct [1], __mpq_struct [1]>::canonicalize() in ex1-4f9d4d.o "___gmpq_clear", referenced from: __gmp_expr<__mpq_struct [1], __mpq_struct [1]>::~__gmp_expr() in ex1-4f9d4d.o "___gmpz_clear", referenced from: __gmp_expr<__mpz_struct [1], __mpz_struct [1]>::~__gmp_expr() in ex1-4f9d4d.o "___gmpz_init_set", referenced from: __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&) in ex1-4f9d4d.o "___gmpz_init_set_si", referenced from: __gmp_expr<__mpz_struct [1], __mpz_struct [1]>::init_si(long) in ex1-4f9d4d.o ld: symbol(s) not found for architecture x86_64

Answer 1

上述问题是由于缺少 GMP 库引起的。在 Mac 上使用“brew install gmp”安装 GMP。使用“-lgmp”标志编译程序

问题解决了。