package dolmen

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

Signature used by the Logic class, which parses languages such as tptp, smtlib, etc... Statements of dirrent languages currently have a lot less in common than terms, so this interface looks a lot more like a patchwork of different logical framework directives than it should.

type t

The type of statements.

Optional infos for statements

val annot : ?loc:L.t -> T.t -> T.t list -> T.t

Constructors for annotations. Annotations are mainly used in TPTP.

Generic statements

val import : ?loc:L.t -> string -> t

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

val include_ : ?loc:L.t -> string -> I.t list -> t

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

val defs : ?loc:L.t -> ?attrs:T.t list -> t list -> t

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

Alt-ergo Statements

val logic : ?loc:L.t -> ac:bool -> I.t list -> T.t -> t

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

val record_type : ?loc:L.t -> I.t -> T.t list -> (I.t * T.t) 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:L.t -> I.t -> T.t list -> t

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

val algebraic_type : ?loc:L.t -> I.t -> T.t list -> (I.t * T.t 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:L.t -> t list -> t

Pack together a list of mutually recursive type definitions.

val pred_def : ?loc:L.t -> I.t -> T.t list -> T.t list -> T.t -> t

Symbol definition. pred_def p vars args body means that "p(args) = (body : bool)", i.e p is a predicate symbol with arguments args, and which returns the value body which is of type bool. The predicate can also be a top-level predicate in which case it doesn't have arguments and it just returns the value of the body which means "p = (body : bool)".

val axiom : ?loc:L.t -> I.t -> T.t -> t

Create a axiom.

val case_split : ?loc:L.t -> I.t -> T.t -> t

Create a case split.

val theory : ?loc:L.t -> I.t -> I.t -> t list -> t

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

val rewriting : ?loc:L.t -> I.t -> T.t list -> t

Create a set of rewriting rules.

val prove_goal : ?loc:L.t -> I.t -> T.t -> t

Goal declaration.

Dimacs&iCNF Statements

val p_cnf : ?loc:L.t -> int -> int -> t

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

val p_inccnf : ?loc:L.t -> unit -> t

Header of iCNF files.

val clause : ?loc:L.t -> T.t list -> t

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

val assumption : ?loc:L.t -> T.t list -> t

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

Smtlib statements

val pop : ?loc:L.t -> int -> t
val push : ?loc:L.t -> 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:L.t -> unit -> t

Reset all assertions that hase been pushed.

val assert_ : ?loc:L.t -> T.t -> t

Add an assertion to the current set of assertions.

val check_sat : ?loc:L.t -> T.t list -> t

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

val set_logic : ?loc:L.t -> string -> t

Set the logic to be used for solving.

val get_info : ?loc:L.t -> string -> t
val set_info : ?loc:L.t -> T.t -> t

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

val get_option : ?loc:L.t -> string -> t
val set_option : ?loc:L.t -> T.t -> t

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

val type_decl : ?loc:L.t -> I.t -> int -> t

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

val type_def : ?loc:L.t -> I.t -> I.t list -> T.t -> 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:L.t -> (I.t * T.t list * (I.t * T.t list) list) list -> t

Inductive type definitions. TODO: some more documentation.

val fun_decl : ?loc:L.t -> I.t -> T.t list -> T.t list -> T.t -> 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:L.t -> I.t -> T.t list -> T.t list -> T.t -> T.t -> 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:L.t -> (I.t * T.t list * T.t list * T.t * T.t) list -> t

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

val get_proof : ?loc:L.t -> 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:L.t -> 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:L.t -> 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:L.t -> unit -> t

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

val get_value : ?loc:L.t -> T.t list -> t

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

val get_assignment : ?loc:L.t -> unit -> t

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

val get_assertions : ?loc:L.t -> unit -> t

Instructs the prover to print all current assertions.

val echo : ?loc:L.t -> string -> t

Print the given sting.

val reset : ?loc:L.t -> unit -> t

Full reset of the prover state.

val exit : ?loc:L.t -> unit -> t

Exit directive (used in interactive mode).

TPTP Statements

val tpi : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val thf : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val tff : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val fof : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val cnf : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> 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:L.t -> ?attrs:T.t list -> t list -> t

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

val rewrite : ?loc:L.t -> ?attrs:T.t list -> T.t -> 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:L.t -> ?attrs:T.t list -> T.t -> t

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

val assume : ?loc:L.t -> ?attrs:T.t list -> T.t -> t

Adds an hypothesis.

val lemma : ?loc:L.t -> ?attrs:T.t list -> T.t -> t

Lemmas.

val decl : ?loc:L.t -> ?attrs:T.t list -> I.t -> T.t -> t

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

val definition : ?loc:L.t -> ?attrs:T.t list -> I.t -> T.t -> T.t list -> t

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

val inductive : ?loc:L.t -> ?attrs:T.t list -> I.t -> T.t list -> (I.t * T.t 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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct