congress.datalog.topdown module¶

class congress.datalog.topdown.TopDownTheory(name=None, abbr=None, theories=None, schema=None, desc=None, owner=None)¶

Bases: congress.datalog.base.Theory

Class that holds the Top-Down evaluation routines.

Classes will inherit from this class if they want to import and specialize those routines.

class TopDownCaller(variables, binding, theory, find_all=True, save=None)¶

Bases: object

Struct for info about the original caller of top-down evaluation.

VARIABLES is the list of variables (from the initial query) that we want bindings for.

BINDING is the initially empty BiUnifier.

FIND_ALL controls whether just the first or all answers are found.

ANSWERS is populated by top-down evaluation: it is the list of VARIABLES instances that the search process proved true.

class TopDownContext(literals, literal_index, binding, context, theory, depth)¶

Bases: object

Struct for storing the search state of top-down evaluation.

class TopDownResult(binding, support)¶

Bases: object

Stores a single result for top-down-evaluation.

abduce(query, tablenames, find_all=True)¶

Compute additional literals.

Computes additional literals that if true would make (some instance of) QUERY true. Returns a list of rules where the head represents an instance of the QUERY and the body is the collection of literals that must be true in order to make that instance true. If QUERY is a rule, each result is an instance of the head of that rule, and the computed literals if true make the body of that rule (and hence the head) true. If FIND_ALL is true, the return list has at most one element. Limitation: every negative literal relevant to a proof of QUERY is unconditionally true, i.e. no literals are saved when proving a negative literal is true.

bi_unify(head, unifier1, body_element, unifier2, theoryname)¶

Unify atoms.

Given something returned by self.head HEAD and an element in the return of self.body BODY_ELEMENT, modify UNIFIER1 and UNIFIER2 so that HEAD.plug(UNIFIER1) == BODY_ELEMENT.plug(UNIFIER2). Returns changes that can be undone via unify.undo-all. THEORYNAME is the name of the theory for HEAD.

body(formula)¶

Return formula body.

Given a FORMULA, return a list of things to push onto the top-down eval stack.

consequences(filter=None, table_theories=None)¶

Return all the true instances of any table in this theory.

defined_tablenames()¶

Returns list of table names defined in/written to this theory.

explain(query, tablenames, find_all=True)¶

Return list of instances of QUERY that are true.

Same as select except stores instances of TABLENAMES that participated in each proof. If QUERY is an atom, returns list of rules with QUERY in the head and the stored instances of TABLENAMES in the body; if QUERY is a rule, the rules returned have QUERY’s head in the head and the stored instances of TABLENAMES in the body.

head(formula)¶

Given the output from head_index(), return the formula head.

Given a FORMULA, return the thing to unify against. Usually, FORMULA is a compile.Rule, but it could be anything returned by HEAD_INDEX.

head_index(table, match_literal=None)¶

Return head index.

This routine must return all the formulas pertinent for top-down evaluation when a literal with TABLE is at the top of the stack.

instances(rule, possibilities=None)¶

classmethod new_bi_unifier(dictionary=None)¶

Return a unifier compatible with unify.bi_unify.

select(query, find_all=True)¶

Return list of instances of QUERY that are true.

If FIND_ALL is False, the return list has at most 1 element.

top_down_abduction(variables, literals, binding=None, find_all=True, save=None)¶

Compute bindings.

Compute all bindings of VARIABLES that make LITERALS true according to the theory (after applying the unifier BINDING), if we add some number of additional literals. Note: will not save any literals that are needed to prove a negated literal since the results would not make sense. Returns a list of TopDownResults.

top_down_evaluation(variables, literals, binding=None, find_all=True)¶

Compute bindings.

Compute all bindings of VARIABLES that make LITERALS true according to the theory (after applying the unifier BINDING). If FIND_ALL is False, stops after finding one such binding. Returns a list of dictionary bindings.