z3 cache

[HNYuuu]

Is your feature request related to a problem? Please describe. After running test_fopen and drawing flame graph, I found that the sat_cut takes lots of time. Moreover, I found that there are only 41 distinct sets of constraints sent to sat_cut without considering the order. In other words, if we can cache the result for these sets of constraints, the analysis process can be accelerated dramatically.

Describe the solution you'd like Add a mapping, named z3_cache in each state. For each of items, the key is the string, i.e., the constraints expressed in SMT format, the value is True or False, indicating sat or not, respectively.

[HNYuuu]

Currently, we use a dict to store mappings from constraints to their sat or unsat. Moreover, to achieve incremental solving, we also maintain the corresponding solver for each set of constraint, which brings in huge memory overhead. In btree test, we can not achieve the 5o3u case, including more than 100 paths, within 128GB memory.

Therefore, we will try to merge the solver into state, and collect the constraints met along paths.

[HNYuuu]

This is done, and all these features are merged into the 'active' branch.

Close this issue.