Z3에서 완전히 평가 된 결과?

Question

Z3은 종종 중간 기능 묶음으로 정의 된 백 모델을 제공합니다. 그래서

(define-const myArray (Array Bool Int) (_ as-array f)) 
(define-fun f (x Bool) Int (f!10 (k!26 x))) 

... 그리고 예를 들어, 그것은 (내 잘못된 구문을 용서) 다음을 참조하는 것이 일반적이다.

라이브러리 바인딩을 사용하여 Z3을 호출하여 결과를 얻고 결과를 출력하고 실제로 실행할 수있는 함수로 구문 분석 할 수있는 결과를 얻고 싶습니다. 서로 모델을 정의하지 않고 실행할 수있는 단일, 직선 프로그램으로 모델 기능을 구현할 수 있다면 훨씬 쉽습니다.

이것이 가능합니까? 그게 도움이된다면 유한 한 도메인 함수 만 다루고 있습니다.

Answer 1

가능한 경우 중간 기능을 압축하기 위해 차기 버전에서 모델 구성을 업데이트 할 예정입니다. 그러나 동일한 보조 기능이 여러 상황에서 재사용 될 수 있기 때문에 이것이 지수 오버 헤드를 유발할 수있는 경우가 있습니다. 이러한 모델의 경우 보조 기능을 확장하는 것이 적절하지 않습니다. 따라서 사용자는 모델을 후 처리하려는 경우에도 이러한 기능을 계속 처리해야합니다.