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