package alt-ergo-lib

  1. Overview
  2. Docs
The Alt-Ergo SMT prover library

Install

Dune Dependency

Authors

Maintainers

Sources

alt-ergo-2.3.1.tar.gz
sha256=0fd6594f30d4e2bea97350a7906ecc2528c37e8fdd32588818a162aacc409688
md5=a0e9dda8f17c1f4f03119badd24d1bf5

doc/src/alt-ergo-lib/var.ml.html

Source file var.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
(******************************************************************************)
(*                                                                            *)
(*     Alt-Ergo: The SMT Solver For Software Verification                     *)
(*     Copyright (C) 2013-2018 --- OCamlPro SAS                               *)
(*                                                                            *)
(*     This file is distributed under the terms of the license indicated      *)
(*     in the file 'License.OCamlPro'. If 'License.OCamlPro' is not           *)
(*     present, please contact us to clarify licensing.                       *)
(*                                                                            *)
(******************************************************************************)

open Options
open Format

type view = {
  hs : Hstring.t ;
  id : int ;
}

type t = view

let cpt = ref 0

let of_hstring hs =
  incr cpt;
  {hs ; id = !cpt}

let of_string s =
  incr cpt;
  {hs = Hstring.make s; id = !cpt}

let view v = v

let compare a b =
  let c = a.id - b.id in
  if c <> 0 then c
  else begin
    assert (Hstring.equal a.hs b.hs);
    c
  end

let equal a b = compare a b = 0

let hash { id; _ } = id

let to_string {hs ; id} =
  sprintf "%s~%d" (Hstring.view hs) id

let print fmt v =
  fprintf fmt "%s" (to_string v)

module Set = Set.Make(struct type t = view let compare = compare end)
module Map = Map.Make(struct type t = view let compare = compare end)
OCaml

Innovation. Community. Security.