import copy
import re


class FirstOrderResolution:
    def __init__(self):

        self.variables = ['x', 'y', 'z']
        self.constants = ['a', 'b', 'c']

        self.kb_facts = set()
        self.kb_rules = list()

    def add_fact(self, fact: str):
        self.kb_facts.add(fact)

    def add_rule(self, rule: str):

        rule = re.sub(r"\s+", "", rule)
        print(rule)

        cnf = rule.split('v')
        print(cnf)

        self.kb_rules.append(cnf)
        

    def unification(self, fact: str, clause: str):
        # e.g S(a, b) and S(x,y) v T(y)
        # take each pair of same terms, and check if they are negations, check the parameters,
        #   facts have constants as parameters, while rules have variables as parameters
        #   just check if the condition's parameters are variables and if they are, replace
        #   the variables with constants 


    def resolve(self):

        for rule in self.kb_rules:
            # check each clause against each fact
            # if both of them are of same predicate, unify them and add it back to rules.
            # if that resultant rule only contains a single term, add it to facts and remove from rules

            all_clauses_satisfy = True
            for clause in rule:
                print(f"Checkin g clause {clause}")
                for f in self.kb_facts:
                    # get the predicate in the fact
                    predicate = re.findall(r'(.)\(', f)

                    if ()

                    # if clause is of same predicate as fact, unify and update the rule
            # thats it

        


    def print_kb(self):
        print("Facts")
        print(self.kb_facts)
        
        print("\nRules")
        for r in self.kb_rules:
            print(r)        


if __name__ == '__main__':
    print("First-Order Logic Resolver\n")

    prover = FirstOrderResolution()    

    #facts
    prover.add_fact("P(a)")
    prover.add_fact("Q(a,b)")
    prover.add_fact("R(b,c)")

    #rules
    prover.add_rule("~P(x) v ~Q(x,y) v S(x,y)")
    prover.add_rule("~S(x,y) v ~R(y,z) v T(x)")

    prover.print_kb()

    prover.resolve("~T(a)")