Z3-Optimierung: Unbeschränktheit über API erkennen

Question

Ich habe Schwierigkeiten, Unbeschränktheit eines Optimierungsproblems zu erkennen. Wie in den Beispielen und in einigen Antworten hier angegeben, ist das gedruckte Ergebnis eines unbegrenzten Optimierungsproblems gleichzusetzen mit etwas wie "oo", das interpretiert werden muss (über Zeichenkettenvergleich?).

Meine Frage ist: Gibt es eine Möglichkeit, die API zu verwenden, um dies zu erkennen?

Ich habe jetzt seit einiger Zeit gesucht und die einzige Funktion, die tun könnte, was ich will, ist Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t), die einige Z3_ast Objekt zurückgibt. Das Problem ist: Ist das der richtige Ansatz und wie bekomme ich die unbegrenzte Eigenschaft aus diesem Z3_ast Objekt?

Answer 1

Es gibt derzeit keine integrierte Möglichkeit, unbegrenzte Werte oder Infinitesimale zu extrahieren. Die Optimierungs-Engine verwendet Ad-hoc-Konstanten namens "Epsilon" (vom Typ Real) und "oo" (vom Typ Real oder Integer), wenn maximal/minimal, sind unbegrenzt oder an einer strikten Grenze. Es gibt keinen integrierten Erkenner für diese Konstanten und formal gehören sie nicht zur Domäne von Reals. Sie gehören zu einem Erweiterungsfeld. Formal müsste ich also einen Ausdruck über ein anderes Zahlenfeld zurückgeben oder zurückgeben, was einem Dreifachen von Ziffern entspricht (Epsilon, Standardzahl, unendlich). Zum Beispiel würde eine Standardzahl 5.6 als (0, 5.6, 0) dargestellt, und eine Zahl, die knapp unter 5.6 liegt, wird als (-1, 5.6, 0) dargestellt, und eine Zahl, die + unendlich ist, ist (0, 0, 1). Die Rückgabe von drei Werten anstelle von einem schien mir keine befriedigendere Lösung als einen Ausdruck zu liefern. Ich überlasse es den Benutzern, die zurückgegebenen Ausdrücke nachzubearbeiten und in der Tat nach den Symbolen "oo" und "epsilon" zu suchen, um die Werte zu zerlegen, wenn sie es brauchen.