package smtml

You can search for identifiers within the package.

in-package search v0.2.0

An SMT solver frontend for OCaml

Install

dune-project

Dependency

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

Authors

Maintainers

F

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

Sources

v0.22.0.tar.gz

md5=2ec822c82786736b275c31e850f7d292

sha512=335a1595b0652ca0d5aa50177e47a66467935d586433ad26329d6fa7d9ff6fd3eda51d630c2002278eb6565e8de83e0750b000c0a0f5b453b7ed11ffca3519a2

doc/smtml/Smtml/Typed/index.html

Module `Smtml.Typed`Source

Sourcetype 'a ty = private Ty.t

The type of a type witness.

Sourcetype 'a expr = private Expr.t

The type of a typed expression (term).

Sourcetype real

Sourcetype regexp

Sourcetype bitv8

Sourcetype bitv16

Sourcetype bitv32

Sourcetype bitv64

Sourcetype bitv128

Sourcetype float32

Sourcetype float64

Sourcemodule Unsafe : sig ... end

Sourceval view : 'a expr -> Expr.expr

view e typed alias for Expr.view. Allows retrieving the underlying structure of the expression e.

Sourceval simplify : 'a expr -> 'a expr

simplify e typed alias for Expr.simplify. Performs algebraic simplifications on the expression e.

Sourceval symbol : 'a ty -> string -> 'a expr

symbol ty name creates a symbolic constant of type ty with the given name.

Sourceval get_symbols : 'a expr list -> Symbol.t list

get_symbols es returns a list of all unique symbols appearing in the list of expressions es.

Sourceval ptr : int32 -> bitv32 expr -> bitv32 expr

ptr value base creates a 32-bit pointer expression by adding value to the base address.

Sourcemodule Types : sig ... end

Sourcemodule Bool : sig ... end

Sourcemodule Int : sig ... end

Sourcemodule Real : sig ... end

Sourcemodule String : sig ... end

Sourcemodule Bitv : sig ... end

Sourcemodule Bitv8 : Bitv.S with type w = bitv8

Sourcemodule Bitv16 : Bitv.S with type w = bitv16

Sourcemodule Bitv32 : sig ... end

Sourcemodule Bitv64 : sig ... end

Sourcemodule Bitv128 : sig ... end

Sourcemodule Float32 : sig ... end

Sourcemodule Float64 : sig ... end

Sourcemodule Func : sig ... end

Typed function builders for SMT usage.