Edit on GitHub

Indexes

In Deductive an interface for defining indexes on tables is defined. This redefinition is necessary since the form of index is often different (although similar) to the classic balancing binary tree structure which most indexes employ.

Deductive.index — Function
index(expressions::Set{AbstractExpression})

Creates an Index for a given set of expressions.

source
index(expressions::Set{AbstractExpression})

Creates an Index for a given vector of expressions. This is the same as indexing the set containing all elements in the vector.

source

Index Structure

This structure provides the interface from which all indexes will use. The parametric type E describes the element type which is being indexed, and the type T describes the type of table which the index is using.

Deductive.Index — Type
Index(table::T, identifier_map::Dict{Int, E}) where {E, T}

Generic index container type which maps between index identifiers and associated values, as well as references the root table of the index. In a linear index the table field contains the only index table, but in recursive indices this table is merely the root of the index where the search starts.

source
Deductive.add! — Method
add!(idx::Index{E, T}, el::E) where {E, T}

Adds an element to an index, making it searchable.

source
Deductive.search — Method
search(idx::Index{E, T}, pattern::E) where {E, T}

Searches an index for a given pattern, which is not necessarily an exact match. This function merely passes the search call to the root index table, so details with how pattern matching is handled will be clarified by the search function documentation for a specific index table type.

source

Expression Indexing

Expression indexing allows for very quick pattern matching across very large sets of expressions simultaneously. Indexing doesn't improve the pattern match speed of a single pattern, but drastically decreases pattern match speed of multiple indexed expressions by leveraging similarities in structure across different indexed expressions.

Deductive.OperatorIndexTable — Type
OperatorIndexTable(roots::Set{Int}, operators::Dict{LogicalOperation, Vector{OperatorIndexTable}})

Structure for a operator table, which keeps a mapping from operators to their constituent argument subexpressions. Roots is a set of identifiers which have been matched at this table level and operators is a dictionary mapping each logical operation to a list of subtables corresponding directly to each of the operator's arguments.

Usually indexes aren't constructed directly through this constructor, but rather through helper functions like index.

source
Deductive.add! — Method
add!(table::OperatorIndexTable, entry::Tuple{Int, LogicalSymbol})

Add an index entry to an OperatorIndexTable for a LogicalSymbol. LogicalSymbols are trivial additions to a operator index since a symbol means that a search has hit a root. Therefore this method just adds the symbol to the table's roots.

source
Deductive.add! — Method
add!(table::OperatorIndexTable, entry::Tuple{Int, LogicalExpression})

Add an index entry to an OperatorIndexTable for a LogicalExpression. LogicalExpressions get added to an operator table's roots regardless and each of its arguments get added to its operations corresponding subtables.

source
Deductive.search — Method
search(table::OperatorIndexTable, sym::LogicalSymbol)

Perform a trivial search in an operator table for a symbol. Since logical symbols are expression tree roots, this search will immediately return the roots of the particular OperatorIndexTable.

source
Deductive.search — Method
search(table::OperatorIndexTable, operator_pattern::LogicalExpression)

Search for an operator pattern in a OperatorIndexTable.

Note

There's an important distinction between "expression pattern" and "operator pattern". An expression pattern matches both operator and symbol structure, while an operator pattern only matches an operator structure. Take the expression (a ∧ b) ∧ c for instance. The pattern a ∧ a, when interpreted as an expression pattern, would not match, while when interpreted as an operator pattern it would match.

source