package soteria

  1. Overview
  2. Docs
package soteria
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Solver.Mutable_to_effectful

Converts a mutable incremental solver into an effectful one. See the documentation of Soteria_std.Reversible.Mutable_to_effectful for more details.

Parameters

Signature

include sig ... end
type t = M.t
val backtrack_n : int -> unit
val save : unit -> unit
val wrap : (t -> 'a) -> unit -> 'a
val run : (unit -> 'a) -> 'a
module Value = M.Value
val add_constraints : ?simplified:??? -> M.Value.sbool M.Value.t list -> unit
val sat : unit -> Symex.Solver_result.t
val simplify : 'a M.Value.t -> 'a M.Value.t
val fresh_var : 'a M.Value.ty -> Symex.Var.t
val as_exprs : unit -> M.Value.Expr.t list