Come posso ottenere valori Python reali da un modello Z3?Z3/Python che ottiene i valori di python dal modello
E.g.
p = Bool('p')
x = Real('x')
s = Solver()
s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))
s.check()
print s.model()[x]
print s.model()[p]
stampe
-1.4142135623?
False
ma questi sono oggetti Z3 e non pitone oggetti galleggiante/bool.
so che posso controllare i valori booleani con is_true
/is_false
, ma come posso elegantemente convertire interi/real/... torna a valori utilizzabili (senza passare attraverso le stringhe e tagliando via questo ?
simbolo in più, per esempio) .
Hai provato 'bool (s.model() [x])' e 'galleggiante (s.model() [p])'? –
Sì, ma ciò non funziona (correttamente): 'bool (s.model() [p])' restituisce 'True', quando dovrebbe essere' False' e 'float (s.model() [x]) 'getta un'eccezione' AttributeError: AlgebraicNumRef istanza non ha attributo '__float __' ' – tqx