diff --git a/resolution.py b/resolution.py index 3a7c79c..a755c17 100644 --- a/resolution.py +++ b/resolution.py @@ -1,6 +1,8 @@ from emis_funky_funktions import * -from ir import IRNeg, IRProp, IRTerm, IRVar, Substitutions, unify, unify_clauses +from itertools import product + +from ir import Clause, IRNeg, IRProp, IRTerm, IRVar, Substitutions, sub_all, unify, unify_clauses def terms_cancel(t1: IRTerm, t2: IRTerm) -> Option[Substitutions]: """ @@ -27,6 +29,52 @@ def terms_cancel(t1: IRTerm, t2: IRTerm) -> Option[Substitutions]: return hush(unify(x, IRNeg(a))) return None +def merge_clauses(c1: Clause, c2: Clause) -> Sequence[Clause]: + """ + Produce a list of all possible clauses which resolution could derive from c1 and c2 + + For each term in c1 that could cancel with a term in c2 using a substitution, a + possible clause is produced equal to the concatenation of c1 and c2 with the canceled + terms removed and the substitution applied. + + >>> merge_clauses( + ... [ IRProp('day'), IRNeg(IRProp('night')) ], + ... [ IRProp('night') ] + ... ) + [[day()]] + + >>> merge_clauses( + ... [ IRNeg(IRProp('transgender', [IRVar('x1')])), IRProp('powerful', [IRVar('x1')]) ], + ... [ IRNeg(IRProp('powerful', [IRVar('x2')])), IRProp('god', [IRVar('x2')]) ] + ... ) + [[¬transgender(*x1), god(*x1)]] + + >>> merge_clauses( + ... [ IRNeg(IRProp('day')), IRProp('night') ], + ... [ IRVar('x2') ] + ... ) + [[night()], [¬day()]] + + If two clauses cannot merge, an empty list is returned + + >>> merge_clauses( + ... [ IRProp('day') ], + ... [ IRProp('wet') ] + ... ) + [] + """ + valid_substitutions = drop_none( + map_opt(lambda subs: (subs, i1, i2), terms_cancel(t1, t2)) + for ((i1, t1), (i2, t2)) in product(enumerate(c1), enumerate(c2)) + ) + return [ + [ + sub_all(subs, term) + for term in (*c1[:i1], *c1[i1 + 1:], *c2[:i2], *c2[i2 + 1:]) + ] + for (subs, i1, i2) in valid_substitutions + ] + if __name__ == '__main__': import doctest doctest.testmod() \ No newline at end of file