Fixpoint3.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.

The three PredTypes originate from semi-naive evaluation and are Full, Delta and New (delta').

Instead of adding an enum type (Full/Delta/New) to the predicate, we embed the type into the identifier, which we can do since we have an upper bound on the integers used.

For a Datalog AST consisting of predicates PredSym("Road", 0) and PredSym("Path", 1) the RAM has 6 predicates, 3 for each predicate in the Datalog AST. Every predicate has a Full version, a Delta version and a New version.

For PredSym("Road", 0) the predicates in RAM are PredSym("Road", 0), PredSym("Road", 2), and PredSym("Road", 4). PredSym("Road", 0) is the full predicate, PredSym("Road", 2) is the delta predicate and PredSym("Road", 4) is the delta' predicate. For PredSym("Path", 1) the predicates in RAM are be PredSym("Path", 1), PredSym("Path", 3), and PredSym("Path", 5).

In the above way PredType is encoded in the identifier of a PredSym.

Definitions

def allFullRelSyms(predInfo: Predicates): List[RelSym] Source

Returns a list of all full RelSym in predInfo.

def allRelSyms(predInfo: Predicates): List[RelSym] Source

Returns a list of all RelSym in predInfo.

def bodyAtomToRelSym(body: BodyPredicate, wantedType: PredType, predInfo: Predicates): RelSym Source

Returns the full RelSym associated with the PredSym in body according to predInfo.

def fullRelSymToType(relSym: RelSym, wantedType: PredType, predInfo: Predicates): RelSym Source

Returns a RelSym of type wantedType given the RelSym relSym, which must be a full RelSym.

def fullRelSymsOfProgram(program: RamProgram): List[RelSym] Source

Returns a list of all RelSym known in program.

def getMax(predicates: Predicates): Int64 Source

Returns 1 plus the maximum full predicate in predicates.

def getRelSymAsType(relSym: RelSym, wantedType: PredType, predInfo: Predicates): RelSym Source

Returns the RelSym of type wantedType from relSym according to predInfo.

def headAtomToRelSym(head: HeadPredicate, wantedType: PredType, predInfo: Predicates): RelSym Source

Returns the full RelSym associated with the PredSym in head according to predInfo.

def initialize(program: Datalog, db: Map[RelSym, BPlusTree[Vector[Boxed], Boxed, Static]]): Predicates Source

Collect all preciate information given a Datalog program program and database db.

def isFullId(id: Int64, predInfo: Predicates): Bool Source

Returns true if id is the id of a full PredSym according to predInfo.

def relSymFromPredType(relSym: RelSym, wantedType: PredType, predInfo: Predicates): RelSym Source

Returns a RelSym of type wantedType from relSym according to predInfo.

def relSymToPredType(relSym: RelSym, predInfo: Predicates): PredType Source

Returns the type of the PredSym in relSym according to predInfo.

def relSymsOfProgram(program: RamProgram): List[RelSym] Source

Returns a list of all RelSym known in program.