ACL2 type functions and their corresponding Z3 uninterpreted function type declarations.
Definition:
(defconst *smt-uninterpreted-types* '((realp . "_SMT_.RealSort()") (rationalp . "_SMT_.RealSort()") (real/rationalp . "_SMT_.RealSort()") (integerp . "_SMT_.IntSort()") (booleanp . "_SMT_.BoolSort()") (symbolp . "Symbol_z3.z3Sym")))