meaning of the output with smt.qi.profile=true

[rospoly]

I am running z3 4.8.9 with the option smt.qi.profile=true.
The output is in the form:

[quantifier_instances] "my_qid" : inst. : max. gen. : max. cost

I suppose "inst." stands for how many times the quantifier gets instantiated. Am I correct here?
What is the meaning of "max.gen." and "max.cost"?

Thanks!

[NikolajBjorner]

• Generation is associated with the number of quantifier instantiations that were used to produce a given quantifier instantiation. This is to understand which instantiations trigger other instantiations. For example, if you have a quantifier forall x . p(x) => p(x + 1), and fact p(0). Then p(1) has generation 1, p(2) has generation 2, etc.

• Cost is associated with a heuristic that gives weights to quantifier instantiations. There is a default cost function that gets applied to quantifiers and it is also possible to define cost functions through configuration. Roughly, the cost of a quantifier instantiation should correspond to the preference of when to instantiate it.

[muraliadithya]

Thanks @NikolajBjorner, that was very useful. I'm want to extract instantiation information from z3 directly. I'm looking specifcally within smt_quantifier.cpp and some related files, but I have two questions:
(i) What should I do to get z3 to print the actual term that the quantifier is being instantiated along with the qid, max_cost, etc in the above code?
(ii) What class/file in general should I look at if I want to extract information about quantifier instantiations?

[NikolajBjorner]

1. To print terms, use either the axiom profiler tool that reassembles and displays terms for you, or add print statements in the code on your own using the mk_pp or mk_bounded_pp class constructors that can be combined with std::ostream.
2. smt_quantifier, smt_model_checker, smt_model_finder, smt_context.