package msat

  1. Overview
  2. Docs
Library containing a SAT solver that can be parametrized by a theory

Install

dune-project
 Dependency

Authors

Maintainers

Sources

v0.8.2.tar.gz
md5=c02d63bf45357aa1d1b85846da373f48
sha512=e6f0d7f6e4fe69938ec2cc3233b0cb72dd577bfb4cc4824afe8247f5db0b6ffea2d38d73a65e7ede500d21ff8db27ed12f2c4f3245df4451d02864260ae2ddaf

doc/src/msat.backtrack/Backtrackable_ref.ml.html

Source file Backtrackable_ref.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

type 'a t = {
  mutable cur: 'a;
  stack: 'a Vec.t;
  copy: ('a -> 'a) option;
}

let create ?copy x: _ t =
  {cur=x; stack=Vec.create(); copy}

let[@inline] get self = self.cur
let[@inline] set self x = self.cur <- x
let[@inline] update self f = self.cur <- f self.cur

let[@inline] n_levels self = Vec.size self.stack

let[@inline] push_level self : unit =
  let x = self.cur in
  let x = match self.copy with None -> x | Some f -> f x in
  Vec.push self.stack x

let pop_levels self n : unit =
  assert (n>=0);
  if n > Vec.size self.stack then invalid_arg "Backtrackable_ref.pop_levels";
  let i = Vec.size self.stack-n in
  let x = Vec.get self.stack i in
  self.cur <- x;
  Vec.shrink self.stack i;
  ()
OCaml

Innovation. Community. Security.