package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t

The type of statements.

(Re)starting and terminating

val reset : ?loc:L.t -> unit -> t

Full reset of the prover state.

val set_logic : ?loc:L.t -> string -> t

Set the problem logic.

val set_option : ?loc:L.t -> T.t -> t

Set the value of a prover option.

val exit : ?loc:L.t -> unit -> t

Exit the interactive loop.

Modifying the assertion stack

val push : ?loc:L.t -> int -> t

Push the given number of new level on the stack of assertions.

val pop : ?loc:L.t -> int -> t

Pop the given number of level on the stack of assertions.

val reset_assertions : ?loc:L.t -> unit -> t

Reset assumed assertions.

Introducing new symbols

val type_decl : ?loc:L.t -> I.t -> int -> t

Declares a new type constructor with given arity.

val type_def : ?loc:L.t -> I.t -> I.t list -> T.t -> t

Defines an alias for types. type_def f args body is such that later occurences of f applied to a list of arguments l should be replaced by body where the args have been substituted by their value in l.

val datatypes : ?loc:L.t -> (I.t * T.t list * (I.t * T.t list) list) list -> t

Inductive type definitions.

val fun_decl : ?loc:L.t -> I.t -> T.t list -> T.t list -> T.t -> t

Declares a new term symbol, and its type. fun_decl f ty_args args ret declares f as a new function symbol which takes arguments of types described in args, and with return type ret.

val fun_def : ?loc:L.t -> I.t -> T.t list -> T.t list -> T.t -> T.t -> t

Defines a new function. fun_def f ty_args args ret body is such that applications of f are equal to body (module substitution of the arguments), which should be of type ret.

val funs_def_rec : ?loc:L.t -> (I.t * T.t list * T.t list * T.t * T.t) list -> t

Declare a list of mutually recursive functions.

Asserting and inspecting formulas

val assert_ : ?loc:L.t -> T.t -> t

Add a proposition to the current set of assertions.

val get_assertions : ?loc:L.t -> unit -> t

Return the current set of assertions.

Checking for satisfiablity

val check_sat : ?loc:L.t -> T.t list -> t

Solve the current set of assertions for satisfiability, under the local assumptions specified.

Models

val get_model : ?loc:L.t -> unit -> t

Return the model found.

val get_value : ?loc:L.t -> T.t list -> t

Return the value of the given terms in the current model of the solver.

val get_assignment : ?loc:L.t -> unit -> t

Return the values of asserted propositions which have been labelled using the ":named" attribute.

Proofs

val get_proof : ?loc:L.t -> unit -> t

Return the proof of the lastest check_sat if it returned unsat, else is undefined.

val get_unsat_core : ?loc:L.t -> unit -> t

Return the unsat core of the latest check_sat if it returned unsat, else is undefined.

val get_unsat_assumptions : ?loc:L.t -> unit -> t

Return a list of local assumptions (as givne in check_sat, that is enough to deduce unsat.

Inspecting settings

val get_info : ?loc:L.t -> string -> t

Get information (see smtlib manual).

val get_option : ?loc:L.t -> string -> t

Get the value of a prover option.

Scripts commands

val echo : ?loc:L.t -> string -> t

Print back as-is, including the double quotes.

val set_info : ?loc:L.t -> T.t -> t

Set information (see smtlib manual).

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct