clingo-hmknf-test/example.py

import clingo

PROGRAM = """
#theory o {
    kterm {- : 0, unary };
    &o/0 : kterm, any
}.

x :- &o{false}.
x :- &o{x}.
y :- &o{y}.
"""

class CheckAtoms:
    def init(self, init: clingo.PropagateInit):
        symbolic_lits = {atom: init.solver_literal(atom.literal) for atom in init.symbolic_atoms}
        theory_lits = {init.solver_literal(atom.literal) for atom in init.theory_atoms}

        overlap = tuple(atom for atom, lit in symbolic_lits.items() if lit in theory_lits)

        if len(overlap) == 0:
            print("There is no solver literal overlap")
        else:
            print("There is overlap")
            print(*(atom.symbol for atom in overlap))


control = clingo.Control(["0"])
control.register_propagator(CheckAtoms())
control.add("base", [], PROGRAM)
control.ground([("base", [])])

control.solve()