package smtml

  1. Overview
  2. Docs
An SMT solver frontend for OCaml

Install 

dune-project
 Dependency

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

Authors

  1. J
    João Pereira <joaomhmpereira@tecnico.ulisboa.pt>
  2. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>
  3. H
    Hichem Rami Ait El Hara <hra@ocamlpro.com>
  4. R
    redianthus <redopam@pm.me>
  5. A
    Arthur Carcano <arthur.carcano@ocamlpro.com>
  6. P
    Pierre Chambart <pierre.chambart@ocamlpro.com>
  7. J
    José Fragoso Santos <jose.fragoso@tecnico.ulisboa.pt>

Maintainers

  1. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>

Sources

v0.16.0.tar.gz
md5=9e0021451109a86f7ebdbc5064220c8f
sha512=9bf3ab3757a0a5d5c355950de5ea5faed3d85194bcaaef18819e1a3e74f04d75baccb86327de5bf044e9e2a031bb261e6f206372fa47b31917e0137b3490458a

doc/src/smtml/symbol.ml.html

Source file symbol.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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2024 formalsec *)
(* Written by the Smtml programmers *)

type name =
  | Simple of string
  | Indexed of
      { basename : string
      ; indices : string list
      }

type namespace =
  | Attr
  | Sort
  | Term
  | Var

type t =
  { ty : Ty.t
  ; name : name
  ; namespace : namespace
  }

let attr = Attr

let sort = Sort

let term = Term

let var = Var

module Name = struct
  let simple name = Simple name

  let indexed basename indices = Indexed { basename; indices }
end

let ( @: ) (name : string) (ty : Ty.t) : t =
  { name = Name.simple name; namespace = term; ty }

let name { name; _ } = name

let namespace { namespace; _ } = namespace

let discr_namespace = function Attr -> 0 | Sort -> 1 | Term -> 2 | Var -> 3

let compare_namespace a b = compare (discr_namespace a) (discr_namespace b)

let compare_name a b =
  match (a, b) with
  | Simple a, Simple b -> String.compare a b
  | ( Indexed { basename = base1; indices = indices1 }
    , Indexed { basename = base2; indices = indices2 } ) ->
    let compare_base = String.compare base1 base2 in
    if compare_base = 0 then List.compare String.compare indices1 indices2
    else compare_base
  | Simple _, _ -> -1
  | Indexed _, _ -> 1

let compare a b =
  let compare_name = compare_name a.name b.name in
  if compare_name = 0 then
    let compare_ty = Ty.compare a.ty b.ty in
    if compare_ty = 0 then compare_namespace a.namespace b.namespace
    else compare_ty
  else compare_name

let equal a b = phys_equal a b || compare a b = 0

let make ty name = name @: ty

let make3 ty name namespace = { ty; name; namespace }

let mk namespace name = { ty = Ty_none; name = Name.simple name; namespace }

let indexed namespace basename indices =
  { ty = Ty_none; name = Name.indexed basename indices; namespace }

let pp_namespace fmt = function
  | Attr -> Fmt.string fmt "attr"
  | Sort -> Fmt.string fmt "sort"
  | Term -> Fmt.string fmt "term"
  | Var -> Fmt.string fmt "var"

let pp_name fmt = function
  | Simple name -> Fmt.string fmt name
  | Indexed { basename; indices } ->
    Fmt.pf fmt "(%s %a)" basename (Fmt.list ~sep:Fmt.sp Fmt.string) indices

let pp fmt { name; _ } = pp_name fmt name

let to_string { name; _ } = Fmt.str "%a" pp_name name

let to_json { name; ty; _ } =
  `Assoc
    [ ( Fmt.str "%a" pp_name name
      , `Assoc [ ("ty", `String (Fmt.str "%a" Ty.pp ty)) ] )
    ]

let type_of { ty; _ } = ty

module Map = Map.Make (struct
  type nonrec t = t

  let compare = compare
end)

module Smtlib = struct
  let pp fmt { ty; name; namespace } =
    match namespace with
    | Term -> pp_name fmt name
    | Sort -> Ty.Smtlib.pp fmt ty
    | Var -> assert false
    | Attr -> assert false
end