The congress.datalog.compile Module

class congress.datalog.compile.Compiler

Bases: object

Process Congress policy file.

print_parse_result()
raise_errors()
read_source(input, input_string=False, theories=None, use_modules=True)
sigerr(error)
sigwarn(error)
class congress.datalog.compile.DatalogSyntax(theories=None, use_modules=True)

Bases: object

Read Datalog syntax and convert it to internal representation.

class Lexer(char_stream, state=None)

Bases: congress.datalog.Python2.CongressLexer.CongressLexer

displayRecognitionError(token_names, e)
getErrorHeader(e)
class Parser(tokens, state=None)

Bases: congress.datalog.Python2.CongressParser.CongressParser

displayRecognitionError(token_names, e)
getErrorHeader(e)
antlr_atom_str(antlr)
atom_vars(antlr_atom)
convert_to_congress(antlr)
create(antlr)
create_and_literals(antlr)
create_atom_aux(antlr)
create_atom_dual_arg_list(antlr)

Get parameter list and named list

Return (i) a list of compile.Term representing the positionally specified parameters in the ANTLR atom and (ii) a dictionary mapping string/number to compile.Term representing the name/index-specified parameters. If there are errors self.errors is modified.

create_event(antlr)
create_literal(antlr)
create_modal_atom(antlr)
create_rule(antlr)
create_tablename(antlr)
create_term(antlr)
literal_and_vars(antlr_and)
classmethod parse_file(input, input_string=False)
rule_variables(antlr_rule)

Get variables in the rule.

Returns a set of all variable names (as strings) that occur in the given rule ANTLR_RULE.

unused_variable_prefix(antlr_rule)

Get unused variable prefix.

Returns variable prefix (string) that is used by no other variable in the rule ANTLR_RULE.

variable_name(antlr)
class congress.datalog.compile.Event(formula=None, insert=True, proofs=None, target=None)

Bases: object

Represents a change to a formula.

formula
insert
is_insert()
lstr()
proofs
tablename(default_theory=None)
target
class congress.datalog.compile.Fact(table, values)

Bases: tuple

Represent a Fact (a ground literal)

Use this class to represent a fact such as Foo(1,2,3). While one could use a Rule to represent the same fact, this Fact datastructure is more memory efficient than a Rule object since this Fact stores the information as a native tuple, containing native values like ints and strings. Notes that this subclasses from tuple.

SORT_RANK = 3
class congress.datalog.compile.Literal(table, arguments, location=None, negated=False, use_modules=True, id_=None, name=None, comment=None, original_str=None, named_arguments=None)

Bases: object

Represents a possibly negated atomic statement, e.g. p(a, 17, b).

SORT_RANK = 5
argument_names()

Return names of all arguments. Ignores named_arguments.

arguments
comment
complement()

Copies SELF and inverts is_negated.

classmethod create_from_iter(list)

Create Literal from list.

LIST is a python list representing an atom, e.g. [‘p’, 17, “string”, 3.14]. Returns the corresponding Literal.

classmethod create_from_table_tuple(table, tuple)

Create Literal from table and tuple.

TABLE is a string tablename. TUPLE is a python list representing a row, e.g. [17, “string”, 3.14]. Returns the corresponding Literal.

drop_theory()

Destructively sets the theory to None.

drop_update()
eliminate_column_references_and_pad_positional(theories, default_theory=None, index=0, prefix=”)

Expand column references to positional args and pad positional args.

Expand column references to traditional datalog positional args. Also pad positional args if too few are provided. Returns a new literal. If no column reference, unless no schema found for the table.

id
invert_update()
is_atom()
is_builtin(check_arguments=True)
is_ground()

Return True if all args are non-vars. Ignores named_arguments.

is_negated()
is_rule()
is_update()
location
make_positive()

Return handle to self or copy of self based on positive check.

Either returns SELF if is_negated() is false or returns copy of SELF where is_negated() is set to false.

make_update(is_insert=True)
name
named_arguments
negated
original_str
plug(binding, caller=None)

