Questions regarding smt.qi.eager_threshold and rewriter.cache_all

[vwinkler]

Hello, everyone.

I evaluated the runtime impact of some of z3's parameters
but find it difficult to make sense of several of them.
I hope you can give me some pointers.

Among the parameters that influence the runtime for some benchmark are smt.qi.eager_threshold, rewriter.cache_all
and rewriter.flat.

qi.eager_threshold

smt.qi.eager_threshold (double) threshold for eager quantifier instantiation (default: 10.0)

I understand that this parameter influences whether or not eager quantification is applied
to a quantified formula that has just become part of the current knowledge.
Eager quantification depends on the cost of the quantifier instantiation
which is defined by the parameter

qi.cost (string) expression specifying what is the cost of a given quantifier instantiation (default: (+ weight ge
neration))

What determines the value for weight and generation?
Does a higher value for eager_threshold increase or decrease the likelihood of an eager instantiation?

How come there is also a parameter that determines the lazy threshold?

qi.lazy_threshold (double) threshold for lazy quantifier instantiation (default: 20.0)

Isn't lazy quantification the only alternative to eager instantiation?
What if a quantified formula passes the threshold
for both - lazy and eager quantification - or for neither?

rewriter.cache_all

rewriter.cache_all (bool) cache all intermediate results. (default: false)

My understanding is that the rewriter performs certain substitutions within the AST of the
SMT input as preliminary work of the actual proof.
I found an API documentation at
src/ast/rewriter/rewriter.txt
that says

- bool cache_all_results() const;
By default, the rewriter only caches the results of 
non-atomic shared ASTs (get_ref_count() > 1). If true, 
is returned, the rewriter will cache all intermediate results.

Is this purely a runtime optimization within the rewriter?
Does it influence the resulting AST of the whole rewriting step?
What is a non-atomic AST? (Is it just constants and variables?)
What is a shared AST?

Thanks

[NikolajBjorner]

many questions, some take longer to answer than others.
Start with easy to answer:

• What is a shared AST?
  An expression (abstract syntax tree) that is used as argument to more than one immediate function.
  For example, x + x is shared if it occurs in terms f(x + x) and g(x + x).

• What is a non-atomic AST? (Is it just constants and variables?)
  x + x is non-atomic because it contains a function "+" and two arguments.
  atomic expressions have no arguments. We often call them "constants" or 0-ary function applications.

• Does it influence the resulting AST of the whole rewriting step?
  No, it doesn't influence the result. It influences memory usage and memory cache access (looking up in large hash-tables can be an overhead, so we often replace hash-tables with flat arrays exploiting that every expression has also associated a unique small unsigned number).

[NikolajBjorner]

Regarding the quantifier questions, I don't have a reference document handy, so would say that you should look at the code.
There are two versions of the code: in src/smt or src/sat/smt. They use the same priority queue structure. The code in src/smt is well tested and tuned and the code in src/sat/smt may miss things that have to do with quantifier prioritization. The weight of a quantifier is a function of properties of the quantifier, and you can configure z3 to compute weights using your own function. I don't think anybody really uses this feature. There is a default function that is used to compute the weight based directly on the weight annotation.