package dolmen

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

Module type Dolmen_smtlib2_v6.StatementSource

Implementation requirement for the Smtlib format.

Sourcetype t

The type of statements.

Sourcetype id

The type of identifiers.

Sourcetype term

The type of terms.

Sourcetype location

The type of locations.

(Re)starting and terminating

Sourceval reset : ?loc:location -> unit -> t

Full reset of the prover state.

Sourceval set_logic : ?loc:location -> string -> t

Set the problem logic.

Sourceval set_option : ?loc:location -> term -> t

Set the value of a prover option.

Sourceval exit : ?loc:location -> unit -> t

Exit the interactive loop.

Modifying the assertion stack

Sourceval push : ?loc:location -> int -> t

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

Sourceval pop : ?loc:location -> int -> t

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

Sourceval reset_assertions : ?loc:location -> unit -> t

Reset assumed assertions.

Introducing new symbols

Sourceval type_decl : ?loc:location -> id -> int -> t

Declares a new type constructor with given arity.

Sourceval type_def : ?loc:location -> id -> id list -> term -> 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.

Sourceval datatypes : ?loc:location -> (id * term list * (id * term list) list) list -> t

Inductive type definitions.

Sourceval fun_decl : ?loc:location -> id -> term list -> term list -> term -> t

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

Sourceval fun_def : ?loc:location -> id -> term list -> term list -> term -> term -> t

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

Sourceval funs_def_rec : ?loc:location -> (id * term list * term list * term * term) list -> t

Declare a list of mutually recursive functions.

Asserting and inspecting formulas

Sourceval assert_ : ?loc:location -> term -> t

Add a proposition to the current set of assertions.

Sourceval get_assertions : ?loc:location -> unit -> t

Return the current set of assertions.

Checking for satisfiablity

Sourceval check_sat : ?loc:location -> term list -> t

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

Models

Sourceval get_model : ?loc:location -> unit -> t

Return the model found.

Sourceval get_value : ?loc:location -> term list -> t

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

Sourceval get_assignment : ?loc:location -> unit -> t

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

Proofs

Sourceval get_proof : ?loc:location -> unit -> t

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

Sourceval get_unsat_core : ?loc:location -> unit -> t

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

Sourceval get_unsat_assumptions : ?loc:location -> unit -> t

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

Inspecting settings

Sourceval get_info : ?loc:location -> string -> t

Get information (see smtlib manual).

Sourceval get_option : ?loc:location -> string -> t

Get the value of a prover option.

Scripts commands

Sourceval echo : ?loc:location -> string -> t

Print back as-is, including the double quotes.

Sourceval set_info : ?loc:location -> term -> t

Set information (see smtlib manual).