Assumes domain of BINDING is Terms. Ignores named_arguments.

pretty_str()
set_comment(comment)
set_id(id)
set_name(name)
set_original_str(original_str)
table
tablename(default_service=None)
theory_name()
variable_names()

Return variable names in arguments. Ignores named_arguments.

variables()

Return variables in arguments. Ignores named_arguments.

class congress.datalog.compile.ObjectConstant(name, type, location=None)

Bases: congress.datalog.compile.Term

Represents a term with a fixed value.

FLOAT = ‘FLOAT’
INTEGER = ‘INTEGER’
SORT_RANK = 2
STRING = ‘STRING’
is_object()
is_variable()
location
name
type
class congress.datalog.compile.Rule(head, body, location=None, id=None, name=None, comment=None, original_str=None)

Bases: object

Represents a rule, e.g. p(x) :- q(x).

SORT_RANK = 6
body
comment
drop_theory()

Destructively sets the theory to None in all heads.

drop_update()
eliminate_column_references_and_pad_positional(theories, default_theory=None)

Return version of SELF /w col refs removed and pos args padded.

All column references removed. Positional args padded up to required length. Throws exception if RULE is inconsistent with schemas.

head
heads
id
invert_update()
is_atom()
is_rule()
is_update()
location
make_update(is_insert=True)
name
original_str
plug(binding, caller=None)
plug_body(binding, caller=None)
plug_heads(binding, caller=None)
pretty_str()
set_comment(comment)
set_id(id)
set_name(name)
set_original_str(original_str)
tablename(theory=None)
tablenames(theory=None, body_only=False, include_builtin=False, include_modal=True)

Return all the tablenames occurring in this rule.

theory_name()
variable_names()
variables()
class congress.datalog.compile.RuleDependencyGraph(formulas=None, theory=None, include_atoms=True, select_head=None, select_body=None, head_to_body=True)

Bases: congress.datalog.utility.BagGraph

A Graph representing the table dependencies of rules.

Creates a Graph that includes one node for each table and an edge <u,v> if there is some rule with u in the head and v in the body. THEORY is the name of the theory to be used for any literal whose theory is None. INCLUDE_ATOMS is a boolean controlling whether atoms should contribute to nodes. SELECT_HEAD is a function that returns True for those head literals that should be included in the graph. SELECT_BODY is a function that returns True for those body literals that should be included in the graph. HEAD_TO_BODY controls whether edges are oriented from the tables in the head toward the tables in the body, or vice versa.

find_definitions(tables)
find_dependencies(tables)
formula_delete(formula, theory=None, include_atoms=True, select_head=None, select_body=None)

Delete rows/edges for the given FORMULA.

formula_insert(formula, theory=None, include_atoms=True, select_head=None, select_body=None)

Insert rows/edges for the given FORMULA.

formula_nodes_edges(formula, theory=None, include_atoms=True, select_head=None, select_body=None)

Compute dependency graph nodes and edges for FORMULA.

Returns (NODES, EDGES, MODALS), where NODES/EDGES are sets and MODALS is a ModalIndex. Each EDGE is a tuple of the form (source, destination, label).

formula_update(events, include_atoms=True, select_head=None, select_body=None)

Modify graph with inserts/deletes in EVENTS.

Returns list of changes.

table_delete(table)
tables()
tables_with_modal(modal)
undo_changes(changes)

Reverse the given changes.

Each change is either (‘node’, <node>, <is-insert>) or (‘edge’, <src_node>, <dst_node>, <label>, <is_insert>) or (‘modal’, <modal-index>, <is-insert>).

class congress.datalog.compile.Schema(dictionary=None, complete=False)

Bases: object

Meta-data about a collection of tables.

arity(tablename)

Returns the number of columns for the given TABLENAME.

Return None if TABLENAME is unknown.

classmethod col(cols)
column_name(tablename, column)

Returns name for given COLUMN or None if it is unknown.

column_number(tablename, column)

Returns the 0-indexed position of the given COLUMN for TABLENAME.

