How do I put boolector as a library in my project?

[aytey]

You've asked this same issue here, and on the Z3 GitHub, and both of your issues have no description.

What problem are you facing?

[Flians]

Hi, I used the Boolector in my project. But it's wrong when I built this project on Mac OS.

Undefined symbols for architecture x86_64: "_btor2parser_delete", referenced from: _delete_btor2_parser in libboolector.a(btorbtor2.c.o) "_btor2parser_error", referenced from: _parse_btor2_parser in libboolector.a(btorbtor2.c.o) "_btor2parser_iter_init", referenced from: _parse_btor2_parser in libboolector.a(btorbtor2.c.o) "_btor2parser_iter_next", referenced from: _parse_btor2_parser in libboolector.a(btorbtor2.c.o) "_btor2parser_new", referenced from: _new_btor2_parser in libboolector.a(btorbtor2.c.o) "_btor2parser_read_lines", referenced from: _parse_btor2_parser in libboolector.a(btorbtor2.c.o) "_lgladd", referenced from: _btor_process_skeleton in libboolector.a(btorskel.c.o) _add in libboolector.a(btorlgl.c.o) "_lglassume", referenced from: _assume in libboolector.a(btorlgl.c.o) "_lglbnr", referenced from: _btor_process_skeleton in libboolector.a(btorskel.c.o) _init in libboolector.a(btorlgl.c.o) "_lglclone", referenced from: _sat in libboolector.a(btorlgl.c.o) "_lglderef", referenced from: _deref in libboolector.a(btorlgl.c.o) "_lglfailed", referenced from: _failed in libboolector.a(btorlgl.c.o) "_lglfixate", referenced from: _sat in libboolector.a(btorlgl.c.o) "_lglfixed", referenced from: _btor_process_skeleton in libboolector.a(btorskel.c.o) _fixed in libboolector.a(btorlgl.c.o) "_lglfreeze", referenced from: _inc_max_var in libboolector.a(btorlgl.c.o) "_lglincvar", referenced from: _inc_max_var in libboolector.a(btorlgl.c.o) "_lglinit", referenced from: _btor_process_skeleton in libboolector.a(btorskel.c.o) "_lglmclone", referenced from: _clone in libboolector.a(btorlgl.c.o) "_lglmelt", referenced from: _melt in libboolector.a(btorlgl.c.o) "_lglmeltall", referenced from: _sat in libboolector.a(btorlgl.c.o) "_lglminit", referenced from: _init in libboolector.a(btorlgl.c.o) "_lglrelease", referenced from: _btor_process_skeleton in libboolector.a(btorskel.c.o) _reset in libboolector.a(btorlgl.c.o) _sat in libboolector.a(btorlgl.c.o) "_lglrepr", referenced from: _repr in libboolector.a(btorlgl.c.o) "_lglsat", referenced from: _sat in libboolector.a(btorlgl.c.o) "_lglseterm", referenced from: _sat in libboolector.a(btorlgl.c.o) _setterm in libboolector.a(btorlgl.c.o) "_lglsetopt", referenced from: _btor_process_skeleton in libboolector.a(btorskel.c.o) _enable_verbosity in libboolector.a(btorlgl.c.o) _sat in libboolector.a(btorlgl.c.o) "_lglsetout", referenced from: _sat in libboolector.a(btorlgl.c.o) _set_output in libboolector.a(btorlgl.c.o) "_lglsetprefix", referenced from: _btor_process_skeleton in libboolector.a(btorskel.c.o) _sat in libboolector.a(btorlgl.c.o) _set_prefix in libboolector.a(btorlgl.c.o) "_lglsimp", referenced from: _btor_process_skeleton in libboolector.a(btorskel.c.o) "_lglstats", referenced from: _btor_process_skeleton in libboolector.a(btorskel.c.o) _sat in libboolector.a(btorlgl.c.o) _stats in libboolector.a(btorlgl.c.o) "_lglunclone", referenced from: _sat in libboolector.a(btorlgl.c.o) ld: symbol(s) not found for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation)

[alemuller]

Based on my first experience with the booleactor, I reckon they are probably asking for a minimal example of Makefile for the C API. The documentation lacks command line compile command example, and the examples in repo uses Cmake -- which is not known by many.

[Flians]

I added the following in CMakeLists.txt.

link_directories("${PROJECT_SOURCE_DIR}/lib") 
target_link_libraries (${PROJECT_NAME} boolector)

[aytey]

Given what you shared, your target_link_libraries is pulling in libboolector.a (the static archive), which needs other components of Boolector to correctly link (e.g., libcadical.a and libbtor2parser.a).

This isn't a Boolector-specific question; this is a "how do I link?" question, which is probably more suitable for somewhere like Stack Overflow.

@anhangaba if you have examples of how to link against Boolector "in standalone", why don't you make a PR and see if this example could be included in the source distribution? Then you will potentially help future people :)

[mpreiner]

Minimal cmake example:

list(APPEND CMAKE_PREFIX_PATH "<path to Boolector install prefix>") # This is only required if Boolector was not installed system-wide but in a custom prefix
find_package(Boolector REQUIRED) # If REQUIRED is not specified you should check Boolector_FOUND
target_link_libraries(<your target> Boolector::boolector)

[aniemetz]

If you don't use cmake, as @andrewvaughanj said, this becomes a question rather of how to link against a library in general.

@anhangaba I'm wondering what makes you think that cmake is not known to many. And Boolector using cmake as a build system has nothing to do with how to proceed from after building it. Cmake is not required to build your own project and link against Boolector.

[alemuller]

I just pointed out a friction point that could be avoided with a few lines on the documentation.

@anhangaba I'm wondering what makes you think that cmake is not known to many. And Boolector using cmake as a build system has nothing to do with how to proceed from after building it.

Cmake is a system building tool. I don't think is farfetched to imagine many students and hardware engineers never wrote a cmake script.

[Flians]

Thank you, I have solved this problem.