1

I am using Z3_solver for nonlinear real arithmetics. I also want to set a timeout for the solver. I am using the following code but it looks like that the timeout does not work since the solver runs forever. Can anyone help me in finding out the problem? 

  Z3_solver solver;
  cfg = Z3_mk_config();
  ctx = Z3_mk_context(cfg);

  Z3_symbol logic_symbol = Z3_mk_string_symbol(ctx, "QF_UFNRA");
  solver = Z3_mk_solver_for_logic((Z3_context)ctx, logic_symbol);
  Z3_solver_inc_ref(ctx, solver);

  Z3_params params = Z3_mk_params(ctx);  
  Z3_params_inc_ref(ctx, params);
  Z3_symbol r = Z3_mk_string_symbol(ctx, ":timeout");    
  Z3_params_set_uint(ctx, params, r, 10);
  Z3_solver_set_params(ctx, solver, params);  
  Z3_params_dec_ref(ctx, params);

  Z3_del_config(cfg);


  ....
  Z3_solver_assert(ctx,solver,pred);
  Z3_lbool b = Z3_solver_check(ctx, solver);
user1857364
  • 105
  • 7

1 Answers1

2

Are you using Z3 on Linux or FreeBSD? I recently fixed a timer setting problem that affected these two systems (commit: http://z3.codeplex.com/SourceControl/changeset/9674f511b3c1)

The fix is already available in the "work-in-progress" branch. You can retrieve it using

git clone https://git01.codeplex.com/z3 -b unstable

I tested it using the following python script. BTW, if you find problems with the "unstable" branch, please report them. 

from z3 import *
a1, a2, t1, t2 = Reals('a1 a2 t1 t2'); 
s = SolverFor("QF_NRA")
s.add( a1 + a2 == 2,
       a1*t1 + a2*t2 == Q(2,3),
       a1*t1*t1 + a2*t2*t2 == Q(2,5),
       a1*t1*t1*t1 + a2*t2*t2*t2 == Q(2,7) )
# On my machine, I get unknown when I set the timeout to 1ms.
s.set(timeout=1) 
print s.check()

EDIT: Here are instructions on how to build the Z3 unstable branch (aka "working-in-progress" branch):

Assumption: we will put Z3 source code in the directory ~/code, and that we will not perform a system-wide installation.

cd ~
mkdir -p code
cd code
git clone https://git01.codeplex.com/z3 -b unstable
cd z3 
python scripts/mk_make.py 
cd build 
make

BTW, if you have a multi-core machine, you can speed up the compilation step by using 

make -j N

instead of 

make

where N is the number of cores in your machine.

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • I am using the Linux version. So, do I need to compile it again? I am wondering how much unstable this version is. :) – user1857364 Dec 19 '12 at 01:52
  • Yes, to get the fix you need to recompile it. The unstable version is the "working-in-progress" branch. It has many changes with respect to the official release (v4.3.1), but it should be stable enough to use. If you prefer, you can get just the changes in the commit above and apply them to the official version on your machine. That is, you replace the file `src/util/scoped_timers.cpp` with the one in this commit. – Leonardo de Moura Dec 19 '12 at 02:06
  • I replaced scoped_timers.cpp in my version and recompiled it, but still the problem is there and solver does not stop. – user1857364 Dec 19 '12 at 02:54
  • Did you try the `unstable` branch? – Leonardo de Moura Dec 19 '12 at 03:38
  • It would be great if you could generate an execution log. You just have to add `Z3_open_log("z3.log")` before any other Z3 API call. This command will record all Z3 API calls in the file `z3.log`. I can execute it on my machine to "replay" the exact behavior of your application. – Leonardo de Moura Dec 19 '12 at 03:40
  • I tried unstable branch, but it seems that it only generates libz3.so and not libz3.a under /usr/lib. So, I can't use -lz3 on the command line. – user1857364 Dec 19 '12 at 03:59
  • Also, as I said, the solver runs forever and therefore I have to kill the process. So, no log file is generated in that case. – user1857364 Dec 19 '12 at 03:59
  • To generate `libz3.a`, we have to provide the option `--static` to `mk_make.py`. You can also replace `-lz3` with `libz3.so`. – Leonardo de Moura Dec 19 '12 at 04:14
  • You should get a log file even if you kill the process. I do that all the time on my machine. – Leonardo de Moura Dec 19 '12 at 04:19
  • How can I give you the log file? Shall I email it to you? – user1857364 Dec 19 '12 at 04:27
  • I updated the answer with the build instructions that fixed the problem for user1857364. – Leonardo de Moura Dec 21 '12 at 07:15