Setting Z3 Solver

Question

Setting Z3 Solver

wombatwen opened this issue 8 years ago · 1 comments

Hi,
I use Eclipse and my OS is win10 x64. I follow the installation guide of Z3 solver and have successfully built Z3 with --java flag. Now I have "com.microsoft.z3.jar", but have no idea how to link jbse with z3 solver.
Is there any suggestion?

Thanks,

ShengHan

Answer 1 · 2017-04-07T12:08:11.000Z

Hi and sorry for the late answer. JBSE does not link to Z3 via the com.microsoft.z3.jar but by exchanging commands through pipes. You just need to inform JBSE about the location of the z3.exe file by the method jbse.apps.run.RunParameters.setExternalDecisionProcedurePath(String). Maybe you will also need to tweak a bit the COMMANDLINE_LAUNCH_Z3 constant in jbse.apps.run.Run and change it as follows:

 private static final String COMMANDLINE_LAUNCH_Z3   = " /smt2 /in /t:10";

Best,
Pietro