Module M.Make

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

Parameters

Signature

type ty

The type of SMT sorts (types).

type term

The type of SMT terms.

type interp

The type of interpretations (evaluated values).

type model

The type of SMT models.

type solver

The type of SMT solvers.

type handle

The type of optimization handles.

type optimizer

The type of SMT optimizers.

type func_decl

The type of function declarations.

val true_ : term

true_ represents the Boolean constant true.

val false_ : term

false_ represents the Boolean constant false.

val int : int -> term

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

val real : float -> term

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

val const : string -> ty -> term

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

val not_ : term -> term

not_ t constructs the logical negation of the term t.

val and_ : term -> term -> term

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

val or_ : term -> term -> term

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

val logand : term list -> term

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

val logor : term list -> term

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

val xor : term -> term -> term

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

val implies : term -> term -> term

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

val eq : term -> term -> term

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

val distinct : term list -> term

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

val ite : term -> term -> term -> term

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

val forall : term list -> term -> term

forall vars body constructs a universal quantification term.

val exists : term list -> term -> term

exists vars body constructs an existential quantification term.

module Internals : sig ... end

Type Handling

module Types : sig ... end

Interpretation Handling

module Interp : sig ... end

Integer Operations

module Int : sig ... end

Real Number Operations

module Real : sig ... end

String Operations

module String : sig ... end

Regular Expression Operations

module Re : sig ... end

Bitvector Operations

module Bitv : sig ... end

Floating-Point Operations

module Float : sig ... end

Function Handling

module Func : sig ... end

Algebraic Data Type Handling

module Adt : sig ... end

Model Handling

module Model : sig ... end

Solver Handling

module Solver : sig ... end

Optimizer Handling

module Optimizer : sig ... end

SMT-LIB Pretty Printing

module Smtlib : sig ... end