CODEWITHSUNDEEP
z3
user1857364
user1857364

Reputation: 105

how to set timeout for z3_solver using C-API?

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);

Upvotes: 1

Views: 1376

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

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.

Upvotes: 2

Related Questions