Faster param symbol management

[smuenzel]

*::get_param_descrs is called many times during the a run of z3 (in my case, a cegis loop), which causes string_hash to be approximately 5% of the runtime of the program, according to callgrind.
The issues are constant strings that are getting converted to symbols on every call, which requires hashing of the string so that we can check the global symbol table.

I have a proof of concept patch here, which turns a lot of the symbols into static entries in the symbol table.

It's only meant for discussion, not for merging, since afaict, it currently only works in debug mode (since the initialization at startup requires some resources that aren't created yet), and requires the library to eagerly initialize the symbol table. However, it does remove the 5% hashing overhead.

[NikolajBjorner]

What is the use case where get_param_descr() gets called repeatedly?
I tried to see if it is internal and didn't spot where this would be.
A fix seems to better avoid symbol alltogether because they are also prone to lock contention (there is a global unique symbol table to intern strings). The fix would change the types used to index params_ref to something else.
Either std::string or a symbol32 (32 byte fixed-length string, enough to hold symbol names).

[smuenzel]

I'm also slightly confused by what's happening.
However, I'm changing the timeout of the solver on different runs, and somehow (according to callgrind), my ~600 invocations of the solver lead to 20million string hashes.
The call graph seems to be something like:

tactic2solver::collect_param_descrs
-> binary_tactical::collect_param_descrs
-> unary_tactical::collect_param_descrs
-> simplify_tactic:collect_param_descrs
-> th_rewriter::get_param_descrs
-> *::get_param_descrs for different rewriters

And callgrind says there is a cycle at binary_tactical::collect_param_descrs (maybe just a red herring)

[NikolajBjorner]

More likely it is:

z3/src/api/api_solver.cpp

Line 394 in 981c82c

param_descrs r;

Every time you set a parameter it collects parameter descriptions to validate the parameter.
A way around is to cache the descriptions.

            if (to_solver(s)->m_descrs.size() == 0) {
                to_solver_ref(s)->collect_param_descrs(to_solver(s)->m_descrs);
                context_params::collect_solver_param_descrs(to_solver(s)->m_descrs);
            }
            params.validate(to_solver(s)->m_descrs);

where in api_solver.h we have added:

struct Z3_solver_ref : public api::object {
    scoped_ptr<solver_factory> m_solver_factory;
    ref<solver>                m_solver;
    params_ref                 m_params;
    symbol                     m_logic;
    scoped_ptr<solver2smt2_pp> m_pp;
    scoped_ptr<cmd_context>    m_cmd_context;
    mutex                      m_mux;
    event_handler*             m_eh;
    param_descrs               m_descrs;

[smuenzel]

I've applied your suggestion, runtime for string_hash has decreased from 5% to 0.32% of my program.
Thanks!