smtinterpol icon indicating copy to clipboard operation
smtinterpol copied to clipboard

Published 20 hours ago • verified publisher icon ultimate-pa

Performance of FunctionSymbol.checkSort

Open stahlbauer opened this issue 7 years ago • 2 comments

In our application, we construct huge formulas where already the construction process takes thousands of seconds. The function FunctionSymbol.checkSort is a huge bottleneck in this case. Is the .toString() for comparing types really necessary? The formula consists of boolean variables only; why is it necessary to have the type check in this case?

stahlbauer avatar Mar 31 '17 14:03 stahlbauer

Loading a formula in CNF (dimacs with approx 300k lines) with Z3 (and converting it to the corresponding solver-representation) takes less than two seconds, whereas SMTInterpol needs several minutes for the same job.

stahlbauer avatar Mar 31 '17 15:03 stahlbauer

The toString() method should only be called if is a type error. I noticed it may also be called for LIRA logic if implicit int to real casts appear. This should be fixed, but I doubt that is your problem since you are only using boolean variables. Do you have an example that triggers this problem?

jhoenicke avatar Mar 31 '17 16:03 jhoenicke