mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

return non-escaped string value for Python #3080

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-26 09:16:23 -08:00
parent dddd740846
commit f0689546f3
5 changed files with 16 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/api/python/z3/z3.py
View file

@ -10032,10 +10032,13 @@ class SeqRef(ExprRef):
def is_string_value(self):
return Z3_is_string(self.ctx_ref(), self.as_ast())
def as_string(self):
"""Return a string representation of sequence expression."""
if self.is_string_value():
return Z3_get_string(self.ctx_ref(), self.as_ast())
string_length = ctypes.c_uint()
chars = Z3_get_lstring(self.ctx_ref(), self.as_ast(), byref(string_length))
return string_at(chars, size=string_length.value).decode('ascii')
return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
def __le__(self, other):