RDL check is a bit too lenient

[Gbury]

The check for real difference logic in the type-checker is currently slightly too lenient. Consider for instance the following problem:

(set-logic QF_RDL)
(declare-const a Real)
(assert (distinct (+ a a) 0))
(check-sat)
(exit)

This is currently accepted by dolmen although the specification states that only the following are allowed:

"Closed quantifier-free formulas with atoms of the form:

• p
• (op (- x y) c),
• (op x y),
• (op (- (+ x ... x) (+ y ... y)) c) with n > 1 occurrences of x and of y,
  where
  • p is a variable or free constant symbol of sort Bool,
  • c is an expression of the form m or (- m) for some numeral m,
  • op is <, <=, >, >=, =, or distinct,
  • x, y are free constant symbols of sort Real.
    "

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:

• when typing the addition, know the context in which the typechecked term appears (i.e. what is "above" the term being typechecked), or
• make it so that the typing of distinct has to know the arithmetic restriction currently in place (i.e. whether we are in difference logic or not).

[Gbury]

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).