search

potassco / clingo

🤔 A grounder and solver for logic programs.
https://potassco.org/clingo
MIT License
616 stars 81 forks source link

Crash with "const: Assertion `validVar(v)' failed" #342

Closed marklaw closed 3 years ago

marklaw commented 3 years ago

Hi,

I'm getting an issue when using Clingo 5.5.0 and the latest Clingo from the wip branch. When I run the attached file with the flag --opt-strat=usc,stratify Clingo crashes and gives the following error:

clingo: /home/mark/Downloads/clingo/clasp/clasp/solver.h:547: Clasp::ValueRep Clasp::Solver::value(Clasp::Var) const: Assertion `validVar(v)' failed.
Aborted (core dumped)

This file is auto generated by ILASP, so is quite messy. It is also using multi-shot solving. If it helps, I can try to reconstruct the final single-shot program which fails and clean up the program a bit.

Thanks,

Mark

crash_file.txt

rkaminsk commented 3 years ago 
➜ gdb --args ./build/debug/bin/clingo crash_file.txt --opt-str=usc,stratify
(gdb) run
Solving...
Answer: 1
v_i(105)
Optimization: 0
Solving...
Progression : [6;inf]
Answer: 1
active(21) active(22) active(23) active(24) active(79)
Optimization: 23
Progression : [10;23] (Error: 1.3)
Progression : [14;23] (Error: 0.642857)
Answer: 2
active(21) active(24) active(79)
Optimization: 15
Answer: 3
active(21) active(24) active(79) v_i(105)
Optimization: 14
Solving...
Progression : [6;inf]
Progression : [12;inf]
Answer: 1
active(21) active(22) active(78) active(97)
Optimization: 21
Progression : [16;21] (Error: 0.3125)
Progression : [18;21] (Error: 0.166667)
Progression : [20;21] (Error: 0.05)
clingo: /home/kaminski/Documents/git/potassco/clingo/clasp/clasp/solver.h:547: Clasp::ValueRep Clasp::Solver::value(Clasp::Var) const: Assertion `validVar(v)' failed.

Program received signal SIGABRT, Aborted.
0x00007ffff6bf918b in raise () from /lib/x86_64-linux-gnu/libc.so.6
(gdb) bt
#0  0x00007ffff6bf918b in raise () from /lib/x86_64-linux-gnu/libc.so.6
#1  0x00007ffff6bd8859 in abort () from /lib/x86_64-linux-gnu/libc.so.6
#2  0x00007ffff6bd8729 in ?? () from /lib/x86_64-linux-gnu/libc.so.6
#3  0x00007ffff6be9f36 in __assert_fail () from /lib/x86_64-linux-gnu/libc.so.6
#4  0x00007ffff75a17c7 in Clasp::Solver::value (this=0x5555556251b0, v=1949) at /home/kaminski/Documents/git/potassco/clingo/clasp/clasp/solver.h:547
#5  0x00007ffff759f42b in Clasp::LoopFormula::simplify (this=0x555555828d30, s=...) at /home/kaminski/Documents/git/potassco/clingo/clasp/src/clause.cpp:1035
#6  0x00007ffff75aa484 in Clasp::simplifyDB<bk_lib::pod_vector<Clasp::Constraint*, std::allocator<Clasp::Constraint*> > > (s=..., db=..., shuffle=false)
    at /home/kaminski/Documents/git/potassco/clingo/clasp/clasp/solver.h:895
#7  0x00007ffff763443f in Clasp::Solver::simplifySAT (this=0x5555556251b0) at /home/kaminski/Documents/git/potassco/clingo/clasp/src/solver.cpp:735
#8  0x00007ffff7633c82 in Clasp::Solver::simplify (this=0x5555556251b0) at /home/kaminski/Documents/git/potassco/clingo/clasp/src/solver.cpp:667
#9  0x00007ffff763146b in Clasp::Solver::endStep (this=0x5555556251b0, top=66, params=...) at /home/kaminski/Documents/git/potassco/clingo/clasp/src/solver.cpp:304
#10 0x00007ffff761fda2 in Clasp::SharedContext::unfreezeStep (this=0x55555562aa48) at /home/kaminski/Documents/git/potassco/clingo/clasp/src/shared_context.cpp:877
#11 0x00007ffff761fc3e in Clasp::SharedContext::unfreeze (this=0x55555562aa48) at /home/kaminski/Documents/git/potassco/clingo/clasp/src/shared_context.cpp:865
#12 0x00007ffff76157bf in Clasp::ProgramBuilder::updateProgram (this=0x55555562ade0) at /home/kaminski/Documents/git/potassco/clingo/clasp/src/program_builder.cpp:48
#13 0x00007ffff75668a0 in Clasp::ClaspFacade::doUpdate (this=0x55555562aa40, p=0x55555562ade0, updateConfig=false, sigAct=0x0)
    at /home/kaminski/Documents/git/potassco/clingo/clasp/src/clasp_facade.cpp:1044
#14 0x00007ffff75667bb in Clasp::ClaspFacade::update (this=0x55555562aa40, updateConfig=false, sigAct=0x0) at /home/kaminski/Documents/git/potassco/clingo/clasp/src/clasp_facade.cpp:1029
#15 0x00007ffff75667fa in Clasp::ClaspFacade::update (this=0x55555562aa40, updateConfig=false) at /home/kaminski/Documents/git/potassco/clingo/clasp/src/clasp_facade.cpp:1033
#16 0x00007ffff7216a8c in Gringo::ClingoControl::update (this=0x55555562b0b0) at /home/kaminski/Documents/git/potassco/clingo/libclingo/src/clingocontrol.cc:199
#17 0x00007ffff7216bb3 in Gringo::ClingoControl::ground (this=0x55555562b0b0, parts=std::vector of length 1, capacity 1 = {...}, context=0x0)
    at /home/kaminski/Documents/git/potassco/clingo/libclingo/src/clingocontrol.cc:215
