Assertion failure "relation not found" on provenance

[DerZc]

Hi,

This program assertion failure on provenance with -t none:

.decl mrxr(A:unsigned)
.decl lxgy(A:unsigned) btree
.decl toay(A:unsigned)
.decl iemw(A:unsigned, B:unsigned, C:unsigned) inline
.decl pwfp(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned, G:unsigned)
.decl tsco(A:unsigned, B:unsigned) no_magic
.decl suvp(A:unsigned)
.decl yemn(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned) btree
.decl axuj(A:unsigned) no_magic brie
.decl xgts(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned, G:unsigned)
.decl vtvf(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned) magic
.decl ikzb(A:unsigned, B:unsigned, C:unsigned, D:unsigned) magic btree
.decl ezku(A:unsigned) brie
.decl edqg(A:unsigned, B:unsigned) btree
.decl pjnu(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned) magic
.decl ledu(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned) btree
.decl tlyw(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned, G:unsigned)
.decl xxlz(A:unsigned) brie
.decl fzmn(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned) magic btree
.decl uktu(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned) btree
.decl eoet(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned) magic btree
.decl nvcp(A:unsigned) brie
.decl iait(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned, G:unsigned) inline
.decl zqsz(A:unsigned, B:unsigned, C:unsigned) magic brie
.decl vdhp(A:unsigned, B:unsigned, C:unsigned) brie
.decl essu(A:unsigned, B:unsigned, C:unsigned) no_inline
.decl clzw(A:unsigned, B:unsigned, C:unsigned, D:unsigned, E:unsigned, F:unsigned, G:unsigned, H:unsigned) brie
.decl vdvr(A:unsigned, B:unsigned, C:unsigned)




mrxr(4).
mrxr(0).
mrxr(4).
mrxr(7).
mrxr(3).
mrxr(5).
mrxr(7).
mrxr(5).
mrxr(2).


lxgy(A) :- mrxr(A), mrxr(A).
toay(A) :- mrxr(B), lxgy(A), lxgy(B).
iemw(A, A, A) :- mrxr(A).
pwfp(A, A, A, A, A, A, A) :- lxgy(A), mrxr(A).
pwfp(A, A, A1, A, A, A, A) <= pwfp(A, A, A2, A, A, A, A) :- A1>A2.
tsco(A, B) :- pwfp(B, B, B, B, A, B, A).
tsco(A1, B) <= tsco(A2, B) :- A1=A2.
suvp(D) :- iemw(F, C, F), pwfp(E, F, E, F, D, D, D).
yemn(E, C, C, C, E, A) :- iemw(H, G, E), pwfp(C, C, B, A, A, C, H), pwfp(C, F, H, B, F, C, E).
axuj(A) :- toay(A).
xgts(A, A, A, C, A, A, C) :- suvp(C), mrxr(A), tsco(A, C).
vtvf(A, C, C, A, max(B,C)-A, A) :- toay(C), xgts(A, C, _, B, C, B, A), axuj(B).
ikzb(A, A, C, B) :- iemw(H, D, C), yemn(B, C, G, G, A, G).
ezku(E) :- vtvf(C, C, E, D, B, E), mrxr(C).
edqg(C, F) :- vtvf(B, A, B, G, D, H), pwfp(A, E, I, B, A, F, C), tsco(C, B).
pjnu(B, B, A, A, A, B) :- ikzb(A, B, A, B), ezku(A), tsco(B, A).
ledu(D, D, D, D, G, D) :- ezku(F), iemw(D, D, C), xgts(B, I, H, 0, G, G, D).
tlyw(B, B, E, D, E, D, B) :- pwfp(E, E, D, B, A, C, D), lxgy(D).
xxlz(A) :- suvp(D), tlyw(B, D, D, A, A, C, C), tlyw(C, A, B, B, A, D, B).
fzmn(H, C, F, J, F, B) :- ikzb(A, G, C, 7), xgts(J, J, B, H, J, E, F), pwfp(A, C, C, J, G, E, H), 0 = 0.
uktu(B, B, B, A, B, B) :- edqg(A, A), mrxr(B).
eoet(B, A, A, B, F) :- suvp(C), vtvf(B, B, D, A, F, A).
nvcp(E*E) :- uktu(C, E, E, C, A, E), pwfp(B, B, C, B, A, B, B), edqg(A, B), !ledu(E, A, A, B, B, A).
iait(B, A, A, B, B, B, B) :- iemw(B, A, B).
iait(B1, A, A, B, B, B, B) <= iait(B2, A, A, B, B, B, B) :- B1>B2.
zqsz(F, J, K) :- pwfp(E, H, A, N, O, M, M), yemn(J, M, J, B, C, F), ledu(L, K, I, F, C, G).
vdhp(B, B, B) :- vtvf(B, C, B, A, B, B), lxgy(A).
essu(A, A, A) :- lxgy(A).
clzw(A, B, C, C, C, D, C, A) :- zqsz(D, B, A), suvp(C), tsco(D, C).
vdvr(B, B, B) :- yemn(A, B, B, A, B, A).
vdvr(B, B, B1) <= vdvr(B, B, B2) :- B1=B2.

.output vdvr

The command is souffle -w -t none example.dl. Get the result:

souffle: /souffle/src/ram/analysis/Relation.cpp:30: const souffle::ram::Relation& souffle::ram::analysis::RelationAnalysis::lookup(const string&) const: Assertion `it != relationMap.end() && "relation not found"' failed.
Aborted

It run correctly without -t none. I don't know whether it is a feature related to #2316

[DerZc]

I find if I remove the subsumption of vdvr, the program can execute correctly with -t none.

[DerZc]

Hi,

I reduce the program, hope this can help you fix this bug.

.decl yemn(A:unsigned)
.decl vdvr(A:unsigned, B:unsigned, C:unsigned)

yemn(0).

vdvr(B, B, B) :- yemn(B).
vdvr(B, B, B1) <= vdvr(B, B, B2) :- B1=B2.

.output vdvr

[b-scholz]

Subsumptive clauses were not implemented in the provenance system. That is missing! Great find.

Either we need to report an issue or implement subsumptive clauses in the provenance system.

[DerZc]

I am very glad that this finding can help you and hope that other findings can be useful to you as well.