来自 std::string 的 cvc4 mkconst in C++ api

Question

我需要在 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));

但我遇到了一些错误

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”标志编译程序

问题已解决。

来自 std::string 的 cvc4 mkconst in C++ api

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

c++

cvc4