Fixpoint3
Functions for solving Datalog programs.
Modules
| Ast | Abstract syntax trees used by the fixpoint solver. |
| Boxable | Functions for boxing and unboxing values, and for lifting functions to operate on boxed values. |
| Boxing | The purpose of this file is to represent every `Boxed` value with an `Int64`. |
| BoxingType | The purpose of this file is to record the transformation from Boxed values to Int64. |
| Debugging | Functions for printing debug output during the fixpoint computation. |
| Interpreter | Interpreter for executable RAM programs. |
| Options | Configuration options for the fixpoint solver. |
| Phase | Phases of the fixpoint solver pipeline. |
| PrecedenceGraph | `PrecedenceGraph` contains a graph module which is used to compute a stratification of a Datalog program. The stratification is based on a topological sort of the strongly connected components (SCC) of the precedence graph. |
| Predicate | This file provides an interface for interacting with `Fixpoint.Ast.Ram.Predicates`. Core features include providing a list of all `RelSym` in `Predicates`, provide the `PredType` of a `RelSym` and transforming `RelSym` of one `PredType` into a `RelSym` of another `PredType`. |
| ProvenanceReconstruct | This module reconstructs the proof tree given a provenance model. It does so by re-evaluating the program in a top-down fashion to prove the sought after atom. This search is augmented with knowledge about which facts are true and the rules used to construct them. |
| ReadWriteLock | Functions on read-write locks. |
| Solver | Functions for solving Datalog programs and querying their models. |
| TypeInfo | This module defines and offers an interface for dealing with the types of the Datalog engine. |
| Util | Utility functions for the fixpoint solver. |
Traits
| PredSymsOf | Trait for types that contain predicate symbols. |
| SubstitutePredSym | Trait for types that contain substitutable predicate symbols. |
Enums
| Boxed | Type of boxed values. |
Structs
| Counter | `Counter` is a wrapper around `Ref` for a simple counter. |
| UniqueInts | The purpose of `UniqueInts` is to assign unique numbers/identifiers to elements. |