Z3Prover/z3

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

rospoly opened this issue · 3 comments

rospoly commented

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 commented

  • 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.

  • 👍3
muraliadithya commented

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 commented
  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.