hegg-0.3.0.0: Fast equality saturation in Haskell
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Equality.Matching.Database

Description

Custom database implemented with trie-maps specialized to run conjunctive queries using a (worst-case optimal) generic join algorithm.

Used in e-matching (Matching) as described by "Relational E-Matching" https://arxiv.org/abs/2108.02290.

You probably don't need this module.

Synopsis

Documentation

genericJoin :: forall l. Language l => Database l -> Query l -> [Subst] Source #

Run a conjunctive Query on a Database

Produce the list of valid substitutions from query variables to the query-matching class ids.

newtype Database lang Source #

The relational representation of an e-graph, as described in section 3.1 of "Relational E-Matching".

Every e-node with symbol 𝑓 in the e-graph corresponds to a tuple in the relation 𝑅𝑓 in the database. If 𝑓 has arity 𝑘, then 𝑅𝑓 will have arity 𝑘 + 1; its first attribute is the e-class id that contains the corresponding e-node , and the remaining attributes are the 𝑘 children of the 𝑓 e-node

For every existing symbol in the e-graph the Database has a table.

In concrete, we map Operators to IntTries -- each operator has one table represented by an IntTrie

Constructors

DB (Map (Operator lang) IntTrie) 

data Query lang Source #

A conjunctive query to be run on the database

Constructors

Query ![Var] ![Atom lang] 
SelectAllQuery !Var 

data IntTrie Source #

An integer triemap that keeps a cache of all keys in at each level.

As described in the paper: Generic join requires two important performance bounds to be met in order for its own run time to meet the AGM bound. First, the intersection [...] must run in 𝑂 (min(|𝑅𝑗 .𝑥 |)) time. Second, the residual relations should be computed in constant time, i.e., computing from the relation 𝑅(𝑥, 𝑦) the relation 𝑅(𝑣𝑥 , 𝑦) for some 𝑣𝑥 ∈ 𝑅(𝑥, 𝑦).𝑥 must take constant time. Both of these can be solved by using tries (sometimes called prefix or suffix trees) as an indexing data structure.

Constructors

MkIntTrie 

Fields

type Subst = IntMap ClassId Source #

Mapping from Var to ClassId. In a Subst there is only one substitution for each variable

type Var = Int Source #

A variable in a query is identified by an Int. This is much more efficient than using e.g. a String.

As a consequence, patterns also use Int to represent a variable, but we can still have an IsString instance for variable patterns by hashing the string into a unique number.

data Atom lang Source #

An Atom 𝑅ᵢ(𝑣, 𝑣1, ..., 𝑣𝑘) is defined by the relation 𝑅ᵢ and by the class-ids or variables 𝑣, 𝑣1, ..., 𝑣𝑘. It represents one conjunctive query's body atom.

Constructors

Atom 

Fields

  • !ClassIdOrVar

    Represents 𝑣

  • !(lang ClassIdOrVar)

    Represents 𝑅ᵢ(𝑣1, ..., 𝑣𝑘). Note how 𝑣 isn't included since the arity of the constructor is 𝑘 instead of 𝑘+1.