사용자 이론 플러그인의 프런트 엔드?

Question

C/C++ 용 smt-lib 또는 유사한 API를 사용하여 사용자 이론 플러그인의 입력을 구문 분석 할 수 있습니까? 예를 들어, 사용자 정의 이론 "test_user_theory.c"에서 입력 파일의 문자열 변수와 상수 문자열을 (비트 벡터로 분해하지 않고) 선언하는 방법은 무엇입니까? 미리 감사드립니다.

Answer 1

기능 z3_parse_smtlib_string, z3_parse_smtlib_file, z3_parse_smtlib2_string, z3_parse_smtlib2_file 사용자가 특정 종류 및 선언으로 임의의 심볼들을 결합 할 수있다. 따라서 이론 플러그인에 정의 된 선언과 함께 유한 한 수의 심볼을 연결할 수 있습니다. 일부 이론에서는 임의의 수의 함수/상수 선언 및 정렬을 정의하므로 완벽한 솔루션은 아닙니다. 예를 들어, 산술 이론은 0, 1, 2 등의 기호를 정의합니다. 배열 이론은 "무한"종류의 정렬을 정의합니다.

이론 플러그인 API는 이제 폐기되었습니다. 이제 Z3 소스 코드를 사용할 수 있으며 Z3 정리 프로 버에 대한 확장은 실제 코드 기반 내에서 직접 구현할 수 있습니다. Z3 소스 코드는 http://z3.codeplex.com에 있습니다. 미래의 릴리스에서 이론 플러그인 API를 제거 할 계획입니다.