package smtml

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Name Types
Namespace Types
Symbol Types
Namespace Constants
Symbol Creation
Symbol Accessors
Comparison
Pretty Printing
Serialization

An SMT solver frontend for OCaml

Install

dune-project

Dependency

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

Authors

Maintainers

F

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

Sources

v0.16.0.tar.gz

md5=9e0021451109a86f7ebdbc5064220c8f

sha512=9bf3ab3757a0a5d5c355950de5ea5faed3d85194bcaaef18819e1a3e74f04d75baccb86327de5bf044e9e2a031bb261e6f206372fa47b31917e0137b3490458a

doc/smtml/Smtml/Symbol/index.html

Module `Smtml.Symbol`Source

Symbol Module. This module defines names, namespaces, and typed symbols, providing utilities for creating, comparing, and manipulating symbols.

Name Types

Sourcetype name =

| Simple of string
(*
A simple name represented as a string.
*)
| Indexed of {
1. basename : string;
  (*
  The base name.
  *)
2. indices : string list;
  (*
  A list of indices associated with the name.
  *)
}

The type name represents a symbol name, which can either be a simple string or an indexed name with a base name and a list of indices.

Namespace Types

Sourcetype namespace =

| Attr
(*
Attributes.
*)
| Sort
(*
Sorts (types).
*)
| Term
(*
Terms (functions, constants).
*)
| Var
(*
Variables.
*)

The type namespace classifies symbols into different kinds of identifiers.

Symbol Types

Sourcetype t = {

ty : Ty.t;
(*
The type of the symbol.
*)
name : name;
(*
The name of the symbol.
*)
namespace : namespace;
(*
The namespace to which the symbol belongs.
*)

}

The type t represents a symbol, consisting of a type, a name, and a namespace.

Namespace Constants

Sourceval attr : namespace

attr represents the attribute namespace.

Sourceval sort : namespace

sort represents the sort (type) namespace.

Sourceval term : namespace

term represents the term (function, constant) namespace.

Sourceval var : namespace

var represents the variable namespace.

Symbol Creation

Sourceval (@:) : string -> Ty.t -> t

s @: ty creates a symbol with name s and type ty, belonging to the term (function, constant) namespace.

Sourceval make : Ty.t -> string -> t

make ty s creates a symbol with type ty and name s in the term (function, constant) namespace.

Sourceval make3 : Ty.t -> name -> namespace -> t

make3 ty name ns creates a symbol with type ty, name name, and namespace ns.

Sourceval mk : namespace -> string -> t

mk ns s creates a symbol with name s in the specified namespace ns with a default type.

Sourceval indexed : namespace -> string -> string list -> t

indexed ns basename indices creates a symbol with an indexed name, where basename is the base name and indices are the associated indices.

Symbol Accessors

Sourceval name : t -> name

name sym returns the name of the symbol sym.

Sourceval namespace : t -> namespace

namespace sym returns the namespace of the symbol sym.

Sourceval type_of : t -> Ty.t

type_of sym returns the type of the symbol sym.

Comparison

Sourceval compare : t -> t -> int

compare sym1 sym2 performs a total order comparison of sym1 and sym2.

Sourceval equal : t -> t -> Smtml_prelude.Bool.t

equal sym1 sym2 checks if sym1 and sym2 are equal.

Pretty Printing

Sourceval pp_namespace : namespace Fmt.t

pp_namespace fmt ns pretty-prints the namespace ns using the formatter fmt.

Sourceval pp : t Fmt.t

pp fmt sym pretty-prints the symbol sym using the formatter fmt.

Serialization

Sourceval to_string : t -> string

to_string sym converts the symbol sym to a string representation.

Sourceval to_json : t -> Yojson.Basic.t

to_json sym converts the symbol sym to a JSON representation.

module Map : Smtml_prelude.Map.S with type key = t

Sourcemodule Smtlib : sig ... end