package encoding

You can search for identifiers within the package.

in-package search v0.2.0

package encoding

Encoding
- Library encoding
  - Encoding
    
    Ast
    
    Eval_numeric
    
    Expr
    
    Pp
    
    Infix
    
    Bitv
    
    Interpret
    
    Make
    
    Interpret_intf
    
    S
    
    Lexer
    
    Log
    
    Mappings_intf
    
    S
    
    Solver
    
    Optimizer
    
    Model
    
    Num
    
    Op_intf
    
    S
    
    Optimizer
    
    Z3
    
    Params
    
    Parse
    
    Parser
    
    Solver
    
    Batch
    
    Z3_batch
    
    Incremental
    
    Z3_incremental
    
    Solver_intf
    
    S
    
    Symbol
    
    Ty
    
    Value
    
    Z3_mappings
    
    Fresh
    
    Make
    
    Solver
    
    Optimizer
    
    Solver
    
    Optimizer
- Sources
  - encoding
    
    ast.ml
    
    encoding.ml
    
    eval_numeric.ml
    
    expr.ml
    
    interpret.ml
    
    interpret_intf.ml
    
    log.ml
    
    mappings_intf.ml
    
    model.ml
    
    num.ml
    
    op_intf.ml
    
    optimizer.ml
    
    params.ml
    
    parse.ml
    
    solver.ml
    
    solver_intf.ml
    
    symbol.ml
    
    ty.ml
    
    value.ml
    
    z3_mappings.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Encoding`Source

Sourcemodule Ast : sig ... end

Sourcemodule Eval_numeric : sig ... end

Sourcemodule Expr : sig ... end

Sourcemodule Interpret : sig ... end

Sourcemodule Interpret_intf : sig ... end

module Lexer : sig ... end

Sourcemodule Log : sig ... end

Sourcemodule Mappings_intf : sig ... end

Sourcemodule Model : sig ... end

Sourcemodule Num : sig ... end

Sourcemodule Op_intf : sig ... end

Sourcemodule Optimizer : sig ... end

Sourcemodule Params : sig ... end

Sourcemodule Parse : sig ... end

module Parser : sig ... end

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

Sourcemodule Solver_intf : sig ... end

Sourcemodule Symbol : sig ... end

Sourcemodule Ty : sig ... end

Sourcemodule Value : sig ... end

Sourcemodule Z3_mappings : sig ... end

package encoding

Module EncodingSource

Module `Encoding`Source