Z3 JAVA-API求解器超时

如何设置求解器超时Z3 JAVA API？Z3 JAVA-API求解器超时

返回再次这样一个问题：

这里是我的代码：

Context ctx = getZ3Context(); 
    solver = ctx.MkSolver(); 
    Params p = ctx.MkParams(); 
    p.Add("timeout", 1); 
    solver.setParameters(p);

不行，求解只是运行查询，直到永远。对此有何想法？

来源

2013-03-20 Betsy

我还没有使用的Java API，但综观官方Java example和this snippet，我认为大致如下的东西应该工作：

Solver s = ctx.MkSolver(); 
Params p = ctx.MkParams(); 
p.Add("timeout", valueInMilliseconds); /* "SOFT_TIMEOUT" or ":timeout"? */ 
s.setParameters(p);

来源

2013-03-20 08:02:16

试过。奇怪的结果。当值<3000时，工作;否则，解算器不会停止。 – Betsy 2013-03-21 05:28:18

你能告诉我们你在运行这个平台吗？谢谢！ – 2013-03-25 12:02:02

@ChristophWintersteiger我的平台是Mac OS，谢谢！ – Betsy 2013-11-09 17:58:17

好了，终于找到了解决办法我自己：

Context ctx = getZ3Context(); 
solver = ctx.MkSolver(); 
Params p = ctx.MkParams(); 
/* Also tried 
* p.Add("timeout", 1), 
* p.Add(":timeout", 1), 
* neither worked. 
*/ 
p.Add("soft_timeout", 1); 
solver.setParameters(p);

来源

2013-11-15 00:28:13 Betsy

Z3 JAVA-API求解器超时

回答

相关问题