Smtml.Mappings_intfSourceMappings Module. This module defines interfaces for interacting with SMT solvers, including term construction, type handling, solver interaction, and optimization. It provides a generic interface for working with different SMT solvers and their functionalities.
The M module type defines the core interface for interacting with SMT solvers, including term construction, type handling, and solver interaction.
The M_with_make module type extends M with a functor for creating instances of M and a flag indicating availability.
The S module type defines a simplified interface for interacting with SMT solvers, focusing on model evaluation, solver interaction, and optimization.
The S_with_fresh module type extends S with a functor for creating fresh instances of S and a flag indicating availability of the mappings.