package alt-ergo-lib

  1. Overview
  2. Docs

Module AltErgoLib.D_state_option

The Dolmen state option manager. Each module defined below is linked to an option that can be set, fetched et reset independently from the Options module, which is used as a static reference.

module type Accessor = sig ... end
module type S = sig ... end
module Mode : S with type t = Util.mode

The current mode of the solver.

Options are divided in two categories: 1. options that can be updated anytime; 2. options that can only be updated during start mode.

1. Options that can be updated anytime.

module StrictMode : S with type t = bool

Option for enabling/disabling strict mode engine.

2. Options that can only be updated during start mode.

module ProduceAssignment : S with type t = bool

Option for enabling/disabling the get-assignment instruction.

module SatSolver : S with type t = Util.sat_solver

The Sat solver used. When set, updates the SatSolverModule defined below.

module SatSolverModule : Accessor with type t = (module Sat_solver_sig.S)

The Sat solver module used for the calculation. This option's value depends on SatSolver: when SatSolver is updated, this one also is.

module Steps : S with type t = int

Option for setting the max number of steps. Interfaces with the toplevel Steps module. The set function may raise Invalid_arg from the Steps.set_steps_bound call if the new option value is lower than the current number of steps.

Initializes the state with options that requires some preprocessing.