Z3 버전 3.2에서 버전 4.0으로 마이그레이션

Question

Z3 버전 3.2에서 버전 4.0으로 마이그레이션 중입니다. 그러나 이전에 작동했던 코드는 더 이상 직접 작동하지 않으며 동일한 이유를 찾으려고합니다. 나는 전체 코드를 매우 단순한 선언과 주장으로 줄 였지만 여전히 효과가 없을 것이다.

1. 어떻게 - 코드는 -

   long intSort = Z3_mk_int_sort (context); 
   long periodDeclStr = Z3_mk_string_symbol(context, "period"); 
   long periodVar = Z3_mk_const(context, periodDeclStr, intSort); 
   
   long solver = z3_mk_solver(); 
   long zero = Z3_mk_int (context, 0, intSort); 
   long eqSt = Z3_mk_eq(context, periodVar, zero);  
   Z3_solver_assert (context, solver, eqSt); 
   

   문제는 Z3_mk_eq()

   내가 같은 오류가 발생 번째 마지막 문이다 - 다음과 같이

   내 질문

   WARNING: invalid function application, sort mismatch on argument at position 2 
   WARNING: (define = arith arith Bool) applied to: 
   period of sort arith 
   0::Int of sort Int 
   

   있습니다 이 오류를 디버깅 하시겠습니까? 이 버전은 여전히 ​​버전 3.2에서 작동하지만 해결사는 없습니다.
2. 컨텍스트에 변수를 추가 한 후에 만 ​​솔버를 만들어야합니다. 솔버를 만든 후 컨텍스트에 변수를 추가 할 수 있습니까? 아니면 솔버를 다시 만들어야합니까?

---

문제를 일으켜 죄송합니다. 솔버와 컨텍스트를 혼합하여 솔버에 전달했습니다. 그러나 문제는 아직 해결되지 않은 채로 남아 있습니다. Z3_ast_to_String() API에 크래시가 발생했습니다. 문제점을 해결하고 업데이트를 게시하려고 노력할 것입니다.

Answer 1

API 상호 작용을 정확하게 기록하는 Z3 4.0과 상호 작용 로그가 있습니다. 이 기능을 사용하여 JNI 레이어 및 발견 된 버그를 디버깅 할 수 있어야합니다. Z3_open_log()를 사용하여 로그를 엽니 다. 컨텍스트를 만들기 전에 로그를 열어야합니다. 상호 작용의 하위 집합 만 캡처하려는 경우 언제든지 로그를 닫을 수 있습니다 (Z3_close_log()). ".log"라는 접미어를 사용하여 로그를 재생하고 Z3을 실행할 수 있습니다. 또는/log 옵션 (즉, "Z3.exe/log")을 사용하여 Z3을 실행하여 상호 작용을 재생할 수 있습니다.

Answer 2

Z3_mk_eq(context, periodDecl, zero) 대신 Z3_mk_eq(context, id, zero)을 원하지 않으십니까?