Inférence à chaînage arrière¶

from moteur_avec_variables.proposition_avec_variables import *

class Noeud:
    """ Représentation d'un noeud. """

    def __init__(self, but, sous_but_courant, sous_buts_a_tester, profondeur):
        self.but = but
        self.sous_but_courant = sous_but_courant
        self.sous_buts_a_tester = sous_buts_a_tester
        self.profondeur = profondeur

    def est_terminal(self):
        """ Teste si le noeud courant est terminal.

            Un noeud est terminal lorsqu'il ne peut
            avoir de successeurs quels que soient les
            faits et les règles.
        """
        return len(self.sous_but_courant) == 0 and len(self.sous_buts_a_tester) == 0

    def est_solution(self):
        """ Teste si le noeud courant est une solution. """
        variables = lister_variables(self.but)
        return self.est_terminal() and len(variables) == 0

    def successeur(self, env, nouveaux_sous_buts, unificateur):
        """ Retourne un noeud successeur du noeud courant. """
        # Les sous-buts à explorer sont composés par les sous-buts
        # encore ouverts et les nouveaux sous-buts (cas d'une règle).
        sous_buts = nouveaux_sous_buts[:]
        sous_buts.extend(self.sous_buts_a_tester)

        if len(sous_buts) > 0:
            premier_sous_but = sous_buts[0]
        else:
            premier_sous_but = ()

        if len(sous_buts) > 1:
            reste_sous_buts = sous_buts[1:]
        else:
            reste_sous_buts = []

        successeur = Noeud(
                         unificateur.substitue(self.but, env),
                         unificateur.substitue(premier_sous_but, env),
                         [unificateur.substitue(sous_but, env) for sous_but in reste_sous_buts],
                         self.profondeur + 1
                        )

        return successeur

    def description_standardisee(noeud):
        """ Retourne une description du noeud sous forme de liste composée du\
            but en premier élément, puis des sous-buts triés selon l'ordre de\
            leurs propres descriptions.
        """

        sous_buts = [noeud.sous_but_courant] if len(noeud.sous_but_courant) > 0 else []
        sous_buts.extend(noeud.sous_buts_a_tester)
        sous_buts = sorted(sous_buts, key=lambda prop: prop)
        but_et_sous_buts = [noeud.but] + sous_buts

        return but_et_sous_buts

    def __repr__(self):
        return '<{},{},{},{}>'.format(self.but,
                                      self.sous_but_courant,
                                      self.sous_buts_a_tester,
                                      self.profondeur)

from moteur_sans_variables.chainage import Chainage
from .noeud import Noeud
from .noeuds_testes import NoeudsTestes

class ChainageArriere(Chainage):
    """ Un moteur d'inférence à chaînage arrière. """

    def __init__(self, connaissances, unificateur):
        self.connaissances = connaissances
        self.unificateur = unificateur

    def successeurs(self, noeud):
        """ Trouve les successeurs d'un noeud. """
        nouveaux_noeuds = []

        if noeud.est_terminal():
            return nouveaux_noeuds

        # On se limite aux faits et aux règles intéressants à examiner.
        # En effet, si le sous-but examiné commence par 'grand-pere',
        # alors il est inutile de considérer des noeuds commençant
        # par 'oncle' par exemple.
        regles_interessantes = self.connaissances.choisir_regles_interessantes(noeud.sous_but_courant, self.unificateur)
        faits_interessants = self.connaissances.choisir_faits_interessants(noeud.sous_but_courant)

        # On parcourt les règles intéressantes.
        for regle in regles_interessantes:
            # Tentative d'unification entre le sous-but sélectionné
            # et la consequence de la règle.
            env = self.unificateur.unifie(noeud.sous_but_courant,
                                          regle.conclusion)
            if env != self.unificateur.echec:
                nouveau_noeud = noeud.successeur(env,
                                                 regle.conditions,
                                                 self.unificateur)
                nouveaux_noeuds.append(nouveau_noeud)

        # On parcourt les faits intéressants.
        for fait in faits_interessants:
            # Tentative d'unification entre le sous-but sélectionné et le fait.
            env = self.unificateur.unifie(noeud.sous_but_courant, fait)
            if env != self.unificateur.echec:
                nouveau_noeud = noeud.successeur(env, [], self.unificateur)
                nouveaux_noeuds.append(nouveau_noeud)
        # Retourne les nouveaux noeuds ainsi trouvés.
        return nouveaux_noeuds

    def backchain(self, noeud_depart):
        """ Exécute l'algorithme de chaînage arrière afin de trouver les\
            faits qui peuvent s'unifier avec le pattern.
        """
        # Liste des noeuds à tester.
        queue = [noeud_depart]
        # Liste des noeuds déjà testés.
        noeuds_testes = NoeudsTestes()
        # Liste des solutions.
        self.solutions = set()

        # Tant qu'il y a des noeuds à tester dans la liste,
        while len(queue) > 0:
            # on sélectionne le noeud suivant.
            noeud = queue.pop(0)
            self.trace.append(noeud)
            # Si le noeud n'appartient pas encore à la liste des noeuds
            # déjà testés, on l'y ajoute pour éviter les cycles.
            if noeud not in noeuds_testes:
                noeuds_testes.ajoute(noeud)
                # Si le noeud est une solution, on l'ajoute à celles qu'on a
                # déjà trouvées.
                if noeud.est_solution():
                    self.solutions.add(noeud.but)
                else:
                    # On obtient des noeuds supplémentaires par chaînage arrière.
                    successeurs = self.successeurs(noeud)
                    successeurs.extend(queue)
                    queue = successeurs

        # Retourne la liste des solutions au problème.
        return self.solutions

    def chaine(self, pattern):
        """ Interroge le moteur de chaînage arrière (fonction d'interface). """

        # Retourne les solutions par chaînage arrière.
        noeud_depart = Noeud(pattern, pattern, [], 0)
        solutions = self.backchain(noeud_depart)

        return solutions