избегайте использования sudo для использования z3 ++. h в качестве библиотеки

Question

Я использую z3prover впервые, прочитав большинство связанных ответов, я заметил, что мне нужно попробовать: sudo make install. Как можно пропустить ссылку z3 в / usr / bin и / usr / lib, чтобы использовать z3 ++. h в моем собственном проекте c ++. (bcs Я заметил, что не у всех есть sudoer, я надеюсь, что мой код будет работать без sudoer.

Answer 1

Вам необходимо скомпилировать исходный код z3, если вы хотите иметь возможность использовать его в своих проектах C / C ++. Компиляция даст вам библиотеку для ссылки. Если вы просто загружаете исходный код, вы можете найти заголовки, но не можете связать и, следовательно, не можете создавать свои собственные исполняемые файлы.

Но для этого вообще не требуется sudo доступ. Правильный способ сделать это на самом деле объясняется на странице https://github.com/Z3Prover/z3, прямо в README. Грубо говоря, они go выглядят так:

python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install

Обратите внимание, что в параметре prefix в первой строке вы указываете z3, куда все устанавливать. Измените этот путь на место, где у вас есть доступ для записи. Таким образом, вам не нужен sudo доступ.

Для успешной компиляции проекта вам нужно указать компилятору, где искать динамические c библиотеки и заголовочные файлы. Спросите отдельно, если у вас возникли проблемы.

Answer 2

Если вы используете GCC в качестве компилятора, вы должны добавить опцию -I для вашего проекта следующим образом:

g++ -Iz3_path/include -Lz3_path/lib  -lz3