Function types are always first-class (#6167)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 22 Mar 2021 17:45:19 +0000 (12:45 -0500)
committerGitHub <noreply@github.com>
Mon, 22 Mar 2021 17:45:19 +0000 (12:45 -0500)
commit519cdc2d4b44a9785ee68d181e2682d74890e89a
tree573fe58b8aa3db82dab1678916ebccb7e4d74ea4
parent64abc6827ec78183605db53e5dd8e2a7a0db59ed
 Function types are always first-class (#6167)

This eliminates one of the dependencies of TypeNode on options. In particular, this makes it so that function types are always considered first-class.

This change makes it so that higher-order types can always be constructed; logic exceptions should occur if they are used in constraints.
src/api/checks.h
src/expr/node_manager.cpp
src/expr/type_node.cpp
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h
test/unit/api/solver_black.cpp
test/unit/api/sort_black.cpp