type nonrec satisfiability = Solver_intf.satisfiabilitymodule type S = Solver_intf.SThe Encoding module defines two types of solvers: Batch and Incremental. The generic definition of these solvers is presented here, and they are parametric on the mappings of the underlying SMT solver. This design allows for the creation of portable solvers that can be used with various SMT solvers implementing Mappings_intf.S.
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 essentially 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) : SBatch 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 it becomes necessary.
module Cached (_ : Mappings_intf.S) : sig ... endIn the Incremental module, constraints are managed incrementally, signifying that upon their addition to the solver, this module promptly communicates with the underlying SMT solver. Unlike the batch solver, nearly every interaction with this solver prompts a corresponding interaction with the underlying SMT solver.
module Incremental (_ : Mappings_intf.S) : SThe Incremental module, akin to 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.
Z3_batch is a concrete instantiation of Batch with Z3_mappings, providing a solver specifically tailored for the Z3 SMT solver.
module Z3_incremental : SZ3_incremental is a specific instantiation of Incremental with Z3_mappings, creating an incremental solver designed for the Z3 SMT solver.