package smtml

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.

SMT-LIB Commands Representation. This module defines types and utilities for representing SMT-LIB commands, which are used to interact with SMT solvers. It includes commands for assertions, declarations, solver control, and metadata management.

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.

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.

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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 that performs two 'important' rewritings:

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.

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.

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

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

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

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

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.

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.

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.