Vielen Dank an Josh und Leonardo für die Beantwortung der vorherigen Frage.

Ich habe noch ein paar Fragen.

<1> Betrachten Sie ein anderes Beispiel.

<code>(exists k) i * k > = 4 and k > 1.
</code>

Dies hat eine einfache Lösung i> 0. (sowohl für Int als auch für Real)

Als ich jedoch versuchte zu folgen,

<code>(declare-const i Int)
(assert (exists ((k Int)) (and (>= (* i k)  4) (> k 1))))
(apply (using-params qe :qe-nonlinear true))
</code>

Z3 Quantifizierer konnte hier nicht eliminiert werden.

Es könnte jedoch für einen Real-Fall beseitigt werden. (Wenn i und k beide reelle Zahlen sind) Ist die Quantifikatoreliminierung für ganze Zahlen schwieriger?

<2> Ich verwende die Z3 C-API in meinem System. Ich füge einige nichtlineare Einschränkungen für Ganzzahlen mit Quantifizierern in meinem System hinzu. Z3 prüft derzeit die Erfüllbarkeit und gibt mir ein korrektes Modell, wenn das System erfüllbar ist.

Ich weiß, dass diese Bedingungen nach der Eliminierung der Quantifizierer auf lineare Bedingungen reduziert werden.

Ich dachte, dass z3 die Quantifizierung automatisch durchführt, bevor die Erfüllbarkeit überprüft wird. Aber da es in Fall 1 oben nicht möglich war, denke ich, dass es normalerweise ein Modell ohne Quantifier Elimination findet. Hab ich recht?

Derzeit kann z3 die Einschränkungen in meinem System lösen. Bei komplexen Systemen kann dies jedoch fehlschlagen. Ist es in diesem Fall eine gute Idee, die Eliminierung von Quantifizierern mit einer anderen Methode ohne z3 durchzuführen und z3 später Einschränkungen hinzuzufügen?

<3> Ich kann mir vorstellen, echte nichtlineare Einschränkungen anstelle von ganzzahligen nichtlinearen Einschränkungen in meinem System hinzuzufügen. Wie kann ich in diesem Fall z3 erzwingen, die Quantifizierer-Eliminierung mithilfe der C-API durchzuführen?

<4> Ist dies eine gute Idee, um z3 für die Quantifier Elimination zu zwingen? Oder findet es ein Modell normalerweise intelligenter, ohne Quantifier Elimination durchzuführen?

Vielen Dank.