Ich benutze Z3 mit SMT2 über C API / JNA / Scala und scheint ziemlich gut zu funktionieren.

Ich möchte versuchen, inkrementell zu lösen. Also übersetze ich das zuerst mitZ3_parse_smtlib2_string:

(declare-fun x () Int)
(assert (>= x 0))
(check-sat)
(get-model)

Dann bekomme ich wieder einZ3_ast, lege es in einen Löser überZ3_solver_assert, überprüfen Sie es mit Z3_solver_check und rufen Sie ein Modell über abZ3_solver_get_model (Wenn der Scheck zufriedenstellend zurückgegeben wurde, ist dies in diesem Beispiel der Fall.) Bisher gibt es kein Problem.

Aber wenn ich zusätzlich so etwas behaupten will:

(assert (= x 1))

Ich bleibe an der Stelle stecken, woZ3_parse_smtlib2_string heißt, weil es sich beschwert, dass x eine unbekannte Konstante ist. Wenn ich hinzufüge, füge ich auch das hinzudeklarieren-Spaß beim zweiten schnipsel erhalte ich einen ungültigen argumentfehler. Sollte diese Variable nicht bereits in der Umgebung existieren? Muss ich die zusätzlichen Parameter von einstellen?Z3_parse_smtlib2_string? Wie kann ich diese aus der zuvor analysierten Formel herausholen?

Auch mit(set-option: global-decls true) hat nicht funktioniert, wie Z3 mir sagt, dass diesDer Optionswert kann nach der Initialisierung nicht mehr geändert werden.

Hat jemand eine Ahnung, wie man dieses Problem löst?