Multiple models solver bug

[Ingmar Dasseville]

Segfault

vocabulary voc {
    type num isa nat
    lives(num,num)
    type neighborAmount isa nat
    nbOfLiveNeighbors(num,num):neighborAmount
}

theory theo: voc {
    // Declare how many neighbors of a certain cell are alive
    !x1 y1: nbOfLiveNeighbors(x1,y1) = #{ x2 y2 :
            (x1 ~= x2 | y1 ~= y2) & 
            abs(y1-y2) < 2 &
            abs(x1-x2) < 2 &
            lives(x2,y2) }.
    // Cells with exactly three living neighbors must live.
    !x y: nbOfLiveNeighbors(x,y)=3 => lives(x,y).
    // Each living cell must have two or three living neighbors.
    !x y: lives(x,y) => 2=< nbOfLiveNeighbors(x,y) =< 3.
}

structure struc: voc {
    neighborAmount = {0..8}
    num = {1..6}
}

term t: voc {
    // This term represents the amount of non-living cells
    #{ x y : ~lives(x,y) }
}

procedure main() {
    stdoptions.cpsupport = true
    stdoptions.nbmodels = 0
    print(minimize(theo,struc,t)[1])
}

[Bart Bogaerts]

Dat unicode negation sign is volgens mij niet het probleem.

Dat staat daar doordat deze code van de nieuwe web-ide is gekopieerd (ik krijg daar trouwens gewoon een parse error).

Als ik het vervang door ~, dan krijg ik een segfault (in de garbage collection van de solver)

0x00007ffff6da10d1 in Minisat::Solver::relocAll(Minisat::ClauseAllocator&) () from /cw/dtailocal/bartb/local/lib/libminisatid.so.3.10.0
(gdb) bt
#0  0x00007ffff6da10d1 in Minisat::Solver::relocAll(Minisat::ClauseAllocator&) () from /cw/dtailocal/bartb/local/lib/libminisatid.so.3.10.0
#1  0x00007ffff6da196c in Minisat::Solver::garbageCollect() () from /cw/dtailocal/bartb/local/lib/libminisatid.so.3.10.0
#2  0x00007ffff6da21ed in Minisat::Solver::search(int, bool) () from /cw/dtailocal/bartb/local/lib/libminisatid.so.3.10.0
#3  0x00007ffff6da24a7 in Minisat::Solver::solve(bool) () from /cw/dtailocal/bartb/local/lib/libminisatid.so.3.10.0
#4  0x00007ffff6d1e517 in MinisatID::PCSolver::solve(bool) () from /cw/dtailocal/bartb/local/lib/libminisatid.so.3.10.0
#5  0x00007ffff6d98243 in MinisatID::SearchEngine::solve(bool) () from /cw/dtailocal/bartb/local/lib/libminisatid.so.3.10.0
#6  0x00007ffff6de2c8c in MinisatID::ModelExpand::findNext(std::vector<MinisatID::Lit, std::allocator<MinisatID::Lit> > const&, MinisatID::ModelExpandOptions const&) () from /cw/dtailocal/bartb/local/lib/libminisatid.so.3.10.0
#7  0x00007ffff6de411a in MinisatID::ModelExpand::innerExecute() () from /cw/dtailocal/bartb/local/lib/libminisatid.so.3.10.0
#8  0x00007ffff7413328 in ModelExpansion::expand() const () from /cw/dtailocal/bartb/local/lib/libidp.so
#9  0x00007ffff7414e28 in ModelExpansion::doMinimization(AbstractTheory*, Structure*, Term*, Vocabulary*, TraceMonitor*, MXAssumptions const&) ()
   from /cw/dtailocal/bartb/local/lib/libidp.so
#10 0x00007ffff73c4259 in MinimizeInference::execute(std::vector<InternalArgument, std::allocator<InternalArgument> > const&) const ()
   from /cw/dtailocal/bartb/local/lib/libidp.so
