[SMT-LIB] declare-, define- and set-logic

[cok@frontiernet.net]

Cesare, Aaron, et al.

In section 5.1.1 of the SMT-LIB document it states that set-logic must occur before define-fun and define-sort (and assert and check-sat), but does not mention declare-fun and declare-sort.

Is there a reason for the distinction?

Prior to a set-logic no theories are defined, but one could define user-defined sorts (declare-sort) and thus some user-defined function symbols (declare-fun); one could just as well use define-fun and define-sort.

So it seems all of declare-sort, declare-fun, define-sort, define-fun should be allowed before set-logic, or (my choice) none of them.

- David