Returns None if TABLENAME or COLUMNNAME are unknown. Returns COLUMN if it is a number.

columns(tablename)

Returns the list of column names for the given TABLENAME.

Return None if the tablename’s columns are unknown.

revert(change)

Revert change made by update.

Return None

update(item, is_insert)

Returns the schema change of this update.

Return schema change.

class congress.datalog.compile.Tablename(table=None, service=None, modal=None)

Bases: object

SORT_RANK = 4
classmethod build_service_table(service, table)

Return string service:table.

classmethod create_from_tablename(tablename, service=None, use_modules=True)
drop_service()
drop_update()

Drop the update.

If end of table name is + or -, return a copy without the sign. If table name does not end in + or -, make no copy.

global_tablename(prefix=None)
invert_update()

Invert the update.

If end of table name is + or -, return a copy after switching the copy’s sign. Does not make a copy if table name does not end in + or -.

is_update()
make_update(is_insert=True)

Turn the tablename into a +/- update.

matches(service, table, modal)
modal
name(default_service=None)

Compute string name with default service.

classmethod parse_service_table(tablename)

Given tablename returns (service, name).

same(other, default_service)

Equality but where default_service is used for None service.

service
table
class congress.datalog.compile.Term

Bases: object

Represents the union of Variable and ObjectConstant.

Should only be instantiated via factory method.

static create_from_python(value, force_var=False)

Create Variable or ObjectConstants.

To create variable, FORCE_VAR needs to be true. There is currently no way to avoid this since variables are strings.

class congress.datalog.compile.Variable(name, location=None)

Bases: congress.datalog.compile.Term

Represents a term without a fixed value.

SORT_RANK = 1
is_object()
is_variable()
location
name
congress.datalog.compile.check_schema_consistency(item, theories, theory=None)
congress.datalog.compile.fact_errors(atom, theories=None, theory=None)

Checks if ATOM has any errors.

THEORIES is a dictionary mapping a theory name to a theory object.

congress.datalog.compile.fact_has_no_theory(atom)

Checks that ATOM has an empty theory. Returns exceptions.

congress.datalog.compile.find_subpolicy(rules, required_tables, prohibited_tables, output_tables)

Return a subset of rules pertinent to the parameters.

:param rules is the collection of Datalog rules to analyze :param required_tables is the set of tablenames that a rule must depend on. :param prohibited_tables is the set of tablenames that a rule must

NOT depend on.

:param output_tables is the set of tablenames that all rules must support.

Table R depends on table T if T occurs in the body of a rule with R in the head, or T occurs in the body of a rule where R depends on the table in the head of that rule.

The subset of RULES chosen has several properties: i) if a chosen rule has table R in the head, then one of @output_tables

depends on R
  1. if a chosen rule has R in the head, then R does not depend on any of @prohibited_tables
  2. if a chosen rule has R in the head, then R depends on at least one of @required_tables.
congress.datalog.compile.formulas_to_string(formulas)

Convert formulas to string.

Takes an iterable of compiler sentence objects and returns a string representing that iterable, which the compiler will parse into the original iterable.

congress.datalog.compile.get_compiler(args, theories=None, use_modules=True)

Run compiler as per ARGS and return the compiler object.

congress.datalog.compile.is_atom(x)

Returns True if object X is an atomic Datalog formula.

congress.datalog.compile.is_atom_like(x)
congress.datalog.compile.is_atom_rule(x)
congress.datalog.compile.is_datalog(x)

Returns True if X is an atom or a rule with one head.

congress.datalog.compile.is_extended_datalog(x)

Returns True if X is a valid datalog sentence.

Allows X to be a multi_rule in addition to IS_DATALOG().

congress.datalog.compile.is_literal(x)

Check if x is Literal.

Returns True if X is a possibly negated atomic Datalog formula and one that if replaced by an ATOM syntactically be replaced by an ATOM.

congress.datalog.compile.is_literal_like(x)
congress.datalog.compile.is_literal_rule(x)
congress.datalog.compile.is_multi_rule(x)

