epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
122 stars 34 forks source link

Build error on windows 7 (x64) #3

Closed dipakc closed 10 years ago

dipakc commented 12 years ago

Thanks for the project. I had been using it successfully on windows 32-bit. But recently I moved to x64.

On compiling the src on x64 I am getting errors.

Build Command:

D:\OpenSourceProjects\ScalaZ3\psuter-ScalaZ3-6c233b2> gcc -shared -o lib-bin\scalaz3.dll -D_JNI_IMPLEMENTATION_ -Wl,--kill-at -I "D:\ProgramFiles\Java\jdk1.6.0_31\include" -I "D:\ProgramFiles\Java\jdk1.6.0_31\include\win32" -I z3\x64\3.2\include src\c\*.h src\c\*.c z3\x64\3.2\bin\z3.lib 

Errors:

C:\Users\dipakc\AppData\Local\Temp\ccXbtYFp.o:extra.c:(.text+0x2be): undefined reference to `Z3_parse_smtlib2_string'
C:\Users\dipakc\AppData\Local\Temp\ccXbtYFp.o:extra.c:(.text+0x319): undefined reference to `Z3_parse_smtlib_string'
C:\Users\dipakc\AppData\Local\Temp\ccXbtYFp.o:extra.c:(.text+0x6d1): undefined reference to `Z3_parse_smtlib2_file'
C:\Users\dipakc\AppData\Local\Temp\ccXbtYFp.o:extra.c:(.text+0x71e): undefined reference to `Z3_parse_smtlib_file'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x7): undefined reference to `Z3_mk_config'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x45): undefined reference to `Z3_del_config'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0xdf): undefined reference to `Z3_set_param_value'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x11b): undefined reference to `Z3_mk_context'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x159): undefined reference to `Z3_del_context'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x189): undefined reference to `Z3_soft_check_cancel
'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x1f8): undefined reference to `Z3_trace_to_file'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x228): undefined reference to `Z3_trace_to_stderr'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x258): undefined reference to `Z3_trace_to_stdout'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x288): undefined reference to `Z3_trace_off'
C:\Users\dipakc\AppData\Local\Temp\ccrpeejK.o:z3_Z3Wrapper.c:(.text+0x2a4): undefined reference to `Z3_toggle_warning_me
..............
...[Many such similar errors...omitted for clarity]
..............
collect2: ld returned 1 exit status

Few things about my setup

Is anything else needs to be done for compiling the src on windows x64 Please let me know if you need any more information about my installation setup to resolve the problem.

psuter commented 12 years ago

Hi,

I unfortunately have very little experience with Windows 64bit architectures. If I remember correctly, the Z3 distribution for Windows comes with only one .dll file. The build script searches the ...\x64\... directory because that is how the layout is for Linux, and the "fix" you suggest in your second bullet point seems to me like the correct way to proceed.

dipakc commented 12 years ago

As a workaround, I am copying the files from %Z3_INSTALL_DIR%\bin instead of %Z3_INSTALL_DIR%\x64. The compilation succeeds and the generated scalaz3 dll is for 32 bit platform. In this case, however, I need to use 32 bit JVM.

%Z3_INSTALL_DIR%\x64 directory has the following files. Microsoft.Z3.dll msvcp100.dll msvcr100.dll vcomp100.dll z3.dll z3.exe z3.lib

psuter commented 11 years ago

Have you tried with recent builds of Z3? E.g. if you compile it yourself from the Codeplex sources?

MikaelMayer commented 10 years ago

We just released a new version which supports Windows X64. Please try it and give us feedback.