Should we allow to create several symbols with identical name but different sort?

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.

Apache License 2.0

179 stars 44 forks source link

Should we allow to create several symbols with identical name but different sort? #172

Open kfriedberger opened 4 years ago

kfriedberger commented 4 years ago

Some solvers allow to create symbols (and UFs) with identical names and different sorts. We should discuss whether we want to avoid such inconsistencies and how to react when creating such a symbol. Currently, we support as much as each solver itself allows, if there is no conflict in our corresponding wrapper. This leaves a large gap between some solvers, which might be a problem when switching a solver in some user application.

This issue might be related to #171.

PhilippWendler commented 4 years ago

Should formulas could never be exported to SmtLib, right?

kfriedberger commented 4 years ago

Exporting is not the problem, because that is just a String representation. However, parsing such a query will (hopefully) always result in a crash.