Z3 static library

Nov 14, 2012 at 12:35 AM

Hi,

I'm not sure how to build the static z3 library with the latest version. Is it still possible?

Thank you!

 

Coordinator
Nov 14, 2012 at 5:59 AM

The latest version does not build a static library containing all modules. 

I will try to add support for that in the future.

In the meantime, you can try to hack the Makefile. The new build system creates a static library for each module (subdirectory) in the build directory. The static library in the previous versions is the union of these static libraries.

Coordinator
Nov 14, 2012 at 5:05 PM

I added an option --staticlib to mk_make.py. If we use it, then make will build libz3.lib (on Windows) and libz3.a (on OSX and Linux). The changes are already available in the "unstable" branch.

Nov 14, 2012 at 5:32 PM

It worked. Thank you!

Dec 19, 2012 at 3:40 PM
Edited Dec 19, 2012 at 3:42 PM

If you are working on Linux, you can also do the following:

  1. Build Z3 as described in the README file.
  2. Once the compilation is finished, run the following command in the build directory (you should already be there):
    ar rs libz3.a $(find . -name *.o)
    
Mar 13, 2013 at 3:13 PM
Is this option (--staticlib) working on windows ? I only get a z3.lib which is 3Ko big. If I lib.exe all the libs of the libz3.dll file, I get a much bigger file. (160 Mo)

AG.
Coordinator
Mar 13, 2013 at 4:35 PM
The --staticlib option is for OSX, Linux and FreeBSD only.
In Windows, the small lib file contains only references to the functions exposed by the Z3 DLL.
The 160 Mb is correct. If we combine all object files in the smaller .lib files, we also get that
Nov 14, 2013 at 3:34 PM
Hi,

I can build libz3.a library follow the instruction above but I cannot compile a program.

For instance,

I try to compile C example by the following command (On Ubuntu 13.10 64bit)
gcc -o test test_capi.c libz3.a

Please tell me how to fix that.

Cheers.
Coordinator
Nov 14, 2013 at 5:39 PM
trucnguyenlam wrote:
I try to compile C example by the following command (On Ubuntu 13.10 64bit)
gcc -o test test_capi.c libz3.a
Its not clear what exactly the problem is, but I guess it doesn't find libz3.a?

Libraries are usually used via the -L and -l parameters. To force the use of static libraries, I believe gcc needs the -static option as well, for instance:
gcc -static -o test test_capi.c -L/path/to/z3 -lz3
In this special case, I think it should also work if instead of just the library name, the path is also supplied, e.g.,
gcc -o test test_capi.c /path/to/z3/libz3.a
Cheers,
Christoph
Nov 18, 2013 at 12:51 PM
Thanks,

However I cannot compile the above by the following command (After sudo make install Z3)

gcc -static -o test test_capi.c -lz3

Got this error:
/usr/bin/ld: cannot find -lz3
collect2: error: ld returned 1 exit status

Could someone please tell me how to fix this.

Thanks.
Coordinator
Nov 18, 2013 at 5:45 PM
Hi,

could you verify that /usr/lib/libz3.a exists and is readable? If not, something went wrong with the installation.

Note that to link statically, a few other options might be required because the static z3 library depends on other libraries which need to be linked to as well. Using g++ instead of gcc gets rid of the standard C++ libraries, but on Ubuntu 13.10 x64, we also need to add OpenMP, pthreads, and rt. On my system, this command line works:
g++ -static -o test test_capi.c -lz3 -lgomp -pthread -lrt
For dynamic linking, these extra options are not required; thus this is enough:
gcc -o test test_capi.c -lz3
Cheers,
Christoph