congress.datalog.unify module

class congress.datalog.unify.BiUnifier(dictionary=None)

Bases: object

A unifier designed for bi_unify_atoms.

Recursive datastructure. When adding a binding variable u to variable v, keeps a reference to the unifier for v. A variable’s identity is its name plus its unification context. This enables a variable with the same name but from two different atoms to be treated as different variables.

class Undo(var, unifier)

Bases: object

class Value(value, unifier)

Bases: object

recur_str()

add(var, value, unifier)

apply(term, caller=None)

apply_full(term, caller=None)

Recursively apply unifiers to TERM.

Return (i) the final value and (ii) the final unifier. If the final value is a variable, instantiate with a new variable if not in KEEP_VARS

delete(var)

is_one_to_one()

recur_str()

value(term)

congress.datalog.unify.bi_unify_atoms(atom1, unifier1, atom2, unifier2, theoryname=None)

Unify atoms.

If possible, modify BiUnifier UNIFIER1 and BiUnifier UNIFIER2 so that ATOM1.plug(UNIFIER1) == ATOM2.plug(UNIFIER2). Returns None if not possible; otherwise, returns a list of changes to unifiers that can be undone with undo-all. May alter unifiers besides UNIFIER1 and UNIFIER2. THEORYNAME is the default theory name.

congress.datalog.unify.bi_unify_lists(iter1, unifier1, iter2, unifier2)

Unify lists.

If possible, modify BiUnifier UNIFIER1 and BiUnifier UNIFIER2 such that iter1.plug(UNIFIER1) == iter2.plug(UNIFIER2), assuming PLUG is defined over lists. Returns None if not possible; otherwise, returns a list of changes to unifiers that can be undone with undo-all. May alter unifiers besides UNIFIER1 and UNIFIER2.

congress.datalog.unify.bi_var_equal(var1, unifier1, var2, unifier2)

Check var equality.

Returns True iff variable VAR1 in unifier UNIFIER1 is the same variable as VAR2 in UNIFIER2.

congress.datalog.unify.binding_str(binding)

Handles string conversion of either dictionary or Unifier.

congress.datalog.unify.instance(formula1, formula2)

Determine if FORMULA1 is an instance of FORMULA2.

If there is some binding that when applied to FORMULA1 results in FORMULA2. Returns None or a unifier.

congress.datalog.unify.instance_atoms(atom1, atom2, unifier2)

Check atoms equality by adding bindings.

Adds bindings to UNIFIER2 to make ATOM1 equal to ATOM2 after applying UNIFIER2 to ATOM2 only. Returns None if no such bindings make equality hold.

congress.datalog.unify.match_atoms(atom1, unifier, atom2)

Modify UNIFIER so that ATOM1.plug(UNIFIER) == ATOM2.

ATOM2 is assumed to be ground. UNIFIER is assumed to be a BiUnifier. Return the changes to UNIFIER or None if matching is impossible.

Matching is a special case of instance-checking since ATOM2 in this case must be ground, whereas there is no such limitation for instance-checking. This makes the code significantly simpler and faster.

congress.datalog.unify.match_tuple_atom(tupl, atom)

Get bindings.

Returns a binding dictionary that when applied to ATOM’s arguments gives exactly TUPLE, or returns None if no such binding exists.

congress.datalog.unify.same(formula1, formula2)

Check formulas are the same.

Determine if FORMULA1 and FORMULA2 are the same up to a variable renaming. Treats FORMULA1 and FORMULA2 as having different variable namespaces. Returns None or the pair of unifiers.

congress.datalog.unify.same_atoms(atom1, unifier1, atom2, unifier2, bound2)

Check whether atoms are identical.

Modifies UNIFIER1 and UNIFIER2 to demonstrate that ATOM1 and ATOM2 are identical up to a variable renaming. Returns None if not possible or the list of changes if it is. BOUND2 is the set of variables already bound in UNIFIER2

congress.datalog.unify.same_schema(atom1, atom2, theoryname=None)

Return True if ATOM1 and ATOM2 have the same schema.

THEORYNAME is the default theory name.

congress.datalog.unify.skolemize(formulas)

Instantiate all variables consistently with UUIDs in the formulas.

congress.datalog.unify.undo_all(changes)

Undo all the changes in CHANGES.