s.model()

[bounabbessis]

Dear All ;
my data is very big when I use z3 on Jupiter using python s.model() show me only a few data and not all the resolution and he adds 3 dots like this :
V115 = 20769187434139310514121985316880384,
V112 = 2728907672762512154713559561500415229952,
V5 = 16,
V48 = 365375409332725734621523609091988572144467443712,
V27 = 1461501640053161853571192540423279879110279561216,
V148 = 45851290363324210541710549631459563513625706496,
V79 = 302231454903657293676544,
V65 = 356811923176489970264576233175741464938807328,
V135 = 21778071482940061661655974875633165533184,
V18 = 5070602400912917606124319047744,
V35 = 17179869184,
V51 = 1125899906842624,
V116 = 41538374868278621028243970633760768,
V97 = 79228162514264337593543950336,
V119 = 332306998946228968225951765070086144,
V95 = 11774793475460589153304560491842506161498619904,
V77 = 75557863725914323419136,
...]
I want to extract all the numerical value when i make like this m=s.model()
print(m[0] ) he print me the literal
for example V276 I use Bitvec for these literal

Best regards

[NikolajBjorner]

This should do the trick:

set_option(max_lines=1000000)

Generally, you can set options on the pretty printer.
There are some examples here:
https://github.com/Z3Prover/z3/blob/master/examples/python/tutorial/jupyter/advanced.ipynb

[bounabbessis]

Many thanks for the time given to me . your indication solved me the problem your solver has very good speed . keep the good work it is me the person who trust microsft and don't trust his self Best Regards Le lun. 7 juin 2021 à 00:39, Nikolaj Bjorner ***@***.***> a écrit :

…

This should do the trick: set_option(max_lines=1000000) Generally, you can set options on the pretty printer. There are some examples here: https://github.com/Z3Prover/z3/blob/master/examples/python/tutorial/jupyter/advanced.ipynb — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#5335 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AUL5CLH3BWRWDIBKK5KX6ZLTRQBMJANCNFSM46GQYPDQ> .

[NikolajBjorner]

@bounabbessis
Please stop sending Linkedin invites to this thread