a;b.
c;d:-a.
e;f:-b.

% Là on est dans le code ASP
#script (python)
# et paf, on est en python maintenant !

from time import sleep  # pour donner une dimension humaine au programme

# La classe qui contient les méthodes.
# Notez qu'il n'y a évidemment aucune contrainte sur le nom,
# et surtout que la classe n'hérite de rien. Duck Typing FTW.
class Propagator:

    # Première méthode : init
    #  (sans les `__`, car il s'agit bien de l'init du propagateur, pas de l'objet)
    def init(self, init):
        # init: un objet qui va nous donner des infos sur le solving
        for atom in init.symbolic_atoms:  # pour chacun des atomes du programme
            init.add_watch(init.solver_literal(atom.literal))  # on le surveille
            # atom.literal: la version littérale de l'atome, unique
            #               (contrairement aux littéraux du solveur).
            # init.solver_literal: donne pour un littéral d'atome le littéral
            #                      que le solveur utilise pour le référencer.
            # init.add_watch: méthode qui permet d'ajouter un littéral à surveiller.

    def propagate(self, ctl, changes):
        # ctl: c'est le contrôleur du solving ; un objet qui mériterait
        #      une section à lui tout seul.
        # changes: la liste des littéraux qui ont eu une assignation ;
        #          c'est eux qui nous intéressent.
        for _ in changes:  # la valeur exacte ne nous intéresse pas
            print('.', flush=True, end='')  # afficher un `.` sans passer à la ligne
            sleep(0.1)  # sans ça, on va rien voir, le programme semblera immédiat
        # À essayer de votre côté : afficher changes à la place des points.
        # Ça permet de voir en quoi consiste le backtrack.

    def undo(self, solver_id, assign, undo):
        # undo contient la liste des littéraux dont l'assignation est annulée.
        # on va donc enlever un '.' pour chacune de ces assignation.
        for _ in undo:  # la valeur exacte ne nous intéresse pas
            # D'abord, revenir en arrière avec \b,
            #  puis afficher un espace (effacer le point déjà affiché),
            #  puis revenir en arrière.
            print('\b \b', flush=True, end='')
            sleep(0.1)  # sans ça, vous n'allez rien voir, le programme semblera immédiat

# notez que la function main est une convention de l'API de clingo :
#  si elle existe, elle reçoit le contrôleur du solveur, et nous
#  permet donc de contrôler tout le processus de solving.
def main(prg):
    # prg: un contrôleur du solveur.
    # d'abord, on enregistre une instance de notre propagateur
    prg.register_propagator(Propagator())
    # on ground le programme 'base', qui est le programme par défaut
    prg.ground([("base", [])])
    # on lance le solving
    prg.solve()
    print()  # on écrit une ligne vide après les '.'

#end.

#script (python)

# de nombreux imports sont nécessaires
import os  # pour nettoyer l'écran
import shutil  # pour avoir la taille du terminal
import textwrap  # pour afficher joliement les atomes
from time import sleep  # pour que ça aille pas trop vite

import colorama  # des couleurs dans le terminal ! (pip install colorama)
from colorama import Fore, Back
colorama.init()  # nécessaire pour windows


# quelques constantes utiles
SPEED = 0.5
TERM_WIDTH = shutil.get_terminal_size().columns
def clear(): os.system('cls' if os.name == 'nt' else 'clear')  # oui, c'est sale


