The datalog_unfolding module

class octant.datalog_unfolding.UFBot

Bottom type corresponds to no information at all

class octant.datalog_unfolding.UFConj(args)

Conjunctions of types

It represent a conjunct of constraints on the origin. It is usually simplified at some point as one of the origins.

args = None

the members of the conjunct: args

class octant.datalog_unfolding.UFDisj(args)

Disjunctions of types

The values of the element may come from either origins.

args = None

the members of the disjunct: args

class octant.datalog_unfolding.UFGround(pos, table, occurrence)

Coerced to be a ground value of parameter at a given position

pos:

position of the argument in the table (integer starting at 0)

table:

table defining the ground term (str)

occurrence:

An occurrence list defining in a unique way the instance of the ground term in use. (linked list represented as pair or None. Elements are pairs of a rule identifier (int) and a position of the atom in the body (int))

class octant.datalog_unfolding.UFTop

Top type means any value

class octant.datalog_unfolding.UFType

Base class for unfolding types

class octant.datalog_unfolding.UnfoldPlan(plan, tables, contents)

Result of unfolding as a plan

plan

the full plan to follow for unfolding. For each rule that needs simplification the plan associate to the id of the rule, a list of simplification actions. An action is a list of elementary actions taking place at the same time. An elementary action specifies a table and a column in that table and the variable that will receive the content of this table.

class octant.datalog_unfolding.Unfolding(rules, extensible_tables, compiler)

Unfolding is the engine for performing rule enfolding

It computes types for unfolding and builds a strategy

get_atom_type(atom, i)

Computes the type of argument at position i of an atom atom

Parameters:

• atom (ast.Atom) – the atom to type
• i (int) – the position

Returns:

a type or None if not typable.

get_partially_ground_preds()

Gives back a map of the ground arguments of a table

An intentional table is ground at argument i, if in all rules defining it, the ith argument in the head is ground.

Returns:a dictionary mapping each table name to the set of argument positions (integers) that are ground for this table.

idb_extract(table_spec)

Enumerates the ground idb tables used

Parameters:table_spec – a map from tablenames to array of argument positions used. Returns:a map from tablenames to arrays of records. Records contain compiled values. Return type:dictionnary

initialize_types()

initialize table_types

The type is either bottom or Ground: arguments are the position of the argument, the name of the table and an empty context.

populate_tables(extensible_tables)

Initialize tables field

It is a map from table name to their arity and the fact they are in the IDB or the EDB

proceed()

The main entry point: type, then compute a strategy

rule_strategy(rule)

Strategy for a rule

Parameters:rule (ast.Rule) – the rule on which to compute a strategy Returns:a plan for the rule which is a list of pairs

• a tuple of tables to unfold with the position to unfold
• a list of variables solved

strategy()

Computes a strategy to unfold.

Returns:an unfoldplan made of three parts:

• the plan itself as a sequence of rules to unfold
• the ground tables that are needed associated with the list of columns used
• the contents of IDB tables (programmatically defined) that are ground and used for the expansion.

type()

Type a set of rules.

Performs a fixpoint. Each iteration type variables then type rule heads. Table types are comparable and the fixpoint is achieved when table types do not evolve.

It is the type structure that guarantees convergence.

type_tables()

Builds table types from variable types

Table types are the conjunction of the types found for each rule. :returns: next value of table types. :rtype: map from string to array of type.

type_variables()

Builds a variables type from table types.

Several types may be found for each variables as they are constrained by multiple tables.

var_types is updated with a map from variable full ids to types.

octant.datalog_unfolding.candidates(problems)

Get the set of candidate variables.

octant.datalog_unfolding.environ_from_plan(unfold_plan)

Takes a plan and compile it to a dictionnary of envs for rules

Parameters:unfold_plan – the complete plan Returns:All the environments to which one must expand the ground variables. Return type:an array of dictionnary.

octant.datalog_unfolding.get_to_solve(rule)

Gets the position where there is a predicate to simplify.

A primitive predicate with more than one variable will not be handled correctly by the difference of cube domain. It must be simplified to reach only one free variable.

octant.datalog_unfolding.head_table(rule)

Table name of the head of a rule

octant.datalog_unfolding.is_disj(t)

Return true is object is a disjonction

Parameters:t (UFType) – type to check Returns:true if disjonction false otehrwise Return type:bool

octant.datalog_unfolding.is_ground(t)

Return true is object is a ground object

Parameters:t (UFType) – type to check Returns:true if ground false otehrwise Return type:bool

octant.datalog_unfolding.len_occ(occ)

Compute length of the occurrence pseudo list

We use pairs and not regular lists because we want a hashable non mutable element.

octant.datalog_unfolding.occurrence(t)

Computes an occurrence for the whole types

Occcurrence shouldbe seen as unique ID :param UFType t: type to analyze :return: all the occurrences :rtype: tuple

octant.datalog_unfolding.reduce_conj(l)

Conjunct simplification

First it removes embedded conjunctions. If there is at least one ground type in the conjunct, keep all those ground types. Otherwise only keep the best of the conjunct and throw away the others.

Parameters:l – the list of types that could build the conjunct. It must be sorted. Returns:a conjunct with more than one type or what was considered as the best type Return type:UFType

octant.datalog_unfolding.reduce_disj(l)

Disjunction simplification

First it removes embedded disjunction.

octant.datalog_unfolding.simplify_to_ground_types(t)

Gives back simple ground or disjunction

octant.datalog_unfolding.weight_type(t)

Weight function for types.

To use in sorting but also min/max. The smaller, the better. Returns a pair for lexicographic ordering.

octant.datalog_unfolding.wrap_type(typ, mark)

Identifies the provenance of type as a given atom

Parameters:

• type – the type to wrap
• mark – mark to add. usually the identifier of rule containing the atom occurrence and the position of this atom in the body of the rule

Returns:

modified type