module type S = Solver_intf.SThe S module type, which defines the core solver interface.
In this module, constraints are handled in a 'batch' mode, meaning that the solver delays all interactions with the underlying SMT solver until it becomes necessary. It communicates with the underlying solver only when a call to Solver_intf.S.check, Solver_intf.S.get_value, or Solver_intf.S.model is made.
module Batch (_ : Mappings_intf.S) : SThe Batch module is parameterized by the mapping module M implementing Mappings_intf.S. In this mode, the solver delays all interactions with the underlying SMT solver until necessary.
module Cached (_ : Mappings_intf.S) : sig ... endIn the Incremental module, constraints are managed incrementally, meaning that every interaction with the solver prompts a corresponding interaction with the underlying SMT solver. Unlike the batch solver, nearly every interaction with this solver involves the underlying SMT solver.
module Incremental (_ : Mappings_intf.S) : SThe Incremental module, like Batch, presents a solver parameterized by the mapping module M. In this mode, the Incremental solver engages with the underlying SMT solver in nearly every interaction.