package smtml

You can search for identifiers within the package.

in-package search v0.2.0

smtml
- Smtml
  - Ast
  - Cache
    
    Strong
  - Cache_intf
    
    Intf
    
    Strong
    
    S
  - Constructors_intf
    
    Infix
  - Eval
  - Expr
    
    Bitv
    
    I32
    
    I64
    
    I8
    
    Bool
    
    Fpa
    
    F32
    
    F64
    
    Hc
  - Interpret
    
    Make
    
    Solver
  - Interpret_intf
    
    Intf
    
    Make
    
    Solver
    
    S
  - Lexer
  - Log
  - Mappings
    
    Make
    
    Bitv_impl
    
    B
    
    Ixx
    
    Bitv_sig
    
    Ixx
    
    Bool_impl
    
    Float32_impl
    
    Float64_impl
    
    Float_impl
    
    F
    
    Float_sig
    
    I32
    
    Ixx
    
    I64
    
    Ixx
    
    I8
    
    Ixx
    
    Int_impl
    
    M
    
    Bitv
    
    Cont
    
    Float
    
    Rounding_mode
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Real
    
    Solver
    
    String
    
    Types
    
    Optimizer
    
    Real_impl
    
    Solver
    
    String_impl
    
    Make'
    
    M
    
    Bitv
    
    Cont
    
    Float
    
    Rounding_mode
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Real
    
    Solver
    
    String
    
    Types
    
    Optimizer
    
    Solver
  - Mappings_intf
    
    M
    
    Bitv
    
    Cont
    
    Float
    
    Rounding_mode
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Real
    
    Solver
    
    String
    
    Types
    
    S
    
    Optimizer
    
    Solver
  - Model
  - Num
  - Op_intf
    
    S
  - Optimizer
    
    Z3
  - Params
  - Parse
  - Parser
  - Solver
    
    Batch
    
    M
    
    Optimizer
    
    Solver
    
    Cached
    
    Cache
    
    M
    
    Optimizer
    
    Solver
    
    Incremental
    
    M
    
    Optimizer
    
    Solver
    
    Z3_batch
    
    Z3_incremental
  - Solver_intf
    
    Intf
    
    Batch
    
    M
    
    Optimizer
    
    Solver
    
    Cached
    
    Cache
    
    M
    
    Optimizer
    
    Solver
    
    Incremental
    
    M
    
    Optimizer
    
    Solver
    
    Z3_batch
    
    Z3_incremental
    
    S
  - Symbol
  - Ty
  - Utils
  - Value
  - Z3_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Solver
    
    Optimizer
    
    Solver
  - Z3_mappings2
    
    Optimizer
    
    Solver

Legend:
Library
Module
Module type
Parameter
Class
Class type

Z3_incremental is a specific instantiation of Incremental with Z3_mappings, creating an incremental solver designed for the Z3 SMT solver.

type t

type solver

val solver_time : float Stdlib.ref

Time spent inside SMT solver.

val solver_count : int Stdlib.ref

Number of queries to the SMT solver.

val pp_statistics : Stdlib.Format.formatter -> t -> unit

Print solver statistics.

val create : ?params:Params.t -> ?logic:Ty.logic -> unit -> t

create ?params ?logic () creates a new solver.

?params is of type Params.t and is used to modify/set parameters inside the solver.

?logic is of type Solver_intf.logic and is used to set the theory of the assertions used. When knowing what the underlying theory is going to be, setting this parameter can help the SMT solver be more performant. The default logic is unknown_theory.

val interrupt : t -> unit

Interrupt solver.

val clone : t -> t

Clone a given solver.

val push : t -> unit

Create a backtracking point.

val pop : t -> int -> unit

pop solver n backtracks n backtracking points.

val reset : t -> unit

Resets the solver, i.e., remove all assertions from the solver.

val add : t -> Expr.t list -> unit

Assert one or multiple constraints into the solver.

val get_assertions : t -> Expr.t list

The set of assertions in the solver.

val check : t -> Expr.t list -> Solver_intf.satisfiability

check solver es checks the satisfiability of the assertions in the solver using the assumptions in es.

Raises Unknown if the SMT solver returns unknown.

val get_value : t -> Expr.t -> Expr.t

get_value solver e get an expression denoting the model value of a given expression.

Requires that the last check query returned true.

val model : ?symbols:Symbol.t list -> t -> Model.t option

The model of the last check.

The result is None if check was not invoked before, or its result was not Satisfiable.