package smtml

  1. Overview
  2. Docs
package smtml
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Z3_mappings.MappingsSource

Make () creates a new instance of the M module type.

Sourceval is_available : bool

is_available indicates whether the module is available for use.

Will be deprecated in the future, please use Internals.is_available instead.

Include the M module type.

include Mappings_intf.M
Sourcetype ty

The type of SMT sorts (types).

Sourcetype term

The type of SMT terms.

Sourcetype interp

The type of interpretations (evaluated values).

Sourcetype model

The type of SMT models.

Sourcetype solver

The type of SMT solvers.

Sourcetype handle

The type of optimization handles.

Sourcetype optimizer

The type of SMT optimizers.

Sourcetype func_decl

The type of function declarations.

Sourceval true_ : term

true_ represents the Boolean constant true.

Sourceval false_ : term

false_ represents the Boolean constant false.

Sourceval int : int -> term

int n constructs an integer term from the given integer n.

Sourceval real : float -> term

real f constructs a real number term from the given float f.

Sourceval const : string -> ty -> term

const name ty constructs a constant term with the given name and type.

Sourceval not_ : term -> term

not_ t constructs the logical negation of the term t.

Sourceval and_ : term -> term -> term

and_ t1 t2 constructs the logical AND of the terms t1 and t2.

Sourceval or_ : term -> term -> term

or_ t1 t2 constructs the logical OR of the terms t1 and t2.

Sourceval logand : term list -> term

logand ts constructs the logical AND of a list of terms ts.

Sourceval logor : term list -> term

logor ts constructs the logical OR of a list of terms ts.

Sourceval xor : term -> term -> term

xor t1 t2 constructs the logical XOR of the terms t1 and t2.

Sourceval implies : term -> term -> term

implies t1 t2 constructs the logical implication of the terms t1 and t2.

Sourceval eq : term -> term -> term

eq t1 t2 constructs the equality of the terms t1 and t2.

Sourceval distinct : term list -> term

distinct ts constructs the distinctness of a list of terms ts.

Sourceval ite : term -> term -> term -> term

ite cond then_ else_ constructs an if-then-else term.

Sourceval forall : term list -> term -> term

forall vars body constructs a universal quantification term.

Sourceval exists : term list -> term -> term

exists vars body constructs an existential quantification term.

Sourcemodule Internals : sig ... end

Type Handling

Sourcemodule Types : sig ... end

Interpretation Handling

Sourcemodule Interp : sig ... end

Integer Operations

Sourcemodule Int : sig ... end

Real Number Operations

Sourcemodule Real : sig ... end

String Operations

Sourcemodule String : sig ... end

Regular Expression Operations

Sourcemodule Re : sig ... end

Bitvector Operations

Sourcemodule Bitv : sig ... end

Floating-Point Operations

Sourcemodule Float : sig ... end

Function Handling

Sourcemodule Func : sig ... end

Algebraic Data Type Handling

Sourcemodule Adt : sig ... end

Model Handling

Sourcemodule Model : sig ... end

Solver Handling

Sourcemodule Solver : sig ... end

Optimizer Handling

Sourcemodule Optimizer : sig ... end

SMT-LIB Pretty Printing

Sourcemodule Smtlib : sig ... end