Для соединения со статически скомпилированным z3 требуются дополнительные библиотеки в Linux - PullRequest
Новая
       23

Для соединения со статически скомпилированным z3 требуются дополнительные библиотеки в Linux

1 голос
/ 28 марта 2019

Я использовал CMake для компиляции статической версии (довольно недавнего) z3, используя: 

cmake -DBUILD_LIBZ3_SHARED=false -DCMAKE_INSTALL_PREFIX=/opt/z3-devel -G "Unix Makefiles" ../

Теперь, когда я статически связываю библиотеку с программой на C ++, произнесите небольшую вариацию примера z3: 

#include"z3++.h"
using namespace z3;

int main(int argc, char** argv) {
  config conf;
  context c(conf);
  expr x = c.int_const("x");
  expr y = c.int_const("y");
  expr z = c.int_const("z");
  goal g(c);
  g.add( ((2*x)+y)+z == 4);
  g.add( (x+(2*y))+z == 4);
  g.add( x+y == 4);
  std::cout << g << "\n";
  tactic t(c, "fm");
  apply_result r = t(g);
  std::cout << r << "\n";
  return 0;
}

через 

g++ -c -I /opt/z3-devel/include -static -o main.o main.cc
g++ -static -L /opt/z3-devel/lib64 -o main main.o -lz3

Я получаю длинный список неопределенных ошибок ссылок. Что решает проблему, так это добавление -lgomp -pthread -lrt -ldl в качестве дополнительных библиотек. Компоновщик выдает следующее предупреждение: 

/usr/bin/ld: /usr/lib/gcc/x86_64-redhat-linux/8/libgomp.a(target.o): in function `gomp_target_init':
(.text+0x32c): warning: Using 'dlopen' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking

Тем не менее, программа отлично работает на моей машине и на Starexec.

Является ли это сочетание статической и динамической связи лучшим, что я могу сделать? Разве эти библиотеки уже не должны быть статически связаны с libz3.a? У меня есть статические версии gomp, pthread и rt, доступные в системе.

...