dolmen

A parser library for automated deduction
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen.std

Type definitions

type term = Term.t
type location = Loc.t

Type aliases for readability.

type abstract = {
id : Id.t;
ty : term;
loc : location;
}

The type for abstract type definitions.

type inductive = {
id : Id.t;
vars : term list;
cstrs : (Id.t * term list) list;
loc : location;
attrs : term list;
}

The type for inductive type declarations. The "vars" field if used to store polymorphic variables of the inductive type. For instance, a polymorphic type for lists would have a single variable "a". The constructors each have a name and a list of concrete arguments types (they all implicitly take as many type arguments as there are variables). So, for instance, the polymorphic list type would have two constructors:

  • "Nil", []
  • "Cons", [var "a"]
type record = {
id : Id.t;
vars : term list;
fields : (Id.t * term) list;
loc : location;
attrs : term list;
}

The type of record definitions.

type decl =
| Abstract of abstract
| Record of record
| Inductive of inductive

Type definitions, type declarations, and term declaration.

type def = {
id : Id.t;
loc : location;
vars : term list;
params : term list;
ret_ty : term;
body : term;
}

Term definition.

type 'a group = {
contents : 'a list;
recursive : bool;
}

Groups of declarations or definitions, which can be recursive or not.

type defs = def group
type decls = decl group

Convenient aliases

type descr =
| Pack of t list(*

Pack a list of statements that have a semantic meaning (for instance a list of mutually recursive inductive definitions).

*)
| Pop of int(*

Pop the stack of assertions as many times as specified.

*)
| Push of int(*

Push as many new levels on the stack of assertions as specified.

*)
| Reset_assertions(*

Reset all assertions.

*)
| Plain of term(*

A plain statement containing a term with no defined semantics.

*)
| Prove of term list(*

Try and prove the current sequent, under some local assumptions.

*)
| Clause of term list(*

Add the given clause on the left side of the current sequent.

*)
| Antecedent of term(*

Add the given proposition on the left of the current sequent.

*)
| Consequent of term(*

Add the given proposition on the right of the current sequent.

*)
| Include of string(*

File include, qualified include paths, if any, are stored in the attribute.

*)
| Set_logic of string(*

Set the logic to use for proving.

*)
| Get_info of string(*

Get required information.

*)
| Set_info of term(*

Set the information value.

*)
| Get_option of string(*

Get the required option value.

*)
| Set_option of term(*

Set the option value.

*)
| Defs of def group(*

Symbol definition, i.e the symbol is equal to the given term.

*)
| Decls of decl group(*

A list of potentially recursive type definitions.

*)
| Get_proof(*

Get the proof of the last sequent (if it was proved).

*)
| Get_unsat_core(*

Get the unsat core of the last sequent.

*)
| Get_unsat_assumptions(*

Get the local assumptions in the unsat core of the last sequent.

*)
| Get_model(*

Get the current model of the prover.

*)
| Get_value of term list(*

Get the value of some terms in the current model of the prover.

*)
| Get_assignment(*

Get the assignment of labbeled formulas (see smtlib manual).

*)
| Get_assertions(*

Get the current set of assertions.

*)
| Echo of string(*

Prints the string.

*)
| Reset(*

Full reset of the prover to its initial state.

*)
| Exit(*

Exit the interactive loop.

*)
and t = {
id : Id.t option;
descr : descr;
attrs : term list;
loc : location;
}

The type of statements. Statements have optional location and attributes (or annotations). Additionally the each have a name (which mainly comes from tptp statements), that can very well be the empty string (and so it is likely not unique).

Implemented interfaces

include Dolmen_intf.Stmt.Logic with type t := t and type id := Id.t and type term := term and type location := location

Optional infos for statements

val annot : ?loc:location -> term -> term list -> term

Constructors for annotations. Annotations are mainly used in TPTP.

Generic statements

val import : ?loc:location -> string -> t

Import directive. Same as include_ but without filtering on the statements to import.

val include_ : ?loc:location -> string -> Id.t list -> t

Inlcude directive. include file l means to include in the current scope the directives from file file that appear in l. If l is the empty list, all directives should be imported.

Alt-ergo Statements

val logic : ?loc:location -> ac:bool -> Id.t list -> term -> t

Functions type definition. Allows to specify whether a list of symbol is ac or not

val record_type : ?loc:location -> Id.t -> term list -> (Id.t * term) list -> t

Declares a new record type, with first a list of type variables, and then the list of the record fields.

val abstract_type : ?loc:location -> Id.t -> term list -> t

Declare a new abstract type, quantified over the given list of type variables.

val algebraic_type : ?loc:location -> Id.t -> term list -> (Id.t * term list) list -> t

Defines a new algebraic datatype, quantified over the lsit of type variables, and with a list of cases each containing a constructor id and a list of fields.

val rec_types : ?loc:location -> t list -> t

Pack together a list of mutually recursive type definitions.

val axiom : ?loc:location -> Id.t -> term -> t

Create a axiom.

val case_split : ?loc:location -> Id.t -> term -> t

Create a case split.

val theory : ?loc:location -> Id.t -> Id.t -> t list -> t

Create a theory, extending another, with the given list of declarations.

val rewriting : ?loc:location -> Id.t -> term list -> t

Create a set of rewriting rules.

val prove_goal : ?loc:location -> Id.t -> term -> t

Goal declaration.

Dimacs&iCNF Statements

val p_cnf : ?loc:location -> int -> int -> t

Header of dimacs files. First argument is the number of variables, second is the number of clauses.

val p_inccnf : ?loc:location -> unit -> t

Header of iCNF files.

val clause : ?loc:location -> term list -> t

