Z3 C API manage Z3_VAR_AST

Question

C에서 Z3의 Z3_ast에 대한 사용자 지정 인쇄를 작성하려고하지만 Z3_VAR_AST 및 Z3_FUNC_DECL_AST의 Z3_ast_kind를 관리하는 방법을 알지 못하고 Z3_VAR_AST의 Z3_sort를 인쇄하는 방법 만 알고 있습니다 (Z3_get_sort),이 변수 값에 대해서 나는 아이디어가 없다. ??? 그리고 Z3_FUNC_DECL_AST에 대해서는 함수 이름, 매개 변수 수 및 매개 변수를 얻을 수있는 접근자를 찾을 수 없습니다. 니들 좀 도와 줄래? 건배

Answer 1

Z3 배포판의 'python/z3printer.py'파일을 살펴 보시기 바랍니다. Python으로 커스텀 예쁜 프린터를 정의합니다. Z3 python API는 C API의 맨 위에있는 계층입니다. 그래서,이

Z3_VAR_AST에 대해서는 C.에서이 프린터를 변환하는 간단합니다, 기능

unsigned Z3_API Z3_get_index_value(__in Z3_context c, __in Z3_ast a);

변수에 대한 디 Brujin 인덱스를 돌려줍니다. 인덱스의 의미는 다음과 같습니다. http://en.wikipedia.org/wiki/De_Bruijn_index 변수 이름은 수량 한정자 AST에 저장됩니다. 이름은 Z3과 관련이 없습니다. 출력을 좋게하기 위해 저장됩니다. z3printer.py의 코드는 변수 이름과 함께 스택을 유지합니다.

Z3_FUNC_DECL_AST에 대해서는 Z3_VAR_AST보다 처리하기 쉽습니다. 이런 종류의 대서양 표준시는 실제로는 Z3_func_decl입니다.

Z3_symbol Z3_API Z3_get_decl_name(__in Z3_context c, __in Z3_func_decl d); 

Z3_decl_kind Z3_API Z3_get_decl_kind(__in Z3_context c, __in Z3_func_decl d); 

unsigned Z3_API Z3_get_domain_size(__in Z3_context c, __in Z3_func_decl d); 

unsigned Z3_API Z3_get_arity(__in Z3_context c, __in Z3_func_decl d); 

Z3_sort Z3_API Z3_get_domain(__in Z3_context c, __in Z3_func_decl d, __in unsigned i); 

가 다시 파일 z3printer.py이 모든 기능을 사용하여 다음 API는 사용자가 원하는 정보를 추출하는 데 사용할 수 있습니다.