SMT-Lib parser is strict

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.

Other

103 stars 40 forks source link

SMT-Lib parser is strict #330

Open kunalsheth opened 1 year ago

kunalsheth commented 1 year ago

SMT-Lib when reading LIRA / LRA formulas, the parser requires that reals have a "." Many smt-lib formulas do not comply with this spec, would it be possible to enhance the parser so it can interpret integers as reals depending on context?