which is more important, number of variables or subexpressions?
I presume the technique detecting shared expressions is applied on most of modern SMT solvers. The performance should be very good when it processes a sequence of similar expressions. However, I got unexpected results after I run Z3 on input1 and input2. Instead of build a long constraint A in "input1", some intermediate variables are defined to map to the sub-expressions of A in "input2". In that case, input1 has less variables, which should be solved faster than input2. I cannot find useful information from the statistic as they are exactly same except the solving time and memory consumed:
I would very much appreciate if someone can answer/explain what affects the performance of the SMT solvers more, the number of variables or number of subexpressions?
I've done some profiling, and it seems that both inputs behave exactly the same in the solver. All (check-sat) commands take exactly the same time. Note that input 2 is a file of size 255KB, but input1 is a file of size 240MB, i.e., this file is about 1000 times larger than the first one. According to my profiler, all of the additional time required to solve these queries is spent in the parser. So, it simply takes a long time to read and check the input; the actual queries are all easy.