# ça, ça va être notre classe propagateur. Notez que pour éviter de dupliquer
#  du code, on a écrit une méthode `print_atoms` qui s'occupe
#  d'afficher les atomes en couleur.
class ColorPropagator:
    # appelée une fois au début: on va dire qu'on va observer tous les atomes du programme
    def init(self, init):
        self.sleep = SPEED
        # On fait un dictionnaire pour se souvenir de la tête qu'à un atome,
        #  connaissant le littéral.
        # Notez que les atomes qui sont soumis aux exactes même règles
        #  (et donc qui sont vrais ou faux en même temps) ont le même litéral.
        # C'est pourquoi à un littéral (clef) on associe plusieurs valeurs
        #   (set d'atomes).
        self.__symbols = {}  # litéral du solveur -> set d'atomes
        for atom in init.symbolic_atoms:
            lit = init.solver_literal(atom.literal)  # on récupère le litéral
            init.add_watch(lit)  # on veut être prévenu lorsque sa valeur de vérité change
            if lit in self.__symbols:  # on l'ajoute au dictionnaire
                self.__symbols[lit].add(atom.symbol)
            else:
                self.__symbols[lit] = {atom.symbol}

    # la fonction appelée quand un litéral surveillé change de valeur.
    def propagate(self, ctl, changes):
        # ctl: le contrôleur
        # changes: la liste des litéraux qui ont changé de valeur
        # C'est assez simple: on dit à print_atoms d'afficher tout ça
        self.print_atoms(ctl.assignment, changes=changes)

    def undo(self, solver_id, assign, undo):
        # c'est globalement la même chose que propagate, juste avec un argument
        #  en plus qu'on utilise pas: solver_id.
        self.print_atoms(assign, changes=undo)

    # La fonction la plus complexe, qui n'a rien à voir avec les propagateurs
    #  en général.
    def print_atoms(self, assignment, changes):
        # assignment: objet qui peut donner pour chaque 
        clear()  # on nettoie l'écran
        to_print = ''
        # là, on boucle sur chaque littéral et atomes associés
        for idx, (lit, atoms) in enumerate(self.__symbols.items(), start=1):
            # quand un litéral est associé à plusieurs atomes,
            #  on les affiche tous, séparés par un point-virgule
            atom = ';'.join(map(str, atoms))
            fore, back = Fore.WHITE, Back.BLACK  # couleurs par défaut
            # assignment.value renvoie, pour un littéral donné:
            #  - True si le littéral est vrai
            #  - False si le littéral est faux
            #  - None si le littéral n'a pas de valeur de vérité
            if assignment.value(lit) is not None:  # donc, là, il a une valeur de vérité
                # s'il est vrai, on le met en vert (GREEN), sinon en rouge (RED)
                fore = Fore.GREEN if assignment.is_true(lit) else Fore.RED
                # si l'atome vient justement d'être changé, on le surligne en blanc
                if lit in changes: back = Back.WHITE
            elif lit in changes:  # C'est un undo
                # Effectivement, undo veut dire «enlever sa valeur de vérité à un atome»,
                #  donc, il ne passe pas la première condition. Mais il fait
                #  bien partie des atomes changé, donc on va le surligner aussi,
                #  mais en en bleu pour montrer que c'est un backtrack.
                back = Back.BLUE
            else:  # et sinon, il n'a pas de valeur et n'a pas été changé
                # on le laisse en couleur par défaut
                pass
            # maintenant on se prépare à l'afficher avec les couleurs sélectionnées
            to_print += fore + back + atom + Fore.RESET + Back.RESET + '  '
        # boucle terminée: on a généré toute la chaîne à afficher.
        #  pour rendre ça beau, on utilise textwrap et la taille de l'écran
        #  pour découper proprement les lignes.
        print('\n\n' + '\n'.join(textwrap.wrap(to_print, width=TERM_WIDTH)))
        # et on attend un poil, sinon on va rien voir.
        sleep(self.sleep)


# Et voilà notre main, qui ressemble à un main des plus standards.
#  Pas grand chose à dire dessus.
def main(prg):
    prg.register_propagator(ColorPropagator())  # on y met notre propagateur
    prg.ground([("base", [])])  # on grounde le programme de base
    prg.solve()  # et on résoud le problème !

# fin du python:
#end.

