package msat

  1. Overview
  2. Docs
On This Page
  1. Backtrackable ref
Library containing a SAT solver that can be parametrized by a theory

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (16)

Authors

  1. S
    Simon Cruanes
  2. G
    Guillaume Bury

Maintainers

  1. G
    guillaume.bury@gmail.com
  2. S
    simon.cruanes.2007@m4x.org

Sources

v0.9.1.tar.gz
md5=ba623630b0b8e0edc016079dd214c80b
sha512=51c133cefe8550125e7b1db18549e893bac15663fdd7a9fac87235c07de755f39eab9fc3cfdf6571612fd79b3d5b22f49f459581b480c7349bacddf2618c8a99

doc/msat.backtrack/Msat_backtrack/Ref/index.html

Module Msat_backtrack.Ref

Backtrackable ref

type 'a t
val create : ?copy:('a -> 'a) -> 'a -> 'a t

Create a backtrackable reference holding the given value initially.

  • parameter copy

    if provided, will be used to copy the value when push_level is called.

val set : 'a t -> 'a -> unit

Set the reference's current content

val get : 'a t -> 'a

Get the reference's current content

val update : 'a t -> ('a -> 'a) -> unit

Update the reference's current content

val push_level : _ t -> unit

Push a backtracking level, copying the current value on top of some stack. The copy function will be used if it was provided in create.

val n_levels : _ t -> int

Number of saved values

val pop_levels : _ t -> int -> unit

Pop n levels, restoring to the value the reference was storing n calls to push_level earlier.