package msat
Library containing a SAT solver that can be parametrized by a theory
Install
Dune Dependency
Authors
Maintainers
Sources
v0.9.1.tar.gz
md5=ba623630b0b8e0edc016079dd214c80b
sha512=51c133cefe8550125e7b1db18549e893bac15663fdd7a9fac87235c07de755f39eab9fc3cfdf6571612fd79b3d5b22f49f459581b480c7349bacddf2618c8a99
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; ()
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>