명제 모델 쿼리

Question

간단한 명제식을 만족하는 해석기가 반환 한 모델에 액세스하는 방법을 찾고있는 http://research.microsoft.com/en-us/um/redmond/projects/z3/ml/Z3.html에서 Z3 용 OCaml API를 탐색했습니다. 단지 "T"부분이 아닌 Z3의 SAT 부분을 사용하십시오. p 또는 q는 p = true, q = false 모델을 리턴 할 수 있습니다. 내가 찾을 수있는 가장 가까운 것은 모델을 반환하는 solver_get_model입니다. 그러나 모델 유형이 불투명 해 보일 때 어떤 식 으로든 모델에 액세스 할 수있는 방법을 찾지 못했습니다. 함수 기호 (model_get_func_interp)와 연관된 intepretation을 얻기위한 함수를 보았습니다.하지만 그것은 원하는 것이 아니었고 반환 된 정보 (func_interp)로 무엇을 할지를 볼 수 없었습니다. 불투명 한 타입. 내가 볼 수있는 유일한 다른 방법은 모델을 문자열로 변환하는 것이 었습니다. 이것이 유일한 방법입니까?

감사

Answer 1

(공정 경고 : 나 자신을 API입니다 OCaml의를 사용하지 않는, 그래서 나는 부분적으로 C API를 사용하여 내 경험에서이 추측하고있어.)

는 한 번 봐 기능 :

val model_get_const_interp : context -> model -> func_decl -> ast 

값은 context에 대한 통과하고 model은 명확해야한다. 이제 상수의 값을 찾을 때 func_decl을 전달해야하는 이유가 궁금 할 것입니다. 문제는 일반적으로 SMT 세계와 특히 Z3에서 상수는 인수가없는 함수와 같습니다 (그러므로 전제 조건은 문서에 표시된대로 get_arity c a == 0입니다).

이렇게하면 (옵션 유형) AST가 반환됩니다. 다음 단계는 AST를 true 또는 false과 대조하는 것입니다. 이 작업을 수행하는 한 가지 방법은 다음 OP_TRUE 및 OP_FALSE과 결과를 비교할 수 있습니다

val get_decl_kind : context -> func_decl -> decl_kind 

함수를 호출하는 것입니다. 모델을 조회하는 또 다른 방법이 기능 (예를 들어 P ∧ ¬q 등) 어떤 AST 전달할 수

val model_eval : context -> model -> ast -> bool -> ast option 

을 사용하고 같은 방법으로 결과를 판독하는 것을

참고.