Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
marklaw opened this issue Oct 29, 2021 · 6 comments
Closed

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

marklaw opened this issue Oct 29, 2021 · 6 comments
Labels
bug
Milestone
v5.5.1

Comments

@marklaw
Copy link

marklaw commented Oct 29, 2021

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
Copy link
Member 

➜ 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 rkaminsk added the bug label Oct 30, 2021
@rkaminsk
Copy link
Member

I reduced the problem to the following two smaller programs:

The programs can be run with

  • zcat bug.lp.gz | clingo --opt-str=usc,stratify --loops=shared, and
  • zcat bug.aspif.gz | clasp --opt-str=usc,stratify --loops=shared.

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

@rkaminsk rkaminsk added this to the v5.5.1 milestone Nov 2, 2021
@marklaw
Copy link
Author

marklaw commented Nov 3, 2021

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 added a commit to potassco/clasp that referenced this issue Nov 6, 2021
@BenKaufmann
Fix potassco/clingo#342
da10954 
* Do not create loop formulas containing aux variables.
@BenKaufmann
Copy link
Contributor

@rkaminsk Thanks for the aspif program 👍
Should be fixed now.

@rkaminsk
Copy link
Member

rkaminsk commented Nov 6, 2021

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

@rkaminsk rkaminsk closed this as completed Nov 6, 2021
@marklaw
Copy link
Author

marklaw commented Nov 6, 2021

Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug
Projects
None yet
Milestone
v5.5.1
Development

No branches or pull requests
3 participants
@rkaminsk @marklaw @BenKaufmann