#script(python)
class DotPropagator:
    """A non-literal *dot* propagator"""

    # Cette fois-ci, notre classe est un poil plus complexe.
    #  Elle a un __init__, qu'on utilise pour préparer les conteneurs et le fichier dot
    def __init__(self, dotfiledesc:str):
        # dotfiledesc -- un descripteur de fichier dans lequel on peut écrire
        self.__dotfiledesc = dotfiledesc
        self.__stack = ['Start']  # c'est une pile de nœuds
        self.__step = 0  # pour pouvoir annoter les arcs
        self.__stable_nodes = set()  # tous les nœuds stables
        self.write_header()  # on commence par écrire des lignes obligatoires
        # C'est bon ! l'objet est prêt à faire propagateur !

    def init(self, init):
        # exactement comme pour notre premier propagateur: on suit tous les atomes
        self.__symbols = {}  # littéral -> set d'atomes
        for atom in init.symbolic_atoms:
            lit = init.solver_literal(atom.literal)
            init.add_watch(lit)
            if lit in self.__symbols:  # on l'ajoute au dictionnaire
                self.__symbols[lit].add(atom.symbol)
            else:
                self.__symbols[lit] = {atom.symbol}

    def propagate(self, ctl, changes):
        # ctl: l'objet de contrôle du solveur
        # changes: les littéraux qui ont reçu une valeur
        level = ctl.assignment.decision_level
        self.__step += 1
        # pour chaque changement, on va écrire dans le fichiers dot.
        for lit in changes:
            self.write('\t{} -> {} [label="{}"];'.format(self.last_node, lit, self.__step))
            self.push_node(lit)  # et on ajoute le litéral dans la pile

    def undo(self, sid, assign, undo):
        # sid: on s'en fiche
        # assign: ce sont les assignations de valeurs de vérité, on s'en fiche aussi
        # undo: les litéraux qui ont été changés
        template = '\t{} -> {} [style=dotted label={}];'
        while undo:  # tant qu'il y a un nœud dans les undo
            prev_node = self.pull_node()  # on récupère le sommet de la pile
            assert prev_node in undo  # par construction, il appartient aux nœuds retirés
            # On affiche le backtrack en dot avec une flèche en pointillé
            #  qui retourne sur le nœud actuel (la tête de pile).
            self.write(template.format(prev_node, self.last_node, self.__step))
            undo.remove(prev_node)  # on enlève le littéral de la liste des undo

    def check(self, ctl):
        # Le solveur trouve que l'assignation est totale et valide :
        #  il s'apprête à générer l'answer set !
        # Que faisons-nous ? On marque le nœud courant comme tel.
        self.__stable_nodes.add(self.last_node)


    # Méthodes pour modifier le nœud courant (le sommet de la pile)
    def pull_node(self):  # le nœud courant devient le précédent
        *self.__stack, ret = self.__stack
        return ret
    def push_node(self, uid):  # nouveau nœud courant !
        self.__stack.append(uid)

    @property
    def last_node(self):  # juste un raccourcis pour le nœud courant
        return self.__stack[-1]

    def write(self, line):  # pour écrire du dot
        self.__dotfiledesc.write(line.rstrip() + '\n')

    def write_nodes(self):  # pour écrire les nœuds
        for uid, atoms in self.__symbols.items():
            self.write('\t{} [label="{}"{}];'.format(
                uid, ' '.join(str(atom) for atom in atoms),
                ' fillcolor="green"' if uid in self.__stable_nodes else ''
            ))

    # Deux méthodes pour les premières et dernières lignes du dot,
    #  qui sont toujours les mêmes.
    def write_header(self):
        self.write('digraph solving {')
        self.write('\tgraph [dpi=400];')  # bonne résolution
        self.write('\tnode [style=filled];')  # affiche la couleurs de fond
        self.write('\tedge [arrowsize=0.5];')  # flèche plus petites
    def finalize(self):
        self.write_nodes()
        self.write('}')


# Le main est assez standard également,
#  sauf le fait que l'on fait tout le solving avec un fichier ouvert,
#  que l'on donne à notre propagateur.
def main(prg):
    with open('out.dot', 'w') as fd:
        propagator = DotPropagator(fd)  # c'est notre propagateur !
        prg.register_propagator(propagator)  # on l'enregistre
        prg.ground([("base", [])])  # on ground
        prg.solve()  # on solve
        propagator.finalize()  # et on termine d'écrire le dot
#end.

a;b.
c;d:-a.
e;f:-b.

#script(python)

from clyngor import Constraint, Variable as V, Main

# On définit la contrainte
def formula(inputs):
    # inputs: c'est un dictionnaire qui mappe un atome avec sa valeur de vérité (True/False)
    # on retourne si oui ou non on écarte le modèle.
    # ici, si le modèle contient b(2), on l'écarte
    return inputs[('b', (2,))]

# On l'encapsule dans l'objet dédié, qui est en fait un propagateur
constraint = Constraint(formula, {('b', (V,))})

# On lance le grounding et le solving, avec le propagateur enregistré
main = Main(constraint)

#end.

b(1);b(2);b(3).  % choisi l'un des trois

Answer 1:
b(1)
Answer 2:
b(3)

#script(python)
from collections import defaultdict
Variable = ...  # Ellipsis en Python


# La fonction qui suit sert à transformer un argument d'atome,
#  sous la forme d'une instance de la classe clingo.Symbol,
# en objet purement python (listes, tuples, int,…).
# Cette fonction est en réalité plus complexe,
#  car elle doit gérer les structures récursives,
#  les types non standards de clingo (comme #inf et #sup),
#  et les double quotes dans les strings.
# le code complet est ici :
#  https://github.com/Aluriak/clyngor/blob/impl/propagator/clyngor/utils.py#L56
def clingo_value_to_python(obj:int or str or 'Symbol'):
    if isinstance(obj, (int, str)):
        return obj
    if type(obj).__name__ == 'Symbol':
        typename = str(obj.type).lower()
        if typename == 'string':
            return '"' + obj.replace('"', '\\"') + '"'
        if typename == 'number':
            return int(str(obj))
    raise TypeError("Can't handle values like {} of type {}."
                    "".format(obj, type(obj)))

