How to load the Z3 build libs for Eclipse Plugin?

[nasmdh]

Hello,

I developed an Eclipse plugin that makes use of Z3 Build. Thank to the Z3 community, the integration was successful until I was forced to change a laptop from Dell (Intel) to HP (AMD). I tried to replicate my successful integration on the new laptop, it didnt work - I dont know why (I thought I knew the hack).

Basically, on the previous laptop, I copied the Z3 build to the Eclipse plugin project , at the root. Then, added "com.microsoft.z3.jar" to the Classapth, located in the Plugin.xml Runtime tab. I also added the jar file as a referenced library - Everything was fine. I tried the same procedure on the new laptop, it didnt work. I tried almost every suggestion from this forum as well from others, nothing could work for me.

I am sure this issue is addressed somehow, somewhere, but I could not find one that worked for me. By the way, I even tried to relate the Z3 build from a simple java project, it didnt work. It seems like unless the Java application is inside the build directory, nothing works!!

The following error is when the Z3 build dir is configured as a native library under com.microsoft.z3.jar Exception in thread "main" java.lang.UnsatisfiedLinkError: C:\Users...\TestZ33\build\libz3java.dll: Can't find dependent libraries at java.lang.ClassLoader$NativeLibrary.load(Native Method) at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1941) at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1857) at java.lang.Runtime.loadLibrary0(Runtime.java:870) at java.lang.System.loadLibrary(System.java:1122) at com.microsoft.z3.Native.<clinit>(Native.java:14) at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:87) at TestZ3.main(TestZ3.java:9) I hope I am not rambling around...please help, tnx

Best, /Nas

[NikolajBjorner]

I wish I knew about something useful to say, but I am not sure. You have two options for building Z3. They differentiate in how Java gets installed post-build. So I suggest to try the cmake based build system if you haven't already.

[nasmdh]

Thank Nikolaj Bjorner for replying quickly. Yes, I also tried with cmake before (ninja, mingw: x64, JAVA enabled), it does not compile well (I had to ignore template errors for successful compilation). I really dont know how to fix these compilation errors- there is little support for these problems in the net.

$ cmake -G "MinGW Makefiles" -DCMAKE_BUILD_TYPE=Release -DENABLE_TRACING=FALSE -DBUILD_JAVA_BINDINGS=ON ../

