Z3/Python che ottiene i valori di python dal modello

Question

Come posso ottenere valori Python reali da un modello Z3?

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) .

Answer 1

Per i valori booleani, è possibile utilizzare le funzioni is_true e is_false. I valori numerici possono essere interi, razionali o algebrici. Possiamo utilizzare le funzioni is_int_value, is_rational_value e is_algebraic_value per testare ciascun caso. Il caso intero è il più semplice, possiamo usare il metodo as_long() per convertire il valore intero Z3 in un lungo Python. Per i valori razionali, possiamo usare i metodi numerator() e denominator() per ottenere gli interi Z3 che rappresentano il numeratore e il denominatore. I metodi numerator_as_long() e denominator_as_long() sono scorciatoie per self.numerator().as_long() e self.denominator().as_long(). Infine, i numeri algebrici sono usati per rappresentare numeri irrazionali. La classe AlgebraicNumRef ha un metodo chiamato approx(self, precision). Restituisce un numero razionale Z3 che approssima il numero algebrico con precisione 1/10^precision. Ecco un esempio su come utilizzare questi metodi. E 'disponibile anche online all'indirizzo: http://rise4fun.com/Z3Py/Mkw

p = Bool('p') 
x = Real('x') 
s = Solver() 
s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p)) 
s.check() 
m = s.model() 
print m[p], m[x] 
print "is_true(m[p]):", is_true(m[p]) 
print "is_false(m[p]):", is_false(m[p]) 
print "is_int_value(m[x]):", is_int_value(m[x]) 
print "is_rational_value(m[x]):", is_rational_value(m[x]) 
print "is_algebraic_value(m[x]):", is_algebraic_value(m[x]) 
r = m[x].approx(20) # r is an approximation of m[x] with precision 1/10^20 
print "is_rational_value(r):", is_rational_value(r) 
print r.numerator_as_long() 
print r.denominator_as_long() 
print float(r.numerator_as_long())/float(r.denominator_as_long())