package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Optional infos for statements
Generic statements
Dimacs&iCNF Statements
Smtlib statements
TPTP Statements
Zipperposition statements

dolmen
- Dolmen
  - Intf
dolmen.class
- Dolmen_class
  - Logic
    
    Make
    
    I
    
    L
    
    S
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    T
dolmen.dimacs
- Dolmen_dimacs
  - Make
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.icnf
- Dolmen_icnf
  - Make
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.intf
- Dolmen_intf
  - Id
    
    Logic
  - Language
    
    S
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
  - Lex
    
    S
  - Location
    
    S
  - Parse
    
    S
    
    Incremental
    
    MenhirInterpreter
  - Stmt
    
    Logic
  - Term
    
    Logic
dolmen.line
- Dolmen_line
dolmen.smtlib
- Dolmen_smtlib
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.std
- Dolmen_std
  - Id
  - Misc
  - Normalize
    
    Smtlib
    
    Tptp
  - ParseLocation
  - Statement
  - Term
  - Transformer
    
    Make
    
    Lex
    
    Loc
    
    Parse
    
    Incremental
    
    MenhirInterpreter
    
    Ty
dolmen.tptp
- Dolmen_tptp
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.zf
- Dolmen_zf
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term

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

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:L.t -> int -> int -> t

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

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

Define a list of mutually recursive functions. Each functions 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 defs : ?loc:L.t -> ?attrs:T.t list -> t list -> t

Packs a list of mutually recursive definitions 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.