Z3 version 4.5.1.0 Found simple git working directory Found git directory "C:/Users/.../git/z3/.git" Adding git dependency "C:/Users/.../git/z3/.git/HEAD" Adding git dependency "C:/Users/.../git/z3/.git/refs/heads/master" Using Git hash in version output: d2ec927844120a4c26236e80b9bd8ae302de51f3 Using Git description in version output: z3-4.5.0-1654-gd2ec9278 CMake generator: MinGW Makefiles Build type: RelWithDebInfo PYTHON_EXECUTABLE: C:/python36/python.exe Detected target architecture: i686 C++ compiler supports -std=c++11 Platform: Windows Not using libgmp Found OpenMP_CXX: -fopenmp
Found OpenMP: TRUE
Using OpenMP Not using API_LOG_SYNC C++ compiler supports -Wall Treating only serious compiler warnings as errors C++ compiler supports -Werror=odr C++ compiler supports -fvisibility=hidden LTO disabled CMAKE_CXX_FLAGS: " -Werror=odr " CMAKE_EXE_LINKER_FLAGS: "" CMAKE_STATIC_LINKER_FLAGS: "" CMAKE_SHARED_LINKER_FLAGS: "" CMAKE_CXX_FLAGS_RELWITHDEBINFO: "-O2 -g -DNDEBUG" CMAKE_EXE_LINKER_FLAGS_RELWITHDEBINFO: "" CMAKE_SHARED_LINKER_FLAGS_RELWITHDEBINFO: "" CMAKE_STATIC_LINKER_FLAGS_RELWITHDEBINFO: "" Z3_COMPONENT_CXX_DEFINES: $<$:Z3DEBUG>;$<$:LEAN_DEBUG>;$<$:_EXTERNAL_RELEASE>;$<$:_EXTERNAL_RELEASE>;-D_WINDOWS;-D_MP_INTERNAL;$<$:_TRACE> Z3_COMPONENT_CXX_FLAGS: -std=c++11;-fopenmp;-mfpmath=sse;-msse;-msse2;-Wall;-fvisibility=hidden Z3_DEPENDENT_LIBS: -lpthread Z3_COMPONENT_EXTRA_INCLUDE_DIRS: C:/Users/nmd02/git/z3/build/src;C:/Users/nmd02/git/z3/src Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: -fopenmp CMAKE_INSTALL_LIBDIR: "lib" CMAKE_INSTALL_BINDIR: "bin" CMAKE_INSTALL_INCLUDEDIR: "include" CMAKE_INSTALL_PKGCONFIGDIR: "lib/pkgconfig" CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: "lib/cmake/z3" Adding component util Adding component lp Adding rule to generate "lp_params.hpp" Adding component polynomial Adding rule to generate "algebraic_params.hpp" Adding component sat Adding rule to generate "sat_asymm_branch_params.hpp" Adding rule to generate "sat_params.hpp" Adding rule to generate "sat_scc_params.hpp" Adding rule to generate "sat_simplifier_params.hpp" Adding component nlsat Adding rule to generate "nlsat_params.hpp" Adding component hilbert Adding component simplex Adding component automata Adding component interval Adding component realclosure Adding rule to generate "rcf_params.hpp" Adding component subpaving Adding component ast Adding rule to generate "pp_params.hpp" Adding component rewriter Adding rule to generate "arith_rewriter_params.hpp" Adding rule to generate "array_rewriter_params.hpp" Adding rule to generate "bool_rewriter_params.hpp" Adding rule to generate "bv_rewriter_params.hpp" Adding rule to generate "fpa_rewriter_params.hpp" Adding rule to generate "poly_rewriter_params.hpp" Adding rule to generate "rewriter_params.hpp" Adding component normal_forms Adding rule to generate "nnf_params.hpp" Adding component model Adding rule to generate "model_evaluator_params.hpp" Adding rule to generate "model_params.hpp" Adding component tactic Adding component substitution Adding component parser_util Adding rule to generate "parser_params.hpp" Adding component grobner Adding component euclid Adding component core_tactics Adding component sat_tactic Adding component arith_tactics Adding component nlsat_tactic Adding component subpaving_tactic Adding component aig_tactic Adding component solver Adding rule to generate "combined_solver_params.hpp" Adding component ackermannization Adding rule to generate "ackermannization_params.hpp" Adding rule to generate "ackermannize_bv_tactic_params.hpp" Adding component interp Adding rule to generate "interp_params.hpp" Adding component cmd_context Adding component extra_cmds Adding component smt2parser Adding component proof_checker Adding component fpa Adding rule to generate "fpa2bv_rewriter_params.hpp" Adding component macros Adding component pattern Adding rule to generate "pattern_inference_params_helper.hpp" Adding component bit_blaster Adding component smt_params Adding rule to generate "smt_params_helper.hpp" Adding component proto_model Adding component smt Adding component bv_tactics Adding component smt_tactic Adding component sls_tactic Adding rule to generate "sls_params.hpp" Adding component qe Adding component duality Adding component muz Adding rule to generate "fixedpoint_params.hpp" Adding component dataflow Adding component transforms Adding component rel Adding component pdr Adding component clp Adding component tab Adding component bmc Adding component ddnf Adding component duality_intf Adding component spacer Adding component fp Adding component nlsat_smt_tactic Adding component ufbv_tactic Adding component sat_solver Adding component smtlogic_tactics Adding rule to generate "qfufbv_tactic_params.hpp" Adding component fpa_tactics Adding component portfolio Adding component smtparser Adding component opt Adding rule to generate "opt_params.hpp" Adding component api Adding component api_dll Adding component fuzzing Found Java: C:/Program Files/Java/jdk1.8.0_144/bin/java.exe (found version "1.8.0.144") Found JNI: C:/Program Files/Java/jdk1.8.0_144/lib/jawt.lib
Building documentation disabled Configuring done Generating done

$ mingw32-make