#18 0x00007ffff7246ced in clingo_control_ground (ctl=0x55555562b0b0, vec=0x555555a64858, n=1, cb=0x0, data=0x0) at /home/kaminski/Documents/git/potassco/clingo/libclingo/src/control.cc:1796
#19 0x00005555555be1ce in (anonymous namespace)::ControlWrap::ground (L=0x555555650ef8) at /home/kaminski/Documents/git/potassco/clingo/libluaclingo/luaclingo.cc:3390
#20 0x00007ffff6fd44d5 in ?? () from /lib/x86_64-linux-gnu/liblua5.3.so.0
#21 0x00007ffff6fe1225 in ?? () from /lib/x86_64-linux-gnu/liblua5.3.so.0
#22 0x00007ffff6fd48c8 in ?? () from /lib/x86_64-linux-gnu/liblua5.3.so.0
#23 0x00007ffff6fd48f5 in ?? () from /lib/x86_64-linux-gnu/liblua5.3.so.0
#24 0x00007ffff6fd0370 in lua_callk () from /lib/x86_64-linux-gnu/liblua5.3.so.0
#25 0x00005555555bfcc4 in (anonymous namespace)::luaMain (L=0x555555650ef8) at /home/kaminski/Documents/git/potassco/clingo/libluaclingo/luaclingo.cc:3764
#26 0x00007ffff6fd44d5 in ?? () from /lib/x86_64-linux-gnu/liblua5.3.so.0
#27 0x00007ffff6fd4897 in ?? () from /lib/x86_64-linux-gnu/liblua5.3.so.0
#28 0x00007ffff6fd48f5 in ?? () from /lib/x86_64-linux-gnu/liblua5.3.so.0
#29 0x00007ffff6fd3cf7 in ?? () from /lib/x86_64-linux-gnu/liblua5.3.so.0
#30 0x00007ffff6fd4b9f in ?? () from /lib/x86_64-linux-gnu/liblua5.3.so.0
#31 0x00007ffff6fd043e in lua_pcallk () from /lib/x86_64-linux-gnu/liblua5.3.so.0
#32 0x00005555555c085b in (anonymous namespace)::LuaScriptC::main (ctl=0x55555562b0b0, data=0x555555623650) at /home/kaminski/Documents/git/potassco/clingo/libluaclingo/luaclingo.cc:3943
#33 0x00007ffff724907e in (anonymous namespace)::CScript::main (this=0x555555623670, ctl=...) at /home/kaminski/Documents/git/potassco/clingo/libclingo/src/control.cc:2129
#34 0x00007ffff725f72b in Gringo::Scripts::main (this=0x7ffff7a470c0 <Gringo::g_scripts()::scripts>, ctl=...) at /home/kaminski/Documents/git/potassco/clingo/libclingo/src/scripts.cc:43
#35 0x00007ffff72172a3 in Gringo::ClingoControl::main (this=0x55555562b0b0, app=..., files=std::vector of length 1, capacity 1 = {...}, opts=..., out=0x55555562ade0)
    at /home/kaminski/Documents/git/potassco/clingo/libclingo/src/clingocontrol.cc:254
#36 0x00007ffff72043c7 in Gringo::ClingoApp::run (this=0x7fffffffcd50, clasp=...) at /home/kaminski/Documents/git/potassco/clingo/libclingo/src/clingo_app.cc:281
#37 0x00007ffff7263689 in Clasp::Cli::ClaspAppBase::run (this=0x7fffffffcd50) at /home/kaminski/Documents/git/potassco/clingo/clasp/app/clasp_app.cpp:217
#38 0x00007ffff76a1a0d in Potassco::Application::main (this=0x7fffffffcd50, argc=3, argv=0x7fffffffd128)
    at /home/kaminski/Documents/git/potassco/clingo/clasp/libpotassco/src/application.cpp:127
#39 0x00007ffff72492a9 in clingo_main_ (argc=3, argv=0x7fffffffd128) at /home/kaminski/Documents/git/potassco/clingo/libclingo/src/control.cc:2152
#40 0x0000555555576b3a in main (argc=3, argv=0x7fffffffd128) at /home/kaminski/Documents/git/potassco/clingo/app/clingo/main.cc:50

This might be a problem with the simplification of clasp's loop formulas. If I run the problem with --loops=common, --loops=distinct, or --loops=no, then it seems to work. @marklaw it would certainly be nice to have something simpler than the program you attached. We would also need @BenKaufmann's help to figure out the problem.

rkaminsk commented 3 years ago

I reduced the problem to the following two smaller programs:

The programs can be run with

@BenKaufmann the aspif program is quite small. I hope this can be used to find the issue easily.

marklaw commented 3 years ago

Sorry Roland. I've been out of the office for the last few days. Thanks for reducing the program yourself. If you need anything further from me, please let me know.

BenKaufmann commented 3 years ago

@rkaminsk Thanks for the aspif program :+1:
Should be fixed now.

rkaminsk commented 3 years ago

Thanks @BenKaufmann. @marklaw, development packages are available.

marklaw commented 3 years ago

Thanks!