package smtml

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

Install 

dune-project
 Dependency

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

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.22.0.tar.gz
md5=2ec822c82786736b275c31e850f7d292
sha512=335a1595b0652ca0d5aa50177e47a66467935d586433ad26329d6fa7d9ff6fd3eda51d630c2002278eb6565e8de83e0750b000c0a0f5b453b7ed11ffca3519a2

doc/smtml/Smtml/Typed/Real/index.html

Module Typed.RealSource

Sourcetype t = real expr
Sourceval v : float -> t
Sourceval symbol : Symbol.t -> t
Sourceval neg : t -> t

neg t constructs the negation of the real number term t.

Sourceval add : t -> t -> t

add t1 t2 constructs the sum of the real number terms t1 and t2.

Sourceval sub : t -> t -> t

sub t1 t2 constructs the difference of the real number terms t1 and t2.

Sourceval mul : t -> t -> t

mul t1 t2 constructs the product of the real number terms t1 and t2.

Sourceval div : t -> t -> t

div t1 t2 constructs the quotient of the real number terms t1 and t2.

Sourceval pow : t -> t -> t

pow t1 t2 constructs the power of the real number terms t1 and t2.

Sourceval eq : t -> t -> bool expr

Alias for Bool.eq.

Sourceval lt : t -> t -> bool expr

lt t1 t2 constructs the less-than relation between t1 and t2.

Sourceval le : t -> t -> bool expr

le t1 t2 constructs the less-than-or-equal relation between t1 and t2.

Sourceval to_int : t -> int expr

to_int t converts the real number term t to an integer term.

Sourceval pp : t Fmt.t