dolmen 0.7 · OCaml Package

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

package dolmen