Phase
Phases of the fixpoint solver pipeline.
Modules
| Compiler | Phase that compiles Datalog programs to RAM programs. |
| Hoisting | The purpose of this phase is to hoist `If` ops as much as possible and merge them with `Search` into `Query` when possible/relevant. Additionally, guards are added at the top of `Insert` statements that only perform the operations if none of the involved relations are empty. For example, the following ``` search a ∈ A do search b ∈ B do search c ∈ C do if (b[0] = a[0] ∧ c[0] = a[0]) then project (a[0]) into R end end end end ``` is hoisted to ``` if (not (A = ∅) ∧ not (B = ∅) not (C = ∅)) then search a ∈ A do query {b ∈ B | b[0] = a[0]} do query {c ∈ C | c[0] = a[0]} do project (a[0]) into R end end end end ``` |
| IndexSelection | Phase that selects the indexes required by the relations of a RAM program. |
| Lowering | This phase lowers a high-level `Ram.RamProgram` into a low-level `ExecutableRam.RamProgram` executable by the Interpreter. |
| ProvenanceAugment | This module augments the program to track when and how facts were created. |
| RenamePredSyms | Purpose of phase: For `PredSym(name, id)` we want `id` to be unique, for the whole program. This phase passes over the Datalog-Ast and replaces the `id` and after everything is done recreates the old `PredSym`s for the resulting model. |
| Simplifier | Phase that simplifies and optimizes RAM programs. |
| Stratifier | Phase that computes the stratification of Datalog programs. |