cleanup() removes theory atoms ?

[MaxOstrowski]

Given this weird looking little example program, I do get an unexpected

'std::logic_error'
what(): Unknown element '0'

during the creation of the backend

#include <clingo.hh>
#include <sstream>

using namespace Clingo;

class TestApp : public Clingo::Application, private SolveEventHandler {
public:
    void main(Control &ctl, StringSpan files) override {
                ctl.add("base",{}, R"(#theory csp {
                               dom_term {};
                               &dom/0 : dom_term, any}.)");
        ctl.add("base",{}, "&dom {0}.");

        ctl.ground({{"base", {}}});

        ctl.cleanup();
        
        auto backend = ctl.backend();
    }
};

int main(int argc, char *argv[]) {
    TestApp app;
    return Clingo::clingo_main(app, {argv + 1, static_cast<size_t>(argc - 1)});
}

[rkaminsk]

Cleanup is meant to be called after solving. It is not meant to and cannot be used for preprocessing by calling it in-between grounding calls. The program you wrote should not crash though. I actually intended it to be a noop.

Looking through this I discovered another bug. The theory is passed unnecessarily often. Even turning your cleanup() call into a noop there are strange effects:

#include <clingo.hh>  
#include <sstream>  
  
using namespace Clingo;  
  
class Observer : public Clingo::GroundProgramObserver {  
    void theory_atom(id_t atom_id_or_zero, id_t , IdSpan ) override {  
        std::cerr << "atom: " << atom_id_or_zero << std::endl;  
    }  
};  
       
class TestApp : public Clingo::Application, private SolveEventHandler {  
public:  
    void main(Control &ctl, StringSpan) override {  
        Observer o;  
        ctl.register_observer(o);      
        ctl.add("base",{}, R"(#theory csp {      
                               dom_term {};      
                               &dom/0 : dom_term, any}.)");      
        ctl.add("base",{}, "&dom {0}. &dom {1}.");      
        ctl.add("acid",{}, "&dom {1}. &dom {2}.");      
        std::cerr << "ground base" << std::endl;        
        ctl.ground({{"base", {}}});      
        std::cerr << "ground acid" << std::endl;      
        ctl.ground({{"acid", {}}});      
        ctl.cleanup();      
        std::cerr << "backend" << std::endl;      
        { ctl.backend(); }      
        std::cerr << "backend" << std::endl;      
        { ctl.backend(); }      
    }  
};       
         
int main(int argc, char *argv[]) {  
    TestApp app;  
    return Clingo::clingo_main(app, {argv + 1, static_cast<size_t>(argc - 1)});  
}

The program gives the following output:

clingo version 5.4.1
Reading from stdin
ground base
atom: 1
atom: 2
ground acid
atom: 1
atom: 2
atom: 3
backend
atom: 1
atom: 2
atom: 3
backend
atom: 1
atom: 2
atom: 3
UNKNOWN

Models       : 0+
Calls        : 1
Time         : 0.007s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.007s

It should give the following output:

clingo version 5.4.1
Reading from stdin
ground base
atom: 1
atom: 2
ground acid
atom: 3
backend
backend
UNKNOWN

Models       : 0+
Calls        : 1
Time         : 0.007s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.007s

This will be fixed in the next release.

[MaxOstrowski]

thanks. Maybe you can add a short notice in the documentation.

[rkaminsk]

thanks. Maybe you can add a short notice in the documentation.

I can recommend to call it after solve. The system is in best state to simplify then. In other circumstances it might still be possible to simplify but when exactly very much depends on the implementation. In principle it should always be possible to simplify; it is just difficult to implement. Future clingo versions might also be able to always simplify right after grounding. (Right now no simplification will happen if a theory is used.)

[rkaminsk]

Just some comments for myself how to fix this (no need to answer 😉). Quite involved actually.

At the moment cleanup calls LogicProgam::endProgram freezing the program. Thus, the next call to ClaspFacade::update unfeezes the program deleting the theory data. With the current implementation, cleanup can only be called after solving (where the program is still frozen) without destroying the theory data.

• The cleanup function no longer calls endProgram. It really only makes sense to call it right after solving.
• At the moment the documentation says that cleanup can be used to mark facts added via the backend. Better automatically mark facts added via the backend.
• Theory atoms should be passed to the backend only once. To do this, the seen flags have to be maintained until the end of solving.