package smtml

  1. Overview
  2. Docs
An SMT solver frontend for OCaml

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (7)

Authors

  1. J
    João Pereira <joaomhmpereira@tecnico.ulisboa.pt>
  2. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>
  3. H
    Hichem Rami Ait El Hara <hra@ocamlpro.com>
  4. L
    Léo Andrès <contact@ndrs.fr>
  5. A
    Arthur Carcano <arthur.carcano@ocamlpro.com>
  6. P
    Pierre Chambart <pierre.chambart@ocamlpro.com>
  7. J
    José Fragoso Santos <jose.fragoso@tecnico.ulisboa.pt>

Maintainers

  1. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>

Sources

v0.12.0.tar.gz
md5=f8549c12d40e6a1dafcced7e319887a4
sha512=f147faa9e2519585cfe9b11654b750061259da4db0b2136d9047b4cb480abb562f6ac627545fd06461f4414acba57558713868de370f58131f3face308f7c7f0

doc/smtml/Smtml/Solver/Batch/index.html

Module Solver.BatchSource

The Batch module is parameterized by the mapping module M implementing Mappings_intf.S. In this mode, the solver delays all interactions with the underlying SMT solver until necessary.

Parameters

module _ : Mappings_intf.S

Signature

Sourcetype t

The type of solvers.

Sourcetype solver

The type of underlying solver instances.

Sourceval solver_time : float Smtml_prelude.ref

solver_time tracks the time spent inside the SMT solver.

Sourceval solver_count : int Smtml_prelude.ref

solver_count tracks the number of queries made to the SMT solver.

Sourceval pp_statistics : t Fmt.t

pp_statistics fmt solver pretty-prints solver statistics using the formatter fmt.

Sourceval create : ?params:Params.t -> ?logic:Logic.t -> 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 Logic.t and is used to set the theory of the assertions used. When the underlying theory is known, setting this parameter can improve solver performance. The default logic is ALL.
Sourceval interrupt : t -> unit

interrupt solver interrupts the current solver operation.

Sourceval clone : t -> t

clone solver creates a copy of the solver solver.

Sourceval push : t -> unit

push solver creates a backtracking point in the solver solver.

Sourceval pop : t -> int -> unit

pop solver n backtracks n backtracking points in the solver solver.

Sourceval reset : t -> unit

reset solver resets the solver solver, removing all assertions.

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

add solver exprs asserts one or multiple constraints exprs into the solver solver.

Sourceval add_set : t -> Expr.Set.t -> unit

add_set solver set asserts constraints from the set set into the solver solver.

Sourceval get_assertions : t -> Expr.t list

get_assertions solver retrieves the set of assertions in the solver solver.

  • deprecated Please use 'get_statistics' instead
Sourceval get_statistics : t -> Statistics.t

get_statistics solver retrieves statistics from the solver solver.

Sourceval check : t -> Expr.t list -> [ `Sat | `Unsat | `Unknown ]

check solver es checks the satisfiability of the assertions in the solver solver using the assumptions in es. Returns `Sat, `Unsat, or `Unknown.

Sourceval check_set : t -> Expr.Set.t -> [ `Sat | `Unsat | `Unknown ]

check_set solver set checks the satisfiability of the assertions in the solver solver using the assumptions in the set set. Returns `Sat, `Unsat, or `Unknown.

Sourceval get_value : t -> Expr.t -> Expr.t

get_value solver expr retrieves an expression denoting the model value of the given expression expr. Requires that the last check query returned `Sat.

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

model ?symbols solver retrieves the model of the last check query. If ?symbols is provided, only the values of the specified symbols are included. Returns None if check was not invoked before or its result was not `Sat.

Not compatible with cached solver mode - use get_sat_model instead

  • see get_sat_model

    For cached solver-compatible alternative

Sourceval get_sat_model : ?symbols:Symbol.t list -> t -> Expr.Set.t -> [ `Model of Model.t | `Unsat | `Unknown ]

Compute and retrieve a model for specific constraints.

get_sat_model ?symbols solver exprs performs: 1. check_set with exprs constraints 2. Returns model if result is `Sat

Filters output using ?symbols when provided. Designed for cached solvers.

  • see model

    For non-cached solvers when you have already performed your own check/check_set and want to retrieve the results