Module Smtml

module Altergo_mappings : sig ... end

Alt-Ergo Solver Mappings. This module defines types and utilities for mapping between internal representations and the format used by the Alt-Ergo solver. It provides functions to translate problems into solver-specific inputs and to interpret solver outputs.

module Ast : sig ... end
module Binder : sig ... end

Quantifiers and Binding Constructs. This module defines types and utilities for representing quantifiers (universal and existential) and let-bindings, which are commonly used in SMT-LIB formulas for logical quantification and local definitions.

module Bitvector : sig ... end
module Bitwuzla_mappings : sig ... end

Bitwuzla Solver Mappings. This module defines types and utilities for mapping between internal representations and the format used by the Bitwuzla solver. It provides functions to translate problems into solver-specific inputs and to interpret solver outputs.

module Cache : sig ... end
module Cache_intf : sig ... end
module Colibri2_mappings : sig ... end

Colibri2 Solver Mappings. This module defines types and utilities for mapping between internal representations and the format used by the Colibri2 solver. It provides functions to translate problems into solver-specific inputs and to interpret solver outputs.

module Compile : sig ... end

Compilation Module. This module provides functionality for parsing and processing abstract syntax trees (ASTs) from files, with support for transformations and rewrites.

module Cvc5_mappings : sig ... end

Cvc5 Solver Mappings. This module defines types and utilities for mapping between internal representations and the format used by the Cvc5 solver. It provides functions to translate problems into solver-specific inputs and to interpret solver outputs.

module Dolmenexpr_to_expr : sig ... end
module Eval : sig ... end

Operators and Evaluation Functions. This module defines types and functions for representing and evaluating various kinds of operations, including unary, binary, ternary, relational, conversion, and n-ary operations. It also defines exceptions for handling errors during evaluation.

module Expr : sig ... end

Abstract Syntax Tree (AST) for Expressions. This module defines the representation of terms and expressions in the AST, along with constructors, accessors, simplification utilities, and pretty-printing functions. It also includes submodules for handling Boolean expressions, sets, bitvectors, and floating-point arithmetic.

module Expr_intf : sig ... end
module Expr_raw : sig ... end
module Feature_extraction : sig ... end
module Interpret : sig ... end
module Interpret_intf : sig ... end
module Lexer : sig ... end
module Log : sig ... end
module Logic : sig ... end

SMT-LIB Logics. This module defines the set of SMT-LIB logics, which specify the theories and operations that a solver may handle. Each logic represents a combination of supported theories, such as arithmetic, arrays, bitvectors, and uninterpreted functions.

module Mappings : sig ... end
module Mappings_intf : sig ... end

Mappings Module. This module defines interfaces for interacting with SMT solvers, including term construction, type handling, solver interaction, and optimization. It provides a generic interface for working with different SMT solvers and their functionalities.

module Model : sig ... end

Model Module. This module defines a symbol table that maps symbols to values. It provides utility functions for iteration, retrieval, evaluation, serialization, and parsing from various formats.

module Num : sig ... end

Typed Values Representation. This module defines types and utilities for representing values with different numeric types, including integers and floating-point numbers. It also provides functions for type checking, comparison, formatting, and conversion.

module Op_intf : sig ... end
module Optimizer : sig ... end
module Optimizer_intf : sig ... end

Optimizer Module. This module defines interfaces for interacting with optimization solvers, including constraint management, optimization objectives, and result retrieval. It provides a generic interface for working with different optimization backends.

module Params : sig ... end

Parameter Management Module. This module defines a type-safe interface for handling solver parameters, allowing configuration of options such as timeouts, model production, and parallel execution.

module Parse : sig ... end

SMT Script Parsing Module. This module provides functionality for parsing Smt.ml and SMT-LIB scripts from files or strings. It supports both custom Smt.ml syntax and the standard SMT-LIB format.

module Parser : sig ... end
module Regression_model_default : sig ... end
module Rewrite : sig ... end

Module that performs two 'important' rewritings:

module Smtlib : sig ... end
module Smtzilla : sig ... end
module Solver : sig ... end
module Solver_dispatcher : sig ... end

Solver Query Module. This module provides functions for querying available solvers and obtaining mappings for specific solver types. It allows checking solver availability, listing available solvers, and retrieving solver mappings.

module Solver_intf : sig ... end

Solver Interface Module. This module defines interfaces for interacting with SMT solvers, including batch and incremental modes. It provides a generic interface for working with different SMT solvers and their functionalities.

module Solver_mode : sig ... end

Solver Mode Type. This module defines different solver modes and provides utilities for conversion, pretty-printing, and command-line argument handling.

module Solver_type : sig ... end

Solver Type Module. This module defines types and utilities for working with different SMT solvers, including parsing, pretty-printing, availability checks, and mapping retrieval.

module Statistics : sig ... end

Statistics Module. This module defines types and utilities for managing and manipulating solver statistics, including merging and pretty-printing.

module Symbol : sig ... end

Symbol Module. This module defines names, namespaces, and typed symbols, providing utilities for creating, comparing, and manipulating symbols.

module Ty : sig ... end

Type Module. This module defines types and operations for working with SMT types, including unary, binary, relational, ternary, conversion, and n-ary operations. It also provides utilities for type comparison, pretty-printing, and parsing.

module Typed : sig ... end
module Utils : sig ... end
module Value : sig ... end

Concrete Values Module. This module defines types and utilities for working with concrete values, including integers, floats, strings, lists, and applications. It provides functions for type checking, comparison, mapping, and conversion to/from strings and JSON.

module Z3_mappings : sig ... end

Z3 Solver Mappings. This module defines types and utilities for mapping between internal representations and the format used by the Z3 solver. It provides functions to translate problems into solver-specific inputs and to interpret solver outputs.