Add to the current set of assertions the given list of terms as a clause.

val assumption : ?loc:location -> term list -> t

Solve the current set of assertions, with the given assumptions.

Smtlib statements

val pop : ?loc:location -> int -> t
val push : ?loc:location -> int -> t

Directives for manipulating the set of assertions. Push directives creates backtrack point that can be reached using Pop directives.

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

Reset all assertions that hase been pushed.

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

Add an assertion to the current set of assertions.

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

Directive that instructs the prover to solve the current set of assertions, undr some local assumptions.

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

Set the logic to be used for solving.

val get_info : ?loc:location -> string -> t
val set_info : ?loc:location -> term -> t

Getter and setter for various informations (see smtlib manual).

val get_option : ?loc:location -> string -> t
val set_option : ?loc:location -> term -> t

Getter and setter for prover options (see smtlib manual).

val type_decl : ?loc:location -> Id.t -> int -> t

Type declaration. type_decl s n declare s as a type constructor with arity n.

val type_def : ?loc:location -> Id.t -> Id.t list -> term -> t

Type definition. type_def f args body declare that f(args) = body, i.e any occurence of "f(l)" should be replaced by body where the "args" have been substituted by their corresponding value in l.

val datatypes : ?loc:location -> (Id.t * term list * (Id.t * term list) list) list -> t

Inductive type definitions. TODO: some more documentation.

val fun_decl : ?loc:location -> Id.t -> term list -> term list -> term -> t

Symbol declaration. fun_decl f vars args ret defines f as a function which takes arguments of type as described in args and which returns a value of type ret.

val fun_def : ?loc:location -> Id.t -> term list -> term list -> term -> term -> t

Symbol definition. fun_def f vars args ret body means that "f(args) = (body : ret)", i.e f is a function symbol with arguments args, and which returns the value body which is of type ret.

val funs_def_rec : ?loc:location -> (Id.t * term list * term list * term * term) list -> t

Define a list of mutually recursive functions. Each functions has the same definition as in fun_def

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

If the last call to check_sat returned UNSAT, then instruct the prover to return the proof of unsat.

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

If the last call to check_sat returned UNSAT, then instruct the prover to return the unsat core of the unsatisfiability proof, i.e the smallest set of assertions needed to prove false.

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

If the last call to check_sat returned UNSAT, then instruct the prover to return a subset of the local assumptions that is sufficient to deduce UNSAT.

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

If the last call to check_sat returned SAT, then return the associated model.

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

Instructs the prover to return the values of the given closed quantifier-free terms.

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

Instructs the prover to return truth assignemnt for labelled formulas (see smtlib manual for more information).

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

Instructs the prover to print all current assertions.

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

Print the given sting.

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

Full reset of the prover state.

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

Exit directive (used in interactive mode).

TPTP Statements

val tpi : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val thf : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val tff : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val fof : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val cnf : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t

TPTP directives. tptp name role t instructs the prover to register a new directive with the given name, role and term. Current tptp roles are:

  • "axiom", "hypothesis", "definition", "lemma", "theorem" acts as new assertions/declartions
  • "assumption", "conjecture" are proposition that need to be proved, and then can be used to prove other propositions. They are equivalent to the following sequence of smtlib statements:

    • push 1
    • assert (not t)
    • check_sat
    • pop 1
    • assert t
  • "negated_conjecture" is the same as "conjecture", but the given proposition is false (i.e its negation is the proposition to prove).
  • "type" declares a new symbol and its type
  • "plain", "unknown", "fi_domain", "fi_functors", "fi_predicates" are valid roles with no specified semantics
  • any other role is an error

Zipperposition statements

val data : ?loc:location -> ?attrs:term list -> t list -> t

Packs a list of mutually recursive inductive type declarations into a single statement.

val defs : ?loc:location -> ?attrs:term list -> t list -> t

Packs a list of mutually recursive definitions into a single statement.

val rewrite : ?loc:location -> ?attrs:term list -> term -> t

Declare a rewrite rule, i.e a universally quantified equality or equivalence that can be oriented according to a specific ordering.

val goal : ?loc:location -> ?attrs:term list -> term -> t

The goal, i.e the propositional formula to prove.

val assume : ?loc:location -> ?attrs:term list -> term -> t

Adds an hypothesis.

val lemma : ?loc:location -> ?attrs:term list -> term -> t

Lemmas.

val decl : ?loc:location -> ?attrs:term list -> Id.t -> term -> t

Symbol declaration. decl name ty declares a new symbol name with type ty.

val definition : ?loc:location -> ?attrs:term list -> Id.t -> term -> term list -> t

Symbol definition. def name ty term defines a new symbol name of type ty which is equal to term.

val inductive : ?loc:location -> ?attrs:term list -> Id.t -> term list -> (Id.t * term list) list -> t

Inductive type definitions. inductive name vars l defines an inductive type name, with polymorphic variables vars, and with a list of inductive constructors l.

Additional functions

val mk_decls : ?loc:location -> ?attrs:term list -> recursive:bool -> decl list -> t

Create a group of declarations

val mk_defs : ?loc:location -> ?attrs:term list -> recursive:bool -> def list -> t

Create a group of declarations

val prove : ?loc:location -> unit -> t

Emit a Prove statement.

val pack : ?id:Id.t -> ?loc:location -> ?attrs:term list -> t list -> t

Pack a list of statements into a single one.

Printing functions

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

Printing functions for statements.

val print_decl : Stdlib.Format.formatter -> decl -> unit
val print_def : Stdlib.Format.formatter -> def -> unit
val print_group : ( Stdlib.Format.formatter -> 'a -> unit ) -> Stdlib.Format.formatter -> 'a group -> unit