ClausePair.py

from copy import deepcopy


class ClausePair:
    def __init__(self, c1_set, c2_set):
        self.c1, self.c2 = frozenset(c1_set), frozenset(c2_set)

    def __eq__(self, other):
        if isinstance(other, self.__class__):
            return ((self.c1 == other.c1 and self.c2 == other.c2) or
                    (self.c1 == other.c2 and self.c2 == other.c1))
        return False

    def __hash__(self):
        return hash(frozenset((self.c1, self.c2)))


def negate(literal):
    if literal[0] == '~':
        return literal[1]
    return '~{}'.format(literal)


def would_resolve(c1, c2):
    if c1 == c2:
        return False

    for literal in c1:
        if negate(c1) in c2:
            return True
    return False


def resolve(c1, c2):
    c1, c2 = deepcopy(c1), deepcopy(c2)
    for literal in c1:
        if negate(literal) in c2:
            combined_clause = c1
            combined_clause.update(c2)
            combined_clause.remove(literal)
            combined_clause.remove(negate(literal))
            return combined_clause
    raise Exception("Could not resolve {} and {}!".format(c1, c2))