# La classe qui implémente le comportement complet
class Constraint:

    # Le constructeur de la classe : on prend une formule
    #  et les atomes qui doivent être suivis.
    def __init__(self, formula:callable, inputs:[tuple]):
        self.__formula = formula
        # les inputs peuvent être données de différentes manières :
        #  - comme des strings, e.g. 'a(2,3)'
        #  - comme des tuple, e.g. ('a', (2, 3))
        # la seconde est plus lourde, mais n'oblige pas de donner
        #  les valeurs exactes des arguments, e.g. ('a', (V, 3))
        self.__inputs = frozenset(inputs)
        # on sauvegarde donc les versions string et tuple à part
        self.__str_inputs = frozenset(input for input in self.__inputs
                                      if isinstance(input, str))
        self.__raw_inputs = frozenset(input for input in self.__inputs
                                      if not isinstance(input, str))


    # la fonction de propagateur d'initialisation
    def init(self, init):
        # on a un dictionnaire qui nous permet de connaître, pour un littéral de solveur,
        #  l'atome dans sa version string ou tuple.
        self.__symbols = defaultdict(set)
        # pour chacun des atomes, il faut décider si on veux le suivre ou pas
        #  (en se basant sur les inputs récupéré dans le constructeur)
        for atom in init.symbolic_atoms:
            lit = init.solver_literal(atom.literal)
            # d'abord on teste l'atome lorsque représenté comme une string
            repr_str = str(atom.symbol)
            if self._match_str(repr_str):  # vrai si repr_str est attendu par la formule
                init.add_watch(lit)
                self.__symbols[lit].add(repr_str)
                continue
            # et ensuite, on le teste sous le format raw
            repr_args = tuple(map(clingo_value_to_python, atom.symbol.arguments))
            repr_raw = atom.symbol.name, repr_args
            if self._match_raw(*repr_raw):  # idem que self._match_str, mais avec Variable
                init.add_watch(lit)
                self.__symbols[lit].add(repr_raw)


    # fonction appelée quand une propagation est réalisée
    def propagate(self, ctl, changes):
        # on appelle la formule donnée par l'utilisateur, avec en argument un dictionnaire
        #  qui mappe la représentation d'un atome et sa valeur de vérité.
        fulfilled = self.__formula({
            repr: ctl.assignment.value(lit)
            for lit, reprs in self.__symbols.items()
            for repr in reprs  # plusieurs atomes peuvent avoir la même valeur de littéral
        })
        # si la contrainte est remplie, on invalide le modèle
        if fulfilled:
            self.__invalidate_model(ctl)

    def __invalidate_model(self, ctl):
        # On ajoute, si c'est pas encore fait, un nouveau littéral.
        # C'est un peu comme si on ajoutait un atome,
        #  mais sans lui donner de représentation comme a(2) par exemple.
        self.__added_lit = ctl.add_literal()
        # Les deux lignes suivantes servent à ajouter une «clause»,
        #  indiquant que notre nouveau littéral est vrai.
        # Quand on ajoute une clause, il se peut que le solveur
        #  ait besoin de revérifier l'espace de recherche.
        # Dans notre cas, on ne le change pas puisque le littéral assigné est tout nouveau
        #  et est indépendant du programme ASP.
        # Mais dans le cas général, on pourrait assigner la valeur d'un atome existant,
        #  et donc là le solveur devrait réagir en conséquence.
        if not ctl.add_clause([self.__added_lit]) or not ctl.propagate():
            return
        # C'est là que la magie se passe : on dit que le littéral est faux.
        if not ctl.add_nogood([self.__added_lit]) or not ctl.propagate():
            return
        # Ce qui entre en conflit avec la clause précédente, qui le déclarait vrai.
        # La situation est donc instable,
        #  aucun modèle ne pourra être vrai dans ces conditions !


    # Les fonctions suivantes sont des détails d'implémentation,
    #  et n'ont pas grand chose à voir avec les propagateurs,
    #  mais je les laisse là pour la complétude du code.

    def _match_str(self, atom:str) -> bool:
        # Retourne vrai si l'atome en string donné
        #  est dans les inputs attendues par la formule.
        if atom in self.__str_inputs:
            return True

    def _match_raw(self, name:str, args:tuple) -> bool:
        # Retourne vrai si l'atome en tuple donné
        #  est dans les inputs attendues par la formule.
        # Premier cas : pas de Variable dans le tuple.
        if (name, args) in self.__raw_inputs:
            return True
        # Second cas : il y a des Variable dans le tuple.
        for pred, params in self.__raw_inputs:
            if pred == name and len(args) == len(params):
                # C'est le même prédicat et le même nombre de variable
                #  donc c'est peut-être bon…
                for arg, param in zip(args, params):
                    # Deux cas : soit l'argument est une Variable,
                    #  soit c'est celui attendu.
                    if param is Variable or arg == param:
                        return True


# On implémente la contrainte
def formula(inputs):
    # c'est équivalent à `:- b(2).`
    return inputs[('b', (2,))]

# On lance le grounding et le solving, avec le propagateur enregistré
def main(prg):
    constraint = Constraint(formula, {('b', (Variable,))})
    prg.register_propagator(constraint)
    prg.ground([("base", [])])
    prg.solve()

#end.

% un code ASP qui génère 1 parmi b(1..3).
1{b(X): X=1..3}1.