как скомпилировать пример кода из Z3 под linux

Я скачал z3 для версии для Linux и пытался заставить его работать под Linux, но он не компилировался (я компилировал код примера с помощью gcc). Я получил список неопределенных ссылок от компилятора gcc. Я полагаю, что указал расположение файла lib при компиляции кода. Может ли кто-нибудь дать, какие библиотеки мне нужны, чтобы правильно скомпилировать.


z3
person user1197891    schedule 18.04.2012    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Z3 для Linux скомпилирован с использованием

gcc (Ubuntu/Linaro 4.6.1-9ubuntu3) 4.6.1

Вы можете получить ошибки связывания, если используете несовместимую версию gcc.

Удалось ли вам скомпилировать пример C, поставляемый с Z3? Он находится по адресу: z3/examples/c

Чтобы скомпилировать его, вы должны выполнить

./build.sh

Если это не работает, возможно, вы используете несовместимую версию GCC.

person Leonardo de Moura    schedule 18.04.2012
comment
Да, я выполнил build.sh, но мой компилятор gcc выдает пропуск несовместимости... и не смог найти -lz3-gmp. Я проверил свою версию gcc (gcc Ubuntu/Linaro 4.6.1-9ubuntu3). - person user1197891; 18.04.2012
comment
мой gcc - x64, поэтому я скачал z3 для версии x64, но при выполнении build.sh я получаю список неопределенных ссылок. - person user1197891; 18.04.2012
comment
Я понимаю. Не могли бы вы попробовать скомпилировать, используя: - person Leonardo de Moura; 19.04.2012
comment
Я переписал build.sh gcc -fopenmp -I../../include -L../../lib test_capi.c -lz3 -lgmp -o test_capi и он компилируется. Но gcc нуждается в libgmp.so.3, а у меня в системе установлен libgmp.so.10. поэтому скомпилированный код не смог загрузить библиотеку. - person user1197891; 19.04.2012
comment
Хорошая новость заключается в том, что Z3 4.0 больше не зависит от gmp. Так что в следующей версии проблемы не будет. - person Leonardo de Moura; 19.04.2012

arrow_upward
1
arrow_downward

В xubuntu 11.10 (та же версия gcc) я переместил -lz3-gmp в конец после test_capi.c. Это не первый раз, когда меня выкидывает gcc, потому что -l не было в конце.

gcc -fopemmp -o test_capi -I ../../include -L ../../lib test_capi.c -lz3-gmp

И это работает нормально.

person Lelouch Lamperouge    schedule 24.04.2012