마찬가지로 previously asked Z3은 재귀 함수에 대한 모델을 제공 할 수 없습니다. 그러나 재귀 함수에 대한 정의가없는 모델이 충분하다는 사실을 Z3 (Java API를 통해 선호)에게 알리는 것이 가능합니다 (또는 실제로 관심이있는 함수를 선택합니다. 본질적으로 비 상수 함수의 모델은 필요 없습니다) ? 분명히 일부 함수에는 모델이 없어도 sat를 반환하는 쿼리가 생성 될 수 있습니다. 기본적으로, 사용자는이 기능들이 어떤 모델을 가지고 있는지 확인해야합니다. 그러나 Z3 또는 SMT 솔버가 작동하는 방식과 같이 실제로 실현할 수 없다고 가정합니다. 즉, Z3에 표현식을 평가하는 재귀 함수 모델이 필요하다고 가정합니다.모델과 재귀 함수
한정사에 대한 MBQI 구현은 재귀 함수와 함께 제대로 작동하지 않습니다. 트릭을 수행 할 수있는 한 가지가 있습니다. 재귀 함수 정의를 바운드 - 재귀 함수로 바꿉니다. 함수를 탐색하고자하는 전개 수를 세는 추가 인수를 추가합니다. 나머지 입력에서 재귀 함수를 적용 할 때마다 depth 매개 변수를 설정하십시오. 대수 데이터 형식 Peano 숫자 또는 정수를 사용할 수 있습니다. 기호식 자동 도구 키트는이 접근법을 사용합니다.
Amin, Leino 및 Rompf (2014)의 "SMT 해석기로 계산하기"에 대한 Nikolaj Bjorner의 답변에서 아이디어를 탐구하는 한 종이를 발견했습니다.
또한, 나는 satisfiability 결정 할 수 연속적 때까지 재귀 함수에 호출을 전개 수터, Köksal 및 Kuncak (2011)에 의해 "Satisfiability 모듈로 재귀 프로그램"을 발견했다.