z3 표현식을 중위 표현식으로 변환하는 방법은 무엇입니까?

Question

Z3에서 boolExpression을 중위 표현으로 변환하고 싶습니다. 예를 들어, z3 표현식 (> = t 3)이 있고, 중위 문자열 "t> = 3"을 얻고 싶습니다. C#으로 구현할 기존 Z3 API입니까?

Answer 1

아니요, 공식 API는 중침 표기법으로 표현식을 표시 할 수 없습니다. 이 기능은 탐색 식에 대한 API 위에 구현 될 수 있습니다. Z3 Python API는 중위 프린터를 구현합니다. 사실 Python과 같은 구문과 HTML 수학과 같은 구문을위한 두 가지를 구현합니다. 이 프린터의 소스 코드는 Z3 배포판에 포함되어 있습니다. 이 코드는 파이썬으로 작성되었지만 모든 프로그래밍 언어로 쉽게 변환 될 수 있습니다. 코드는 python\z3printer.py에 있습니다.