package smtml

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

Install 

dune-project
 Dependency

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

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.28.0.tar.gz
md5=dccec4e664735d96f7d5e867f8c0841f
sha512=4e1586451c0e61dcae6bd46bb8fe899430b383c776dbf214cffcd6802449ee522f4658e2990ac1a1ad6f8e89f72a8d83ba0a40a7d33b2faaa9f8ae0c7a1d0c67

doc/smtml/Smtml/Statistics/index.html

Module Smtml.StatisticsSource

Statistics Module. This module defines types and utilities for managing and manipulating solver statistics, including merging and pretty-printing.

Entry Types

Sourcetype entry = [
  1. | `Int of int
    (*

    An integer statistic entry.

    *)
  2. | `Float of float
    (*

    A floating-point statistic entry.

    *)
]

The type entry represents a single statistic entry, which can be either an integer or a floating-point number.

Statistics Map

Sourcemodule Map : Smtml_prelude.Map.S with type key = string

Map is a module for managing statistics as a map from string keys to statistic entries.

The type t represents a collection of statistics as a map from string keys to statistic entries.

Merging and Aggregation

Sourceval sum_entries : entry -> entry -> entry

sum_entries e1 e2 sums two statistic entries e1 and e2. If both entries are integers, the result is an integer. If either entry is a float, the result is a float.

Sourceval merge : t -> t -> t

merge t1 t2 merges two statistics maps t1 and t2. If a key exists in both maps, the corresponding entries are summed using sum_entries.

Pretty Printing

Sourceval pp_entry : entry Fmt.t

pp_entry fmt entry pretty-prints a single statistic entry entry using the formatter fmt.

Sourceval pp : t Fmt.t

pp fmt stats pretty-prints the statistics map stats using the formatter fmt.

Sourceval to_json : t -> Yojson.Safe.t

to_json stats converts the statistics map stats into a JSON representation.