#11 0x00007ffff72926f1 in LuaConnection::InternalProcedure::operator()(lua_State*) const () from /cw/dtailocal/bartb/local/lib/libidp.so
#12 0x00007ffff7292efe in LuaConnection::internalCall(lua_State*) () from /cw/dtailocal/bartb/local/lib/libidp.so
#13 0x00007ffff6a8c549 in luaD_precall(lua_State*, lua_TValue*, int) () from /cw/dtailocal/bartb/local/lib/liblua.so.5
#14 0x00007ffff6aa1110 in luaV_execute(lua_State*, int) () from /cw/dtailocal/bartb/local/lib/liblua.so.5
#15 0x00007ffff6a8cb1d in luaD_call(lua_State*, lua_TValue*, int) () from /cw/dtailocal/bartb/local/lib/liblua.so.5
#16 0x00007ffff6a8bc47 in luaD_rawrunprotected(lua_State*, void (*)(lua_State*, void*), void*) () from /cw/dtailocal/bartb/local/lib/liblua.so.5
#17 0x00007ffff6a8ce86 in luaD_pcall(lua_State*, void (*)(lua_State*, void*), void*, long, long) () from /cw/dtailocal/bartb/local/lib/liblua.so.5
#18 0x00007ffff6a828e1 in lua_pcall(lua_State*, int, int, int) () from /cw/dtailocal/bartb/local/lib/liblua.so.5
#19 0x00007ffff728ac76 in LuaConnection::execute(std::string const&) () from /cw/dtailocal/bartb/local/lib/libidp.so
#20 0x00007ffff73d31ce in handleAndRun(void*) () from /cw/dtailocal/bartb/local/lib/libidp.so
#21 0x00007ffff66722d7 in tthread::thread::wrapper_function(void*) () from /cw/dtailocal/bartb/local/lib/libtinythread.so
#22 0x00007ffff57fde9a in start_thread (arg=0x7ffff4c34700) at pthread_create.c:308
#23 0x00007ffff552a73d in clone () at ../sysdeps/unix/sysv/linux/x86_64/clone.S:112
#24 0x0000000000000000 in ?? ()

[Broes De Cat]

Ik heb het in een oudere versie van idp geprobeerd en die segfaulte op het negatie sign. Vervelend dat ik een edit niet kan rollbacken :) Probleem zit dan inderdaad in Jo's aanpassingen aan de optimalisatie in de solver.

[JoD]

Hmm, heb die aanpassingen nog niet naar de master gepusht :D Ga eens zien of ik het kan vinden...

[JoD]

Confirmed, segfault doet zich ook al voor in 07d9b93daf5e05decb619264e6d09c799dcfeec5. Het gebeurt op het moment dat een optimaal model gevonden is, en er een tweede model moet beginnen gezocht worden. Die garbage collect van minisatid dient om de clauses in een meer optimale geheugenconfiguratie te krijgen. Vermoeden is dat er ergens een ongeldige clause wordt meegegeven. Soit, onderzoek gaat door.

[JoD]

Goed, ik heb er geen idee van. De toegevoegde clause is simpelweg een unitclause met een nieuwe literal die zegt dat de varID die de objectieffunctie voorstelt een bepaalde waarde moet krijgen. Dit lijkt een use case die vaak getest is, en dus in het algemeen goed werkt.

Daarnaast zorgen kleine aanpassingen aan de theorie (bvb een constraint weglaten, of een overbodige constraint ( !x y: lives(x,y) => 1=< nbOfLiveNeighbors(x,y) =< 4.) toevoegen, dat de segmentation fault zich niet laat zien. Wat mij betreft is het een bug in minisatid, of een heel subtiel samenspel van het toevoegen van constraints in MinisatID en Minisat's clause management systeem.

Either way, dit zal tijdrovend zijn om uit te vissen -- ik ga hier voorlopig niet verder op zoeken.

[JoD]

On a sidenote: https://bitbucket.org/krr/minisatid/branch/opt_refactor_2 heeft deze segfault niet. Die branch raakt wel nog niet door alle tests.

Misschien ligt het aan de (in de toekomst weggerefactorde) savestate functionaliteit van de solver?

[Broes De Cat]

Gezien de error heeft het zo goed als zeker met de savestate te maken. (daarom dat aan jouw aanpassingen dacht, in de veronderstelling dat die in de master zaten ;) )

[JoD]

Ah, deze issue dient dan als motivatie om de branch met stateless solver sneller in orde te krijgen :)