package smtml

You can search for identifiers within the package.

in-package search v0.2.0

package smtml

smtml
- Smtml
  - Altergo_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
  - Ast
  - Binder
  - Bitwuzla_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
  - Cache
    
    Strong
  - Cache_intf
    
    Intf
    
    Strong
    
    S
  - Colibri2_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
  - Compile
  - Constructors_intf
    
    Infix
  - Cvc5_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
  - Dolmenexpr_to_expr
    
    Builtin
    
    SHT
  - Eval
  - Expr
    
    Bitv
    
    I32
    
    I64
    
    I8
    
    Bool
    
    Fpa
    
    F32
    
    F64
    
    Hc
    
    Set
    
    BaseMap
    
    WithForeign
    
    Map2
  - Interpret
    
    Make
    
    Solver
  - Interpret_intf
    
    Intf
    
    Make
    
    Solver
    
    S
  - Lexer
  - Log
  - Logic
  - Mappings
    
    Make
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    M_with_make
    
    Bitv
    
    Float
    
    Rounding_mode
    
    Func
    
    Int
    
    Interp
    
    Make
    
    Bitv
    
    Float
    
    Rounding_mode
    
    Func
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Re
    
    Real
    
    Smtlib
    
    Solver
    
    String
    
    Types
    
    Model
    
    Optimizer
    
    Re
    
    Real
    
    Smtlib
    
    Solver
    
    String
    
    Types
    
    Optimizer
    
    Smtlib
    
    Solver
  - Mappings_intf
    
    M
    
    Bitv
    
    Float
    
    Rounding_mode
    
    Func
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Re
    
    Real
    
    Smtlib
    
    Solver
    
    String
    
    Types
    
    M_with_make
    
    Bitv
    
    Float
    
    Rounding_mode
    
    Func
    
    Int
    
    Interp
    
    Make
    
    Bitv
    
    Float
    
    Rounding_mode
    
    Func
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Re
    
    Real
    
    Smtlib
    
    Solver
    
    String
    
    Types
    
    Model
    
    Optimizer
    
    Re
    
    Real
    
    Smtlib
    
    Solver
    
    String
    
    Types
    
    S
    
    Optimizer
    
    Smtlib
    
    Solver
    
    S_with_fresh
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
  - Model
    
    Parse
    
    Json
    
    Scfg
    
    Smtlib
  - Num
  - Op_intf
    
    S
  - Optimizer
    
    Make
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Z3
  - Optimizer_intf
    
    Intf
    
    Make
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Z3
    
    S
  - Params
  - Parse
    
    Smtlib
    
    Smtml
  - Parser
    
    Incremental
    
    MenhirInterpreter
  - Rewrite
    
    Symb_map
  - Smtlib
    
    Extension
    
    Lexer
    
    Parser
    
    Statement
    
    Term
  - Solver
    
    Batch
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Cached
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Incremental
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
  - Solver_dispatcher
  - Solver_intf
    
    Intf
    
    Batch
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Cached
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Incremental
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    S
  - Solver_mode
  - Solver_type
  - Statistics
    
    Map
  - Symbol
  - Ty
    
    Binop
    
    Cvtop
    
    Naryop
    
    Relop
    
    Triop
    
    Unop
  - Utils
  - Value
  - Z3_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
smtml.prelude
- Smtml_prelude
  - Option
  - Result

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Make () : Mappings_intf.M

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

val is_available : bool

is_available indicates whether the module is available for use.

Include the M module type.

include Mappings_intf.M

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 caches_consts : bool

caches_consts indicates whether the solver caches constants.

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 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.

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

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