package universo

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module Spec : L.LRA_SPECIFICATION

type t = Z3.Expr.expr

type smt_model = Z3.Model.model

type ctx = Z3.context

val logic : [> `Lra ]

val mk_name : B.name -> string

val int_sort : Z3.context -> Z3.Sort.sort

val mk_var : ctx -> string -> t

val to_int : ctx -> int -> t

val mk_univ : ctx -> U.univ -> t

val mk_max : ctx -> t -> t -> t

val mk_imax : ctx -> t -> t -> t

val mk : (ctx, t) L.k

val mk_axiom : ctx -> t -> t -> t

val mk_rule : ctx -> t -> t -> t -> t

val mk_cumul : ctx -> t -> t -> t

val mk_bounds : ctx -> string -> int -> Z3.Expr.expr

val solution_of_var : ctx -> int -> Z3.Model.model -> string -> U.univ

val mk_theory : bool