Scanning dependencies of target util [ 0%] Building CXX object src/util/CMakeFiles/util.dir/approx_nat.cpp.obj [ 0%] Building CXX object src/util/CMakeFiles/util.dir/approx_set.cpp.obj [ 0%] Building CXX object src/util/CMakeFiles/util.dir/bit_util.cpp.obj [ 0%] Building CXX object src/util/CMakeFiles/util.dir/bit_vector.cpp.obj [ 0%] Building CXX object src/util/CMakeFiles/util.dir/cmd_context_types.cpp.obj In file included from C:/Users/.../git/z3/src/util/symbol.h:26:0, from C:/Users/.../git/z3/src/util/cmd_context_types.h:20, from C:\Users...\git\z3\src\util\cmd_context_types.cpp:18: C:/Users/.../git/z3/src/util/string_buffer.h: In member function 'void string_buffer::append(int)': C:/Users/.../git/z3/src/util/string_buffer.h:85:53: error: there are no arguments to 'sprintf_s' that depend on a template parameter, so a declaration of 'sprintf_s' must be available [-fpermissive] sprintf_s(buffer, ARRAYSIZE(buffer), "%d", n); ^ C:/Users/.../git/z3/src/util/string_buffer.h:85:53: note: (if you use '-fpermissive', G++ will accept your code, but allowing the use of an undeclared name is deprecated) C:/Users/.../git/z3/src/util/string_buffer.h: In member function 'void string_buffer::append(unsigned int)': C:/Users/.../git/z3/src/util/string_buffer.h:95:53: error: there are no arguments to 'sprintf_s' that depend on a template parameter, so a declaration of 'sprintf_s' must be available [-fpermissive] sprintf_s(buffer, ARRAYSIZE(buffer), "%d", n); ^ C:/Users/.../git/z3/src/util/string_buffer.h: In member function 'void string_buffer::append(long int)': C:/Users/.../git/z3/src/util/string_buffer.h:105:54: error: there are no arguments to 'sprintf_s' that depend on a template parameter, so a declaration of 'sprintf_s' must be available [-fpermissive] sprintf_s(buffer, ARRAYSIZE(buffer), "%ld", n); ^ src\util\CMakeFiles\util.dir\build.make:162: recipe for target 'src/util/CMakeFiles/util.dir/cmd_context_types.cpp.obj' failed mingw32-make[2]: [src/util/CMakeFiles/util.dir/cmd_context_types.cpp.obj] Error 1 CMakeFiles\Makefile2:446: recipe for target 'src/util/CMakeFiles/util.dir/all' failed mingw32-make[1]: [src/util/CMakeFiles/util.dir/all] Error 2 Makefile:128: recipe for target 'all' failed mingw32-make: *** [all] Error 2

However, if I ignore the template related errors with $ mingw32-make i, it compiles successfully. But, I could not generate the examples with mingw32-make examples from the "build" location, so i concluded that something went wrong during the compilation. For this reason, I am using nmake (without cmake), which compiled beautifully.

If someone has succeeded on calling the Z3 Build from a different location, please share your experience. I am trying different ways...., not succeeded yet.

Cheers, /Nas

[nasmdh]

My problem is solved!! A silly mistake from my side, but a bit tricky. In short, the Eclipse environment was not getting the latest environment settings from the system (Windows 10), once changed. Therefore, I had to restart my workstation to observe the effect on the Eclipse plugin, after adding the Z3 build directory path into the Path environment variable, which I didn't for so many changes.

Eventually my Eclipse plugin is interacting with the Z3 SMT Solver successfully. My working environment is:

HP, AMD, x64 , Windows 10 java version "1.8.0_144" Java(TM) SE Runtime Environment (build 1.8.0_144-b01) Java HotSpot(TM) 64-Bit Server VM (build 25.144-b01, mixed mode) Version: Mars.2 (4.5.2)

How it worked for me, I ...

1. Cloned Z3 (Z3 Full Version: 4.5.1.0)

2. Built it with nmake, following the READEME file on

Building Z3 on Windows using Visual Studio Command Prompt

3. Added the Z3 build directory to the Path environment variable

4. RESTARTED MY WORKSTATION!!! Otherwise, restarting Eclipse won't update the Path variable (I dont know why) that the plugin uses. I found out this as follows: Right-mouth click on the plugin-project->Run As->Run Configurations... On the popup window click the Environment tab->Select, from the list of check boxes, look for the Path settings, and compare it with the one from Windows 10 setting. You can also find out the same thing programmatically using the System.getProperty() method.

5. Also copy com.microsoft.z3.jar from the build directory and past it into the root of the Eclipse plugin, which allows successful compilation of the plugin. It can also be added as external jar.

Cheers, /Nas

[NikolajBjorner]

Thanks for sharing. These kinds of issues tend to happen to more than one person.