1

我正在使用 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);
4

1 回答 1

2

您在 Linux 或 FreeBSD 上使用 Z3 吗？我最近修复了一个影响这两个系统的计时器设置问题（提交：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()

编辑： 以下是关于如何构建 Z3unstable分支（又名“工作中”分支）的说明：

假设：我们将 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您的机器中的内核数在哪里。

于 2012-12-19T01:25:53.460 回答