search

ultimate-pa / smtinterpol

SMTInterpol interpolating SMT solver
GNU Lesser General Public License v3.0
60 stars 17 forks source link

Performance of FunctionSymbol.checkSort #28

Open stahlbauer opened 7 years ago

stahlbauer commented 7 years ago

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 commented 7 years ago

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.

jhoenicke commented 7 years ago

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?