Show what patterns Z3 infers for quantifiers

0
votes

I would like to see what patterns Z3 is using for some quantifiers in my formulas.

This comment suggests that it may be possible, but I couldn't find any more details.

How do I get Z3 to print this information?

1
triggersz3quantifiers
Currently you can only print this information via debug traces in debug mode, there is no convenient way to display that information in a readable way. It's still on the todo-list and I've started adding some things toward this in a separate branch, but it will still take time to make that convenient to use. – Christoph Wintersteiger
@ChristophWintersteiger Can you tell me how to do it in debug mode (even if it's unreadable)? – James Wilcox
I found a way to do it using a debug build of Z3. I remain hopeful that this will be possible in normal builds someday. – James Wilcox

1 Answers

1
votes

Based on a helpful comment from Christoph, I found that building Z3 in debug mode (pass -d to mk_make.py during the build process) and then passing -v:10 on the command line to the resulting Z3 prints inferred patterns.