Z3最適化：APIを使用して無限を検出する

Question

最適化問題の無限を検出するのが難しいです。例とここでのいくつかの解答で述べたように、無制限の最適化問題の印刷結果は、 "oo"のようなものに等しくなります。

私の質問です：これを検出するためにAPIを使用する方法はありますか？

これまでのところ検索しましたが、唯一の機能は、オブジェクトを返すZ3_mk_fpa_is_infinite(Z3_context c, Z3_ast t)です。問題は：これは正しいアプローチであり、そのZ3_astオブジェクトから無制限のプロパティを取得するにはどうすればよいですか？

Answer 1

現在、無制限の値または無限小を抽出する組み込みの方法はありません。 最適化エンジンでは、 が無制限または厳密な境界にある最大/最小値を表すときに、 "ε"（Real型）と "oo"（Real型またはInteger型）と呼ばれるアドホック定数を使用します。これらの定数のための認識機能は組み込まれておらず、正式にはRealsのドメインに属していません。拡張フィールドに属します。正式には、別の数字フィールドで式を返すか、三つの数字（ε、標準数字、無限大）を返す必要があります。例えば、標準数字5.6は（0,5,6,0）と表され、5.6のすぐ下の数字は（-1,5,6,0）と表され、+無限大は（0、 0,1）。 1つではなく3つの値を返すことは、表現を返すという私の解決策ではありません。返される式を後処理し、必要に応じて値を分解するためにシンボル "oo"と "epsilon"に実際にマッチさせるために、ユーザーに残しています。