search

Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
BSD 2-Clause "Simplified" License
80 stars 17 forks source link

More information for reserved id, and adjusted errors #193

Closed Gbury closed 1 year ago

Gbury commented 1 year ago

This commits adds more information to "reserved" ids in the typechecker, to distinguish ids reserved for solver use (e.g. those starting with '@' or '.' in smt2), from ids that may be used in some models (such as div0). This allows to correctly decide when to error out when a reserved id becomes shadowed.

Will close #185