Z3 JAVA-API для тайм-аута решателя

Question

Как установить тайм-аут решателя для Z3 JAVA API?

Вернуться к этому вопросу еще раз:

Вот мой код:

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

Не работает, решатель только при выполнении запроса навсегда. Есть идеи об этом?

Answer 1

Я не использовал API Java, но из Глядя на официальный Java example и в this snippet, я бы предположить, что что-то по следующим направлениям должно работать:

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

Answer 2

Хорошо, наконец, нашли решение самостоятельно:

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