Manquant (str.to-int s) dans Z3 4.5.1

Question

J'utilise Z3 4.5.1 avec succès avec des chaînes et des opérations telles que la sous-chaîne, la longueur de chaîne, les comparaisons de chaînes, etc., comme cet exemple:

(declare-const s1 String) 
(declare-const s2 String) 
(declare-const i Int) 
(assert (= s1 "97\x00098\x0099###$$")) 
(assert (= s2 (str.substr s1 2 (- (str.len s1) 2)))) 
(assert (= "\x00058\x0099###$$" (str.replace s2 "9" "5"))) 
(check-sat) 
(get-value (s1 s2 i)) 

Cependant, lorsque je tente d'ajouter str.to-int:

(declare-const s1 String) 
(declare-const s2 String) 
(declare-const i Int) 
(assert (= s1 "97\x00098\x0099###$$")) 
(assert (= s2 (str.substr s1 2 (- (str.len s1) 2)))) 
(assert (= "\x00058\x0099###$$" (str.replace s2 "9" "5"))) 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
(assert (= 98 (str.to-int "000098"))) 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
(check-sat) 
(get-value (s1 s2 i)) 

Je reçois cette erreur:

(error "line 8 column 35: unknown function/constant str.to-int") 

Je suis perplexe parce que "to-int" apparaît dans la documentation le long d'autres opérations de chaîne qui fonctionnent parfaitement. J'utilise cette documentation: Z3str3 Input Language. Toute aide est très appréciée, merci !!

Answer 1

Z3 utilise str.to.int et int.to.str depuis un moment. Le format SMTLIB2 pour les chaînes n'a pas été finalisé à ce stade non plus.