Index of values

Add a rule to the system

Add the term->data binding.

Interpret the given constant by the given function.

Add a builtin fun

Add given list of axioms

Add given list of axioms

Test for alpha equivalence.

apply the relation symbol to some term

Special version of alpha_equiv, using distinct scopes for the two terms to test, and discarding the result

Number of subliterals of the literal.

Returns the answers to a query in a given DB.

Given a list of variables, and a list of literals that contain those variables, return a set.

Extension of TopDown.S.ask, where the query ranges over the list of variables (the term list), all of which must be bound in the list of literals that form a constraint.

Bind a variable,scope to a term,scope

Default builtin functions

Number of elements of the set

A datalog clause is safe iff all variables in its head also occur in its body

Alpha equivalence of clauses.

Parse a clause from a string, or fail.

Copy the rewriting system

Recursive copy of the index

New relation, with given name and argument

New rewriting system

Add the clause/fact to the DB as an axiom, updating fixpoint.

Add a fact (ground unit clause)

Add a function to be called on new literals.

Deep copy of the DB

Create a DB

Explain the given fact by returning a list of facts that imply it under the current clauses, or raise Not_found

Get all the explanations that explain why this clause is true

Fold on all clauses in the current DB (including fixpoint)

Add a goal to the DB.

Iterate on all current goals

match the given literal with facts of the DB, calling the handler on each fact that match

Is the clause member of the DB?

Immediate premises of the fact (ie the facts that resolved with a clause to give the literal), plus the clause that has been used.

Like BottomUp.S.db_match, but the additional int list is used to select bindings of variables in the literal.

Size of the DB

List of default interpreters for some symbols, mostly infix predicates

While the term is a variable bound in subst, follow its binding.

Create a new embedding.

new, empty index

Empty subst

Check whether clauses are (syntactically) equal

Are the literals equal?

Evaluate the given term at root

Evaluate the term at root

Apply the substitution to the term.

Iterate on all instances of the relation present in the DB

find clauses whose head unifies with the given term, and give them along with the unifier, to the callback

find facts unifying with the given term, and give them along with the unifier, to the callback

Given an interpreted goal, try all interpreters on it, and match the query against their heads.

The given function decides of the given relation (if it returns true for a couple of constants, then the relation holds for those constants)

The given function decides of the given relation (if it returns true for a constant, then the relation holds for this constant)

Retrieve data associated with terms that are a generalization of the given query term

Check whether this term is a "R(t)" with t an object packed with the appropriate key, and "R" the name of the given relation

Hash the clause

Hash the literal

Help messages for interpreted predicates

Add an interpreter for the given constant.

Add several interpreters, with their documentation

Is the constant interpreted by a built-in function?

A fact is a ground clause with empty body

Is the literal ground (a fact)?

Is the constant interpreted by some OCaml code?

Iterate on bindings

Evaluate the set by iterating on it

Create a term from this relation description

Hashcons the symbol

match_ a sa b sb matches the pattern a in scope sa with term b in scope sb.

max var, or 0 if ground

Create a clause from a conclusion and a list of premises

Helper to build a literal.

Name of the relation

Create a new key.

Deconstruct a clause

Deconstruct a literal

Pretty print the clause

Pretty print the literal

Print query plan

Special symbol, that will never occur in any user-defined clause or term.

reflexive db r makes r reflexive in db, ie for all X, r(X,X) holds in db.

Remove the term->data binding.

Rename the given variable into a variable that is unique within variables known to the given renaming

Normalize the term recursively.

rewrite the term, but only its root.

Load the default interpreters and builtin functions into the DB

Number of bindings

subset db r1 r2 adds to db the axiom that r2(X,Y) :- r1(X,Y); in other words, r1 is a subset of r2 as a relation

subset db r1 r2 adds to db the axiom that r2(X) :- r1(X); in other words, r1 is a subset of r2 as a relation

Axiom for symmetry (ie "r(X,Y) <=> r(Y,X)") added to the DB

tc_of db ~tc r adds to db axioms that make the relation tc the transitive closure of the relation r.

List of rules

Convert to a list

Axioms for transitivity are added to the DB

Retrieve data associated with terms that unify with the given query term

Unify the two terms.