Как установить время ожидания для z3_solver с помощью C-API?

Question

Я использую Z3_solver для реальной нелинейной арифметики. Я также хочу установить время ожидания для решателя. Я использую следующий код, но похоже, что тайм-аут не работает, так как решатель работает вечно. Может ли кто-нибудь помочь мне выяснить проблему?

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

Answer 1

Вы используете Z3 на Linux или FreeBSD? Недавно я исправил проблему установки таймера, которая затронула эти две системы (коммит: http://z3.codeplex.com/SourceControl/changeset/9674f511b3c1)

Исправление уже доступно в ветке "в процессе работы". Вы можете получить его, используя

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

Я проверил это, используя следующий скрипт Python. Кстати, если вы обнаружите проблемы с "нестабильной" веткой, сообщите о них.

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

РЕДАКТИРОВАТЬ: Вот инструкции о том, как построить Z3 unstable филиал (иначе называемый "незавершенный" филиал):

Предположение: мы поместим исходный код Z3 в каталог ~/codeи что мы не будем выполнять общесистемную установку.

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

Кстати, если у вас есть многоядерный компьютер, вы можете ускорить этап компиляции, используя

make -j N

вместо

make

где N количество ядер в вашей машине.