Fixpoint3.Ast.ExecutableRam.RelOp
enum RelOpSourcecase Search(Int32, Int32, Int32, BoxedDenotation, Vector[WriteTuple], RelOp)case Query(Int32, Int32, Int32, BoxedDenotation, Vector[WriteTuple], RelOp)case Functional(Int32, Vector[Boxed] -> Vector[Vector[Boxed]], Vector[RamTerm], Vector[WriteTuple], RelOp, Vector[UnifiedTypePos])case Project(Vector[RamTerm], Int32, BoxedDenotation)case ProvProject(Vector[RamTerm], Int32, Int32)case If(Vector[BoolExp], RelOp)Search(rvPos, indexPos, meet, den, writeTuple, body) iterates the facts in the
index at indexPos saving them at rvPos and using the facts as context for
writeTuple.
If den is a relational execute body.
If den is a latticenal, saves the lattice element at rvPos. If
meet != rvPos, saves the meet of the lattice element and the element at meet.
If the value saved to rvPos is not Bot execute body.
Query(rvPos, indexPos, meet, den, writeTuple, body) is the same as Search,
except the facts will be filtered by the query for rvPos.
Functional(rv, f, input, writeTuple, body, unboxingInfo) evaluates f(input),
for each result saves it as rv, does writes as described by writeTuple and
executes body. unboxingInfo can be used to unbox the values returned by f.
Project(terms, newIndex, den) constructs a tuple from terms and inserts it a
fact in index newIndex. For den == Latticenal we only insert if the
lattice-value is greater than the current and we insert with least uppber bound.
ProvProject(terms, newIndex, fullIndex) constructs a tuple from terms and inserts it a
fact in index newIndex. Values are only inserted if the depth in terms is less than
the (potential) depth of the fact in fullIndex and less than the current depth in the
fact found in newIndex.
If(bools, body) evaluates body if bools is true.