package mc2
A mcsat-based SMT solver in pure OCaml
Install
Dune Dependency
Authors
Maintainers
Sources
v0.1.tar.gz
md5=92de696251ec76fbf3eba6ee917fd80f
sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0
doc/src/mc2.core/Value.ml.html
Source file Value.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 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
(** {1 Values} *) open Solver_types module Fmt = CCFormat type t = value type view = value_view let[@inline] is_bool = function V_true | V_false -> true | V_value _ -> false let[@inline] is_true = function V_true -> true | _ -> false let[@inline] is_false = function V_false -> true | _ -> false let[@inline] as_bool = function V_true -> Some true | V_false -> Some false | _ -> None let[@inline] as_bool_exn = function V_true -> true | V_false -> false | _ -> assert false let[@inline] view v = match v with | V_true | V_false -> assert false | V_value{view;_} -> view let[@inline] tc v = match v with | V_true | V_false -> assert false | V_value{tc;_} -> tc let[@inline] equal v1 v2 = match v1, v2 with | V_true, V_true | V_false, V_false -> true | V_value {tc=tc1;view=v1}, V_value{view=v2;_} -> tc1.tcv_equal v1 v2 | V_true, _ | V_false, _ | V_value _, _ -> false let[@inline] hash v = match v with | V_true -> 10 | V_false -> 20 | V_value{view;tc} -> tc.tcv_hash view let[@inline] pp out v = match v with | V_true -> Fmt.string out "true" | V_false -> Fmt.string out "false" | V_value {view;tc} -> tc.tcv_pp out view let true_ = V_true let false_ = V_false let[@inline] of_bool b = if b then true_ else false_ let[@inline] make tc view : t = V_value { tc; view } let[@inline] bool_neg = function | V_true -> false_ | V_false -> true_ | v -> v module As_key = struct type t = value let equal = equal let hash = hash end module Tbl = CCHashtbl.Make(As_key) module TC = struct type t = tc_value let make ~pp ~equal ~hash () : t = {tcv_pp=pp; tcv_equal=equal; tcv_hash=hash} end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>