Z3 최적화 : API를 통해 무한대를 감지합니다.

Question

최적화 문제의 무한 함을 감지하는 데 어려움이 있습니다. 예제와 여기에 나온 답변에서 말한 것처럼, 무제한 최적화 문제의 인쇄 된 결과는 "oo"와 같습니다 (문자열 비교를 통해 해석되어야합니다).

내 질문에 : API를 사용하여이를 감지 할 수있는 방법이 있습니까?

저는 지금 약간의 시간을 검색했습니다. 원하는 것을 할 수있는 유일한 기능은 개체를 반환하는 Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t)입니다. 문제는 다음과 같습니다. 올바른 방법이며 Z3_ast 객체에서 무한 속성을 가져 오는 방법은 무엇입니까?

Answer 1

현재 제한되지 않은 값 또는 극소값을 추출 할 수있는 기본 제공 방법이 없습니다. 최적화 엔진은 이 제한되지 않거나 엄격한 경계에있는 최대/최소를 나타낼 때 "ε"(Real 유형) 및 "oo"(Real 또는 Integer 유형)라는 ad-hoc 상수를 사용합니다. 이 상수들에 대한 내장형 인식기가 없으며 형식적으로 Reals의 도메인에 속하지 않습니다. 확장 필드에 속합니다. 그래서 공식적으로, 나는 다른 숫자 필드를 통해 표현을 반환하거나 숫자의 세 배 (엡실론, 표준 숫자, 무한)를 반환해야 할 것입니다. 예를 들어, 표준 숫자 5.6은 (0, 5.6, 0)으로 표시되고, 5.6 아래의 숫자는 (-1, 5.6, 0)으로 표시되며 + 무한대 숫자는 (0, 0, 1). 하나가 아닌 3 개의 값을 리턴하는 것은 표현을 반환하는 것으로 더 이상 만족스럽지 못한 해결책으로 보였다. 반환 된 표현식을 사후 처리하고 필요하면 기호를 "oo"및 "엡실론"과 일치시켜 사용자가 값을 분해하도록 사용자에게 맡기고 있습니다.