dolmen 0.4 · 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 = ParseLocation.t

Type aliases for readability.

type inductive = {

id : Id.t;
vars : term list;
cstrs : (Id.t * term list) list;
loc : location option;

}

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 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 ontaining 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.
*)
| Def of Id.t * term
(*
Symbol definition, i.e the symbol is equal to the given term.
*)
| Decl of Id.t * term
(*
Symbol declaration, i.e the symbol has the given term as its type.
*)
| Inductive of inductive
(*
Inductive type definition, see the inductive type.
*)
| 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 prove to initial state.
*)
| Exit
(*
Exit the interactive loop.
*)

and t = {

id : Id.t;
descr : descr;
attr : term option;
loc : location option;

}

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.

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 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 -> t

Symbol declaration. fun_decl f 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 -> term -> t

Symbol definition. fun_def f 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 * 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 pp : Buffer.t -> t -> unit

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

Printing functions for statements.

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

Emit a Prove statement.

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

Pack a list of statements into a single one.

val normalize : (Term.t -> Term.t) -> t -> t

Normalize statements with regards to a normalization function on terms.

package dolmen