Grounding order calculation fails at recursive rule using external atoms

[madmike200590]

Input (external implementations at the bottom):

instr("bla blubb foo bar").

% Split input string by spaces
%%%% Rule R1
instr_segments(SEGS) :- instr(STR), &string_split[STR, " "](SEGS).
% Assign its array index to every string
%%%% Rule R2
instr_idx(STR, 0) :- instr_segments(SEGS), &lst_idx_value[SEGS, 0](STR), &lst_length[SEGS](LEN), LEN > 0.
%%%% Rule R3
instr_idx(STR, IDX) :- 
    instr_segments(SEGS), 
    &lst_idx_value[SEGS, IDX](STR), 
    &lst_length[SEGS](LEN), 
    IDX < LEN, 
    instr_idx(_, P_IDX), 
    P_IDX = IDX - 1.

Alpha fails to find a grounding order for R3:

Exception in thread "main" java.lang.RuntimeException: Could not find a grounding order for rule instr_idx(STR, IDX) :- instr_segments(SEGS), &lst_idx_value[SEGS, IDX](STR), &lst_length[SEGS](LEN), IDX < LEN, instr_idx(_0, P_IDX), P_IDX = IDX - 1. with starting literal: instr_segments(SEGS). Rule is not safe.
        at at.ac.tuwien.kr.alpha.grounder.RuleGroundingOrders.computeGroundingOrder(RuleGroundingOrders.java:186)
        at at.ac.tuwien.kr.alpha.grounder.RuleGroundingOrders.computeGroundingOrders(RuleGroundingOrders.java:163)
        at at.ac.tuwien.kr.alpha.common.rule.InternalRule.<init>(InternalRule.java:84)

I haven't debugged this any further due to lack of time, but it seems to me that this is a bug, especially because the following version of R3 where only the last literal P_IDX = IDX - 1 is swapped for IDX = P_IDX + 1 works and gives the following (correct) answer set:

instr("bla blubb foo bar")
instr_idx("bar", 3)
instr_idx("bla", 0)
instr_idx("blubb", 1)
instr_idx("foo", 2)
instr_segments(io.github.madmike200590.aoc.aspsupport.AlphaAspList@5f9b2141)

On a quick try, I wasn't able to reproduce this in a simpler setting without externals, so I'd assume this to be related to the atom &lst_idx_value[SEGS, IDX](STR) where it seems that IDX cannot be bound.

A working grounding order with starting literal instr_segments(SEGS) would be:

instr_segments(SEGS) -> binds SEGS
&lst_length[SEGS](LEN) -> binds LEN
instr_idx(_, P_IDX) -> binds P_IDX
P_IDX = IDX - 1 -> binds IDX
&lst_idx_value[SEGS, IDX](STR) -> binds STR, all variables bound

Also, note that in this case instr_ind(_, P_IDX) would probably make more sense as a starting literal.

I'll continue to investigate this.

External Atoms

@Predicate(name = "string_split")
public static Set<List<ConstantTerm<AlphaAspList<String>>>> splitString(String str, String regex) {
	// LOGGER.info("Split: {} by {}", str, regex);
	return Collections.singleton(
			Collections.singletonList(
					ConstantTerm.getInstance(AlphaAspList.of(str.split(regex)))));
}
	
@Predicate(name = "lst_idx_value")
public static <T extends Comparable<T>> Set<List<ConstantTerm<T>>> getValueAt(List<T> lst, int idx) {	
	if (idx >= lst.size()) {	
		return Collections.emptySet();
	}
	return Collections.singleton(Collections.singletonList(ConstantTerm.getInstance(lst.get(idx))));
}

@Predicate(name = "lst_length")
public static <T extends Comparable<T>> Set<List<ConstantTerm<Integer>>> lengthOfList(List<T> lst) {
	return Collections.singleton(Collections.singletonList(ConstantTerm.getInstance(lst.size())));
}	

[madmike200590]

Note that this problem also exists in #263. (I had the hope it might have resolved itself due to the new arithmetic term rewritings...)

[AntoniusW]

I think this is a case of "works as intended" and has nothing to do with external atoms. If I am not mistaken, then the rule R3 where it does not find a grounding order is not safe, simply because the variable IDX is not bound anywhere. IDX appears as input to an external atom, which is not binding, it appears in a comparison <, which is not binding, and it appears a third time inside some arithmetic expression, which is not binding again.

In order to bind IDX the solver would need to transform the equation P_IDX = IDX - 1 into IDX=P_IDX + 1 but such transformations are not always possible. Hence, for safety the usual rule is VAR = arithExpr is binding VAR but nothing else.
Or did I misunderstand the example?

Now we could of course consider whether the solver should be clever here and figure out that P_IDX = IDX -1 is sufficient to bind IDX whenever P_IDX gets its binding from somewhere else (which it does in the above example R3). An argument against this approach is that not all variables in equations can be resolved, for example X = Y * Y would yield two potential bindings for Y (one positive, one negative). In general, there may be many cases where the variables can be bound by a clever transformation of the input rules (for example if we have more than 2 variables and multiple equations), but we soon would need an algebra system to figure that out. So, the simple solution is to go with a syntactic approach ("equations only bind if one variable is alone at one side of the equation") and put the burden of writing it in the right way on the programmer.

[madmike200590]

oops.. yeah, I took the solver for cleverer than it's supposed to be 😅
I thought P_IDX = IDX - 1 should be sufficient to bind IDX, but considering your quadratic equation example, I fully agree that I shouldn't be lazy and write better code.

Should we just close this issue or re-label to potential enhancement along the lines of "figure out (simple) equations with unique integer solutions"? (I think closing it might be the more reasonable thing to do...)

Edit: Even though this is probably a bit of effort, should we think about better error messages here?

[AntoniusW]

Well, with Clingo one can do rules like p(X) :- dom(X - 2). where it is clever enough to figure out what is meant here even though the X in the head is not safe. But it also fails already at p(X) :- dom(X / 2). with an error and complains about the unsafe rule.

This is also not the first time, such an idea comes up, so it is rather natural to expect it to work. On the other hand, however, it will then fail at some more complex arithmetic expression and it may be rather confusing why some expressions work and others do not. So, I think the cleaner way is to not do that expression reformulation.

Ad error messages: yes, we need a well-done safety check in advance that prints good error messages.