package soteria

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

Parameter Mutable_to_effectful.M

This module represents a solver state, it is fully imperative!

include Soteria.Soteria_std.Reversible.Mutable
type t
val init : unit -> t

Create a new reversible state initialized with the default value.

val backtrack_n : t -> int -> unit

Remove the last n checkpoints from state.

val save : t -> unit

Save the current state as a new checkpoint.

val reset : t -> unit

Clear all checkpoints and reset to the default value.

type sbool_v := Value.sbool Value.t
val add_constraints : t -> ?simplified:bool -> sbool_v list -> unit

Adds constraints to the solver state. The simplified flag indicates if simplify was already applied to the constraints, and is false by default. When it is false, the solver may simplify constraints before adding them to the state, depending on its implementation.

Returns the satisfiability of the current state.

val simplify : t -> 'a Value.t -> 'a Value.t

Attempts to simplify the given value according to the current solver state.

val fresh_var : t -> 'a Value.ty -> Symex.Var.t

Creates a fresh variable of the given type.

val as_exprs : t -> Value.Expr.t list

Converts the current solver state into the list of constraints it contains. These are syntactic constraints, not semantic ones.

val pp : Format.formatter -> t -> unit