Allow defining non-theory "intrinsic" functions in problem files

[kjcjohnson]

It's come up a few times that we want a way to quickly add new signatures to the parser. The two big cases are:

• Quickly trying things out before a theory is fully added
• Solver-specific extensions

Using declare-function will get the signature dumped to the output, but we don't necessarily want that, because it makes it harder on tools down the line. Now, in theory, we'd want to add them as regular auxiliary functions and filter the definitions out later, but it makes sense for now to just have a quick way to add extra signatures.

The plan is to add experimental commands:

(define-intrinsic-fun <identifier> (<arg-sorts>) <return-sort>)`
(define-intrinsic-const <identifier> <sort>)
(define-intrinsic-sort <identifier>)

For example, to use cvc5's transcendental theory, one might do:

(define-intrinsic-const real.pi Real)
(define-intrinsic-fun sin (Real) Real)

These function symbols will be used during parsing, but will not be emitted as declare-function or define-function events.

In the future, we'd probably want to support parametric sorts and/or multiple ranks.