Overloaded constructors are not always constructor-like

Overloaded constructors are not constructor-like if they appear under a sort injection, but they are currently treated as other constructors.

At present, we need the full OverloadGraph to determine if a symbol is overloaded. We would like to cache this information in the symbol attributes instead. To do that, we need to build the OverloadGraph earlier during verification; that should not be deeply challenging because it is built using only the axiom attributes, but we do need the attributes for all axioms in scope, not only the axioms in scope at the symbol's definition.

• Parameterize OverloadGraph by symbol type.
• Fully parameterize IndexedModule.
• Change module verification so that the IndexedModule parameters change at every stage.
• Definition verifier resolves the import graph, then verifies the axiom attributes.
• Definition verifier constructs a subsort graph and an overload graph using the axiom attributes.
• Module verifier takes the overload graph and subsort graph as inputs.
• Symbol verifier uses the graph to cache overloads in symbol attributes.
• Pattern verifier uses the subsort graph to verify sort injections.

Start by tracing OverloadGraph, IndexedModule, and the definition, module, symbol, and pattern verifiers. Review how axiom attributes and verification stages currently flow, then work through the checklist in order. Done means overload and subsort graphs are built from the required in-scope attributes and consumed by the verifiers as specified.