package encoding

  1. Overview
  2. Docs

The 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.

Batch Mode

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.

Batch 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.

Z3_batch is a concrete instantiation of Batch with Z3_mappings, providing a solver specifically tailored for the Z3 SMT solver.

Incremental Model

In 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.

The 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_incremental is a specific instantiation of Incremental with Z3_mappings, creating an incremental solver designed for the Z3 SMT solver.

OCaml

Innovation. Community. Security.