package encoding

You can search for identifiers within the package.

in-package search v0.2.0

package encoding

encoding
- Encoding
  - Ast
  - Constructors_intf
    
    Bitv
  - Eval_numeric
  - Expr
    
    Bitv
    
    I32
    
    I64
    
    I8
  - Interpret
    
    Make
    
    Solver
  - Interpret_intf
    
    S
  - Lexer
  - Log
  - Mappings_intf
    
    S
    
    Optimizer
    
    Solver
  - Model
  - Num
  - Op_intf
    
    S
  - Optimizer
    
    Z3
  - Params
  - Parse
  - Parser
  - Solver
    
    Batch
    
    M
    
    Optimizer
    
    Solver
    
    Incremental
    
    M
    
    Optimizer
    
    Solver
    
    Z3_batch
    
    Z3_incremental
  - Solver_intf
    
    S
  - Symbol
  - Ty
  - Value
  - Z3_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Solver
    
    Optimizer
    
    Solver

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Ast : sig ... end

module Constructors_intf : sig ... end

module Eval_numeric : sig ... end

module Expr : sig ... end

Term definitions of the abstract syntax

module Interpret : sig ... end

module Interpret_intf : sig ... end

module Lexer : sig ... end

module Log : sig ... end

module Mappings_intf : sig ... end

module Model : sig ... end

module Num : sig ... end

module Op_intf : sig ... end

module Optimizer : sig ... end

module Params : sig ... end

module Parse : sig ... end

module Parser : sig ... end

module Solver : sig ... end

The Encoding module defines two types of solvers: Batch and Incremental. The generic definition of these solvers is presented here, and they are parametric on the mappings of the underlying SMT solver. This design allows for the creation of portable solvers that can be used with various SMT solvers implementing Mappings_intf.S.

module Solver_intf : sig ... end

module Symbol : sig ... end

module Ty : sig ... end

module Value : sig ... end

module Z3_mappings : sig ... end