1
Mit der z3/Python-Web-Oberfläche, wenn ich frage:z3/python Reale
x = Real ('x')
solve(x * x == 2, show=True)
ich gut erhalten:
Problem:
[x·x = 2]
Solution:
[x = -1.4142135623?]
Ich dachte, die folgende smt-lib2 Skript die gleiche Lösung würde :
(set-option :produce-models true)
(declare-fun s0() Real)
(assert (= 2.0 (* s0 s0)))
(check-sat)
Leider bekomme ich unknown mit z3 (v3.2).
Ich vermute, das Problem ist mit dem nichtlinearen Begriff (* s0 s0), die die Python-Schnittstelle irgendwie nicht leiden. Gibt es eine Möglichkeit, in smt-lib2 dasselbe zu programmieren, um ein Modell zu erhalten?
Ganz richtig! Und das ist, was es für den Wert von s0 zurückgibt: ((s0 (root-obj (+ (^ x 2) (- 2)) 1))) Ich bin gespannt, wie die "root-obj" Funktion wird interpretiert; und wie andere Tools, die Z3 abfragen, eine reelle Zahl daraus erhalten können. –
Das frage ich mich auch. Hoffentlich kann @Leo es klären. – pad
Z3 4.0 verwendet Wurzel-Obj, um algebraische irrationale Zahlen darzustellen. Es besteht aus einem univariaten Polynom und einem Index. Das obige root-obj stellt die erste Wurzel von x^2 - 2 dar, also -1,41 ... Wir können das SMT 2.0 bitten, die Ergebnisse in Dezimalschreibweise mit '(set-option: pp-decimal true) anzuzeigen. ". Ich habe Dezimalzahlen standardmäßig in z3py verwendet, weil das Ziel darin besteht, eine Menge zu erreichen, die nicht an das Beschränkungs-Lösen und die algebraische Zahlentheorie gewöhnt ist. –