Index of values

Terms as annotations for statements.

Attach a list of attributes (also called annotations) to a term.

Constructors for annotations.

Attach a list of attributes (also called annotations) to a term.

Application.

Application of terms.

Application.

Application constructor, seen as higher order application rather than first-order application for the following reasons: being able to parse tptp's THF, having location attached to function symbols.

Function type constructor.

Arow, i.e function type constructor, currifyed.

Function type constructor, for curryfied functions.

Add a proposition to the current set of assertions.

Add an assertion to the current set of assertions.

Adds an hypothesis.

Generate a solve instruction with the given list of assumptions.

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

Make an atom from an non-zero integer.

Make an atom from an non-zero integer.

Atoms are used for dimacs cnf parsing.

The namespace for sorts (also called typee), terms and attributes, respectively.

Namespace used for attributes (also called annotations) in smtlib.

Constants lexically recognised as numbers in different formats.

Constructors for words defined as numeric formats by the languages specifications.

Solve the current set of assertions for satisfiability.

Directive that instructs the prover to solve the current set of assertions.

Indefinite description, also called choice operator.

Make a clause from a list of literals.

Make a clause from a list of literals.

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

TPTP statements, used for instance as tff ~loc ~annot name role t.

TPTP directives.

Juxtaposition of terms, usually used for annotating terms with their type.

Juxtaposition of terms, usually used for annotating terms with types.

Juxtaposition of terms, used to annotate terms with their type.

Represents juxtaposition of two terms, usually denoted "t : t'" in most languages, and mainly used to annotated terms with their supposed, or defined, type.

LogtkPosition that spans the two given positions.

N-ary version of ParseLocation.combine.

Usual functions for hashing, comparisons, equality.

Make a constant.

Create a new constant.

Constants, i.e non predefined symbols.

Variable and constant constructors.

Packs a list of mutually recursive inductive type declarations.

Predefined symbols in tptp.

Term without semantic meaning, used for creating "data" terms.

Names used to refer to tptp phrases.

Symbol declaration.

Namespace used for declaration identifiers (for instance used to filter declarations during includes)

Symbol definition.

Definite description.

Binders for variables.

Make a constant whose name possibly contain special characters (All 'distinct' constants name are enclosed in quotes).

Used in tptp to specify constants different from other constants, for instance the 'distinct' "Apple" should be syntactically different from the "Apple" constant.

Enumeration of languages together with an appropriate name.

Make an equality between terms.

Hash and equality

Usual propositional functions.

Proposition construction functions.

Existencial porpositional quantification.

Existencial porpositional qantification.

Existencial quantification.

Exit the interactive loop.

Exit directive (used in interactive mode).

Standard pre-defined constants.

The constants for the true and false propositional constants.

A function that parses an entire file, i.e until the end-of-file token, and return the list of parsed statements.

Tries and find the given file, using the language specification.

Helper function to find a file using a language specification.

Printing functions

Universal propositional quantification.

Universal propositional quantification.

Universal quantification.

Returns a full name for the identifier.

Declares a new term symbol, and its type.

Symbol declaration.

Defines a new function.

Symbol definition.

Multi-arguments function type constructor.

Return the current set of assertions.

Instructs the prover to print all current assertions.

Return the values of asserted propositions which have been labelled using the ":named" attribute.

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

Get information (see smtlib manual).

Get the value of a prover option.

Return the proof of the lastest check_sat if it returned unsat, else is undefined.

If the last call to check_sat returned UNSAT, then instruct the prover to return the proof of unsat.

Return the unsat core of the latest check_sat if it returned unsat, else is undefined.

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.

Return the value of the given terms in the current model of the solver.

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

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

Standard logical connectives viewed as terms.

Include directive.

Inlcude directive.

Inductive type definitions.

A function to parse a single statement.

Conditional, of the form ite condition then_branch els_branch.

Conditional constructor, both for first-order terms and propositions.

Function construction.

Local binding for terms.

Local term binding.

Local bindings.

Make an identifier

Make identifiers from a namespace and a string.

Make an identifier from a name and namespace.

Make an identifier from its namespace and name.

Create an identifier.

Reutnrs the lexbuf associetd with the given file or stdin, with the correct filename.

Make a position from two lewing positions.

Construction functions

Namespace used by modules (for instance in dedulkti).

The terms representing equality and disequality, respectively.

These function take as argument either a language, or a filename, and return a triple: language, language file extension (starting with a dot), appropriate parsing module Extensions should start with a dot (for instance : ".smt2")

Make a position using a lexbuf directly.

Recover a position from a lexbuf

Header of a dimacs file.

Header of dimacs files.

Given a filename, parse the file, and return the detected language together with the list of statements parsed.

Parse the given file.

Incremental parsing of either a file (see ), or stdin (with given language).

Incremental parsing.

Dependant type constructor, used for polymorphic function types.

Dependant product, or polymorphic type quantification.

Pop the given number of level on the stack of assertions.

Printing functions for statements.

Printing functionson buffer and formatters.

Printing functions.

Product of types, used for function types with more than one argument.

Product type constructor, used for instance in the types of functions that takes multiple arguments in a non-curry way.

The type of propositions.

Push the given number of new level on the stack of assertions.

Directives for manipulating the set of assertions.

Constants that are syntaxically recognised as numbers.

Declare a rewrite rule, i.e a universally quantified equality or equivalence that can be oriented according to a specific ordering.

Sequents as terms, used as sequents hyps goals.

Sequents as terms

Change the file name used for positions in this lexbuf

Set information (see smtlib manual).

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

Set the problem logic.

Set the logic to be used for solving.

Set the value of a prover option.

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

S-expressions.

S-expressions (for smtlib attributes), should probably be related to the data_t term.

smaller p1 p2 is true if p1 is included in p2, ie p1 is a sub-location of p2 (interval inclusion)

The namespace for sorts (also called types).

String representation of the variant

Comparison of type (used in tptp's THF).

Subtype relation for types.

The type of types, defined as specific token by the Zipperposition format; in other languages, will be represented as a constant (the "$tType" constant in tptp for instance).

Usual namespace, used for temrs, types and propositions.

The naemspace for terms, types, and pretty much everything

The usual namespace for terms.

The function producing token from a lexbuf.

Declares a new type constructor with given arity.

Type declaration.

Defines an alias for types.

Type definition.

Union of types.

Union type constructor, currently used in tptp's THF format.

Make a variable (in tptp, variable are syntaxically different from constants).

The wildcard term, usually used in place of type arguments to explicit polymorphic functions to not explicit types that can be inferred by the type-checker.