dolmen 0.7 · OCaml Package

Standard imlplementation of statements. This module provides a reasonable and standard implementation of statements, that can directly be used to instantiated the various functors of the dolmen library. These statements are closer to smtlib statements than to other languages statements because it is easier to express other languages statements using smtlib's than the other way around. Still, a generalisation of smtlib statements was needed so as not to lose some important distinctions between conjectures and assertions for instance.

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

package dolmen