Single shot solving without deleting the logic program

[rkaminsk]

Currently, the clingo API always uses multi-shot solving. Some users reported that solving performance in this mode is worse compared to single-shot solving. Thus, it would be nice to be able to use the API in single-shot mode, too. The problem is that clasp's facade releases the logic program right after preprocessing in single-shot mode. Since the clingo API relies on having the logic program available even after/during solving, we cannot simply switch to single-shot solving mode. Would it be possible to switch to single-shot solving mode without deleting the logic program?

[BenKaufmann]

@rkaminsk
I implemented somthing in dev but I'm not fully convinced that it is enough. Could you please check whether this works for you?

[rkaminsk]

I'll have a look.

[rkaminsk]

On my small test this seems to be working. We might need additional runtime checks though:

from sys import argv
from clingo import Control

ctl = Control(argv[1:])

ctl.add('base', [], '1 {a; b} 1.')
ctl.ground([('base', [])])
print('solving step 1.1')
ctl.solve(on_model=print)
print('solving step 1.2')
ctl.solve(on_model=print)

ctl.add('blub', [], '1 {c; d} 1.')
ctl.ground([('blub', [])])
print('solving step 2')
ctl.solve(on_model=print)

The above code produces the following output:

$ python test.py 0 --single-shot
solving step 1.1
a
b
solving step 1.2
b
solving step 2
b c
b d

$ python test.py 0 
solving step 1.1
a
b
solving step 1.2
a
b
solving step 2
a d
a c
b d
b c

What do you think? Should we already throw a runtime error in step 1.2? In clingo I could only do this by having another state bool. Would it be easier in clasp?

[rkaminsk]

Actually, I think I could do the check easily in the update function but I think in clasp it is nicer. Would it be as simple as this?

diff --git a/src/clasp_facade.cpp b/src/clasp_facade.cpp
index c70549e..00b452e 100644
--- a/src/clasp_facade.cpp
+++ b/src/clasp_facade.cpp
@@ -888,6 +888,7 @@ void ClaspFacade::enableSolveInterrupts() {
 }
 
 void ClaspFacade::startStep(uint32 n) {
+       POTASSCO_REQUIRE(n == 0 || incremental());
        step_.init(*this);
        step_.totalTime = RealTime::getTime();
        step_.cpuTime   = ProcessTime::getTime();

[BenKaufmann]

@rkaminsk I added a slightly different version of the runtime checks - hopefully with the same effect for clingo. While currently not fully implemented, conceptually, clasp supports three different modes:

• destructive single-shot, where the problem can be solved exactly once
• multi-solve, where the same problem can be solved multiple times, e.g. with different reasoning modes
• multi-shot, where the problem can be updated and solved multiple times

In order to not break the second case, I added checks to prepare() and update() instead.

[rkaminsk]

Sounds good. The multi-solve mode would actually be interesting for clingo, too. It just might be tricky to fiddle it in because, currently, solving always starts a new step.