

def eq_assoccomm(u, v):
    " Associative/Commutative eq\n\n    Works like logic.core.eq but supports associative/commutative expr trees\n\n    tree-format:  (op, *args)\n    example:      (add, 1, 2, 3)\n\n    State that operations are associative or commutative with relations\n\n    >>> from logpy.assoccomm import eq_assoccomm as eq\n    >>> from logpy.assoccomm import commutative, associative\n    >>> from logpy import fact, run, var\n\n    >>> fact(commutative, 'add')    # declare that 'add' is commutative\n    >>> fact(associative, 'add')    # declare that 'add' is associative\n\n    >>> x = var()\n    >>> e1 = ('add', 1, 2, 3)\n    >>> e2 = ('add', 1, x)\n    >>> run(0, x, eq(e1, e2))\n    (('add', 2, 3), ('add', 3, 2))\n    "
    try:
        (uop, uargs) = op_args(u)
        (vop, vargs) = op_args(v)
    except ValueError:
        return (eq, u, v)
    if (uop and (not vop) and (not isvar(v))):
        return fail
    if (vop and (not uop) and (not isvar(u))):
        return fail
    if (uop and vop and (not (uop == vop))):
        return fail
    if (uop and (not ((uop,) in associative.facts))):
        return (eq, u, v)
    if (vop and (not ((vop,) in associative.facts))):
        return (eq, u, v)
    if (uop and vop):
        (u, v) = ((u, v) if (len(uargs) >= len(vargs)) else (v, u))
        n = min(map(len, (uargs, vargs)))
    else:
        n = None
    if (vop and (not uop)):
        (u, v) = (v, u)
    w = var()
    return (lall, (eq_assoc, u, w, eq_assoccomm, n), (eq_comm, v, w, eq_assoccomm))

dataset/ETHPy150Open logpy/logpy/logpy/assoccomm.py eq_assoccomm/original