Open Gbury opened 4 months ago
Idea for a fix for future me: shadow the typing of the distinct
builtin in the arith module of the typechecker, and document that the order of applications of the typing extensions is important (i.e. arith needs to go before core/base, at least for smtlib).
The check for real difference logic in the type-checker is currently slightly too lenient. Consider for instance the following problem:
This is currently accepted by
dolmen
although the specification states that only the following are allowed:The term
(distinct (+ a a) 0)
does not conform to any of the allowed forms.This is quite annoying since it effectively breaks the locality (and independance) of checking the invariants of real difference logic: to enforce the spec, one would have to either:
distinct
has to know the arithmetic restriction currently in place (i.e. whether we are in difference logic or not).