Returns True if X is a rule with multiple heads.

congress.datalog.compile.is_recursive(x)

Check for recursive.

X can be either a Graph or a list of rules. Returns T iff the list of rules RULES has a table defined in Terms of itself.

congress.datalog.compile.is_regular_rule(x)

Returns True if X is a rule with a single head.

congress.datalog.compile.is_result(x)

Check if x is result representation.

Returns T iff x is a formula or tablename representing the result of an action invocation.

congress.datalog.compile.is_rule(x)

Returns True if x is a rule.

congress.datalog.compile.is_stratified(rules)

Check if rules are stratified.

Returns T iff the list of rules RULES has no table defined in terms of its negated self.

congress.datalog.compile.is_update(x)

Returns T iff x is a formula or tablename representing an update.

congress.datalog.compile.keywords_safety(lit)
congress.datalog.compile.literal_schema(literal, theories, default_theory=None, theory_assertion=None)

Return the schema that applies to LITERAL or None.

:param LITERAL is a Literal for which we want the schema :param THEORIES is a dictionary mapping the name of the theory

to the theory object
:param DEFAULT_THEORY is the theory to use if no theory is
recorded as part of LITERAL
Returns:the schema that applies to LITERAL or None
congress.datalog.compile.literal_schema_consistency(literal, theories, theory=None)

Returns list of errors, but does no checking if column references.

congress.datalog.compile.literal_theory(literal, theories, default_theory=None)

Return the theory that applies to LITERAL or None.

:param LITERAL is a Literal for which we want the schema :param THEORIES is a dictionary mapping the name of the theory

to the theory object
:param DEFAULT_THEORY is the theory to use if no theory is
recorded as part of LITERAL
Returns:the theory that applies to LITERAL or None
congress.datalog.compile.parse(policy_string, theories=None, use_modules=True)

Run compiler on policy string and return the parsed formulas.

congress.datalog.compile.parse1(policy_string, theories=None, use_modules=True)

Run compiler on policy string and return 1st parsed formula.

congress.datalog.compile.parse_file(filename, theories=None)

Compile the file.

Run compiler on policy stored in FILENAME and return the parsed formulas.

congress.datalog.compile.print_antlr(tree)

Print an antlr Tree.

congress.datalog.compile.print_tree(tree, text, kids, ind=0)

Helper function for printing.

Print out TREE using function TEXT to extract node description and function KIDS to compute the children of a given node. IND is a number representing the indentation level.

congress.datalog.compile.reorder_for_safety(rule)

Reorder the rule.

Moves builtins/negative literals so that when left-to-right evaluation is performed all of a builtin’s inputs are bound by the time that builtin is evaluated. Reordering is stable, meaning that if the rule is properly ordered, no changes are made.

congress.datalog.compile.rule_body_safety(rule)

Check rule body for safety.

Checks if every variable in a negative literal also appears in a positive literal in the body. Checks if every variable in a builtin input appears in the body. Returns list of exceptions.

congress.datalog.compile.rule_errors(rule, theories=None, theory=None)

Returns list of errors for RULE.

congress.datalog.compile.rule_head_has_no_theory(rule, permit_head=None)

Checks if head of rule has None for theory. Returns exceptions.

PERMIT_HEAD is a function that takes a literal as argument and returns True if the literal is allowed to have a theory in the head.

congress.datalog.compile.rule_head_safety(rule)

Checks if every variable in the head of RULE is also in the body.

Returns list of exceptions.

congress.datalog.compile.rule_modal_safety(rule)

Check if the rule obeys the restrictions on modals.

congress.datalog.compile.rule_schema_consistency(rule, theories, theory=None)

Returns list of problems with rule’s schema.

congress.datalog.compile.schema_consistency(thing, theories, theory=None)
congress.datalog.compile.stratification(rules)

Stratify the rules.

Returns a dictionary from table names to an integer representing the strata to which the table is assigned or None if the rules are not stratified.

congress.datalog.compile.string_is_servicename(name)

Returns True if @name can be a servicename in the policy language.