package dolmen

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

Module Dolmen_std.StatementSource

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

Sourcetype term = Term.t
Sourcetype location = Loc.t

Type aliases for readability.

Sourcetype abstract = {
  1. id : Id.t;
  2. ty : term;
  3. loc : location;
  4. attrs : term list;
}

The type for abstract type definitions.

Sourcetype inductive = {
  1. id : Id.t;
  2. vars : term list;
  3. cstrs : (Id.t * term list) list;
  4. loc : location;
  5. 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"]
Sourcetype record = {
  1. id : Id.t;
  2. vars : term list;
  3. fields : (Id.t * term) list;
  4. loc : location;
  5. attrs : term list;
}

The type of record definitions.

Sourcetype decl =
  1. | Abstract of abstract
  2. | Record of record
  3. | Inductive of inductive

Type definitions, type declarations, and term declaration.

Sourcetype def = {
  1. id : Id.t;
  2. vars : term list;
  3. params : term list;
  4. ret_ty : term;
  5. body : term;
  6. loc : location;
  7. attrs : term list;
}

Term definition.

Sourcetype 'a group = {
  1. contents : 'a list;
  2. recursive : bool;
}

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

Sourcetype defs = def group
Sourcetype decls = decl group

Convenient aliases

Sourcetype local = {
  1. hyps : term list;
  2. goals : term list;
}

Local hypothesis and consequents used by Prove.

Sourcetype other = {
  1. name : Id.t;
    (*

    The name of the statement, used to determine its semantics. For instance, it might be `plain` or `minimize`.

    *)
  2. args : term list;
    (*

    The arguments/payloads of the statements. The elements of the list, and their interpretation depends on the input language and the contents of the `name`.

    *)
}

'Other' statements serve to encode input statements whose semantics are not expressible using the other statements. Examples of that are `plain` statements from TPTP, or extension statements from SMTLIBv2.

Sourcetype descr =
  1. | Pack of t list
    (*

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

    *)
  2. | Pop of int
    (*

    Pop the stack of assertions as many times as specified.

    *)
  3. | Push of int
    (*

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

    *)
  4. | Reset_assertions
    (*

    Reset all assertions.

    *)
  5. | Prove of local
    (*

    Try and prove the current consequents or local consequents, under some local assumptions.

    *)
  6. | Clause of term list
    (*

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

    *)
  7. | Antecedent of term
    (*

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

    *)
  8. | Consequent of term
    (*

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

    *)
  9. | Include of string
    (*

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

    *)
  10. | Set_logic of string
    (*

    Set the logic to use for proving.

    *)
  11. | Get_info of string
    (*

    Get required information.

    *)
  12. | Set_info of term
    (*

    Set the information value.

    *)
  13. | Get_option of string
    (*

    Get the required option value.

    *)
  14. | Set_option of term
    (*

    Set the option value.

    *)
  15. | Defs of def group
    (*

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

    *)
  16. | Decls of decl group
    (*

    A list of potentially recursive type definitions.

    *)
  17. | Get_proof
    (*

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

    *)
  18. | Get_unsat_core
    (*

    Get the unsat core of the last sequent.

    *)
  19. | Get_unsat_assumptions
    (*

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

    *)
  20. | Get_model
    (*

    Get the current model of the prover.

    *)
  21. | Get_value of term list
    (*

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

    *)
  22. | Get_assignment
    (*

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

    *)
  23. | Get_assertions
    (*

    Get the current set of assertions.

    *)
  24. | Other of other
    (*

    A statement with no semantics, or semantics that are not expressible with the current type of statements.

    *)
  25. | Echo of string
    (*

    Prints the string.

    *)
  26. | Reset
    (*

    Full reset of the prover to its initial state.

    *)
  27. | Exit
    (*

    Exit the interactive loop.

    *)
Sourceand t = {
  1. id : Id.t option;
  2. descr : descr;
  3. attrs : term list;
  4. 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

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

Constructors for annotations. Annotations are mainly used in TPTP.

Generic statements

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

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

Sourceval include_ : ?loc:location -> string -> Id.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.

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

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

Alt-ergo Statements

Sourceval 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

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

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

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

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

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

Pack together a list of mutually recursive type definitions.

Sourceval pred_def : ?loc:location -> Id.t -> term list -> term list -> term -> 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)".

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

Create a axiom.

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

Create a case split.

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

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

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

Create a set of rewriting rules.

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

Goal declaration.

Sourceval prove_sat : ?loc:location -> name:Id.t -> term list -> t

Check-sat declaration.

Dimacs&iCNF Statements

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

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

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

Header of iCNF files.

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

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

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

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

Smtlib statements

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

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

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

Reset all assertions that hase been pushed.

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

Add an assertion to the current set of assertions.

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

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

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

Set the logic to be used for solving.

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

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

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

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

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

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

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

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

Inductive type definitions. TODO: some more documentation.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Instructs the prover to print all current assertions.

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

Print the given sting.

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

Full reset of the prover state.

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

Exit directive (used in interactive mode).

TPTP Statements

Sourceval tpi : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
Sourceval thf : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
Sourceval tff : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
Sourceval fof : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
Sourceval 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

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

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

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

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

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

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

Adds an hypothesis.

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

Lemmas.

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

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

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

Sourceval 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

Sourceval other : ?id:Id.t -> ?loc:location -> ?attrs:term list -> Id.t -> term list -> t

Create an 'Other' statement.

Sourceval add_attrs : term list -> t -> t

Add some attributes to a statement.

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

Create a group of declarations

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

Create a group of declarations

Sourceval def : ?loc:location -> Id.t -> vars:term list -> params:term list -> term -> term -> def

Create a single definition.

Sourceval group : recursive:bool -> 'a list -> 'a group

Make a group 'usually of declarations/definitions.

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

Emit a Prove statement.

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

Pack a list of statements into a single one.

Printing functions

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

Printing functions for statements.

Sourceval print_decl : Format.formatter -> decl -> unit
Sourceval print_def : Format.formatter -> def -> unit
Sourceval print_group : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a group -> unit
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