showing theory atoms

[ArdalanKhazraei]

I would like to ask how to use the theory app in order to show theory atoms which are being replaced by symbolic atoms using the ast.Transformer.

At the moment, I am adding show statements explicitly using the parse_string method, putting the subsequent symbolic atom form of the atoms in the show statement.

Specifically, I want them to show up in the smodels output of clingo. I wanted to ask if there is a more direct way without writing the statement and adding it with parse_string. For example, would showTerm be relevant?

Also, what if I were not replacing theory atoms with symbolic atoms? Would there be a relevant way to show the theory atoms in this case?

[rkaminsk]

It sounds like the backend is a good idea here. Using parse_string is not a good idea whenever you add a large number of already ground statements to the program. The grounder is not made for this. I put an example below to show some (efficient) ways to show terms:

from clingo.symbol import Function
from clingo.control import Control

ctl = Control()

sym_a = Function("a")
sym_b = Function("b")

with ctl.backend() as backend:
    atm_a = backend.add_atom(sym_a)
    backend.add_rule([atm_a])

class Context:
    def show(self):
        return sym_b

ctl.add("#show @show().")
ctl.ground(context=Context())

with ctl.solve(yield_=True) as hnd:
    for m in hnd:
        print(m)
    hnd.get()