clorm with theory solving

[MaxOstrowski]

I tried to use clorm in conjunction with clingo-dl. This example snippet is the proposed way of loading difference logic into clingo:

from clingo import Control
from clingo.ast import parse_string, ProgramBuilder
from clingodl import ClingoDLTheory

prg = '&diff { x } >= 1. &diff { y } >= 3.'

thy = ClingoDLTheory()
ctrl = Control()
thy.register(ctrl)
with ProgramBuilder(ctrl) as bld:
    parse_string(prg, lambda ast: thy.rewrite_ast(ast, bld.add))

ctrl.ground([("base",[])])
thy.prepare(ctrl)

with ctrl.solve(yield_=True, on_model=thy.on_model) as hnd:
    for mdl in hnd:
        print([f'{key}={val}' for key, val in thy.assignment(mdl.thread_id)])

I wanted to change this now using clorm by only changing two lines, the Control import and the control constructor:

from clorm.clingo import Control
from clingo.ast import parse_string, ProgramBuilder
from clingodl import ClingoDLTheory

prg = '&diff { x } >= 1. &diff { y } >= 3.'

thy = ClingoDLTheory()
ctrl = Control(unifier=[])
thy.register(ctrl)
with ProgramBuilder(ctrl) as bld:
    parse_string(prg, lambda ast: thy.rewrite_ast(ast, bld.add))

ctrl.ground([("base",[])])
thy.prepare(ctrl)

with ctrl.solve(yield_=True, on_model=thy.on_model) as hnd:
    for mdl in hnd:
        print([f'{key}={val}' for key, val in thy.assignment(mdl.thread_id)])

But I do get the following error:

  File "test.py", line 17, in <module>                                                   
    for mdl in hnd:                                                                                                    
  File "python3.9/site-packages/clorm/clingo.py", line 202, in __iter__                                                
    for model in self.solvehandle_:                                                                                    
  File "python3.9/site-packages/clingo/solving.py", line 461, in __iter__                                              
    m = self.model()                                                                                                   
  File "python3.9/site-packages/clingo/solving.py", line 506, in model                                                 
    _handle_error(                                                                                                     
  File "python3.9/site-packages/clingo/_internal.py", line 61, in _handle_error                                        
    raise handler.error[0](handler.error[1]).with_traceback(handler.error[2])                                          
  File "python3.9/site-packages/clingo/control.py", line 83, in _pyclingo_solve_event_callback                         
    goon[0] = handler.on_model(_ffi.cast('clingo_model_t*', event))                                                    
  File "python3.9/site-packages/clingo/control.py", line 58, in on_model                                               
    ret = self._on_model(Model(m))                                                                                     
  File "python3.9/site-packages/clorm/clingo.py", line 475, in on_model_wrapper                                        
    return on_model(Model(model, self.unifier))  # type: ignore                                                        
  File "python3.9/site-packages/clingo/theory.py", line 282, in on_model                                               
    self._ffi.cast('clingo_model_t*', model._rep))                                                                     
AttributeError: 'Model' object has no attribute '_rep' 

What am I doing wrong ? Using:

clingo                    5.5.1            py39h3fd9d12_0    potassco
clingo-dl                 1.3.0            py39hda08288_0    potassco
clorm                     1.4.0.post3              pypi_0    pypi

[daveraja]

Clorm creates wrapper/proxy classes clorm.clingo.Control, clorm.clingo.Model, etc, that wrap the corresponding clingo objects. It then adds or overloads some member functions and passes through other member functions/attributes. But it only does this for the public API stuff.

However, Theory.on_model() is trying to access the internal clingo.Model._rep attribute, which doesn't exist for clorm.clingo.Model.

We could try adding a clorm.clingo.Model._rep attribute that points to the underlying clingo.Model._rep attribute. I think this would work for your example. But I'm not sure if it is a good idea since the ._rep stuff is an implementation detail and not part of the official clingo API.

BTW. As a hack you could change the solve line to:

with ctrl.solve(yield_=True, on_model=lambda m: thy.on_model(m._wrapped)) as hnd:

This relies on an internal implementation detail of clorm.clingo.Model (the ._wrapped attribute). But I would be interested to know if this is the only thing that would need to change for a typical python clingo DL application.

[MaxOstrowski]

Hi, that's exactly what I thought. This is the only change I would need to do to get this example working. The question is whether it is better to rely on clingo's internal _rep or clorm's internal _wrapped. Maybe @rkaminsk has an oppinion on it ? Maybe a m.clingo_model() is nicer than a _wrapped for this case ?

[rkaminsk]

I would not use clorm.clingo.Control. Instead, I would explicitly create a FactBase from a model when needed.

Otherwise, I don't see an harm in making _wrapped a public member in clorm. Maybe via a property to forbid changing it. This allows using the clorm.clingo.Model in a type safe manner with a clingo.theory.Theory.

[daveraja]

I've also wondered whether having clorm.clingo.Control is worth the extra complexity. When things work it only makes life a little easier, but when something breaks it makes it harder to work out what's gone wrong.

Anyway, I'm happy to add a property to access the underlying clingo object. A general name like wrapped or wrapped_ would be simplest since I would only need to change the function that generates the wrapper. We just need to make sure it is a name that doesn't appear in the attributes of Control, SolveHandle, and Model.

Separate to this it might also be worthwhile creating a clorm.clingo.ControlDL class that hides the details of importing and registering ClingoDLTheory. A corresponding clorm.clingo.ModelDL object would then provide a convenience function to access the DL assignment for that model.

[MaxOstrowski]

I do not think that a clorm.clingo.ControlDL class is necessary. The assignment can be easily accessed using mdl.facts(unifier, theory=True)