Undefined arithmetics throws exception instead of ignoring the ground instance.

[AntoniusW]

The following program tries to evaluate f(1+b), which contains an undefined arithmetic. An exception is thrown although the ground instance should be simply ignore.

q(1). q(b).
r(H) :- H = f(X + Y), q(X), q(Y).

The expected answer is { q(1), q(b), r(f(2)) } but an exception originating in substituting during grounding is thrown.

java.lang.NullPointerException
at at.ac.tuwien.kr.alpha.common.terms.ConstantTerm.hashCode(ConstantTerm.java:80)
at java.util.WeakHashMap.hash(WeakHashMap.java:298)
at java.util.WeakHashMap.get(WeakHashMap.java:396)
at at.ac.tuwien.kr.alpha.common.Interner.intern(Interner.java:15)
at at.ac.tuwien.kr.alpha.common.terms.ConstantTerm.getInstance(ConstantTerm.java:25)
at at.ac.tuwien.kr.alpha.common.terms.ArithmeticTerm.getInstance(ArithmeticTerm.java:58)
at at.ac.tuwien.kr.alpha.common.terms.ArithmeticTerm.substitute(ArithmeticTerm.java:89)
...

Side note: in a recent version of the standard, Undefined Arithmetics are actually treated differently than in older versions. Now the standard requires input programs to be invariant under substitution of undefined arithmetic expressions with any term from the universe (in other words: programmer has to make sure undefined arithmetics do not occur). We might adopt a similar stance and decide that throwing an exception is actually the right thing (albeit it should be way more telling than the one Alpha produces with the above example). @madmike200590 what is your opinion on that?

[madmike200590]

As for the undefined arithmetics, yes, a better error message is definitely needed. Also, I'd read ... requires input programs to be ... more as Solvers should have a static check rejecting programs that do not fulfill the criteria rather than making this something users get only notified of when it blows up at runtime.
However, isn't the real problem with the above rule the uninterpreted function symbol f? Even if X + Y were an integer, the rule would still not be safe in the sense that Alpha has no way of knowing what f(X + Y) is, even if it has a value for X + Y.

I think (although I don't know if Alpha would be smart enough), a variant of the program, say

q(1). q(2), p(f(3)).
r(H) :- H = f(X + Y), q(X), q(Y), p(H).

should work (in the sense that it's valid ASP and should have substitutions), but I see no way of resolving f(X + Y) in the original program.

[madmike200590]

This issue seems to be a duplicate of #203

[AntoniusW]

Regarding the text of the standard, I think they explicitly cite a program

a(0).
p :- a(X), not q(X/X).

where for the substitution X->0 we get the ground instance p :- a(0), not q(0/0). where zero divided by zero is undefined arithmetics, so this is not a well-formed substitution and thus should be disregarded. So the answer-set of the above program is { a(0) }. On the other hand, a clever grounder might observe that q/1 never occurs in any rule head, so any not q(...) will evaluate to true. Hence the clever grounder might simply rewrite the rule to p :- a(X). and then one of course obtains as answer set { a(0), p }. In other words: preprocessing and optimizations have to consider that some instantiations may result in undefined arithmetics.
Now for practical reasons, the recent ASP-Core-2 disallows such input programs. Note that we can get rid of the problem in the above program by changing the rule to p :- a(X), not q(X/X), X != 0. as now a clever grounder would rewrite this to p :- a(X), X != 0. For Alpha, this would of course still mean that we might encounter an instantiation of an ArithmeticTerm with 0/0 which is undefined and should be handled properly (note that whether we encounter 0/0 depends on the grounding order for this rule).

Regarding the questions whether H = f(X+Y) has valid substitutions at all: I am quite sure it does, just consider X->1, Y->3 then we have H = f(1+3). Since the value of a ground arithmetic term is the evaluated value of the arithmetic expression, so 4 in this case, we actually have here H = f(4), which is perfectly fine. Note that the standard puts the arithmetic evaluation of a ground rule as last step, so formally, we take a substitution X->1, Y->3, H->f(4) and apply that to obtain f(4) = f(1+3), then after arithmetic evaluation (i.e., replacing every maximal arithmetic sub-term with the integer it evaluates to) this becomes f(4)=f(4) and evaluates to true.

Regarding the duplicate, yes, this is basically #203 resurfacing again. But this time I have more questions. :-)

How to solve the issue: currently, it seems that we have to change all substitutions and subclasses of Term to make them aware that every substitution might yield no result. Our current code assumes that applying a substitution to any term or atom yields a term or atom again. One workaround to avoid changing all the return types could be to add another rewriting that extracts all arithmetic evaluations and puts them into a new atom type just for evaluating arithmetic expressions (similarly as we do it with intervals). Then dealing with undefined arithmetic would be concealed in one place, but then we have another type of program -- those with arithmetic evaluations safely encapsulated and those without it.

Basically, we could go two ways: 1) add evaluation abilities to all terms and make them aware that the result of an evaluation of one term may be any number of new terms (so we can also cover interval terms then). 2) add rewriting and put the evaluation safely way into builtin atoms (like we do it now with interval terms).
Any ideas/opinions on that observation?

[madmike200590]

Right, I wasnt't thinking the part with the uninterpreted function through, sorry about that..

I tested a bit now and took a closer look at our code. The current NullPointerException seems to be caused by an actual bug in ArithmeticTerm:
Leaving aside the bigger discussion about sophisticated arithmetics for now, I tested following program

p(1). q(a).
r(X) :- p(Y), q(Z), X = Y + Z.

and got the NPE mentioned above.
Now, theoretically, this should - even with our current implementation - just yield the answer set {p(1), q(a)}. The arithmetic term Y + Z should be evaluated when getSatisyingSubstitutions on X = Y + Z is called with substitution Y -> 1, Z -> A, see ComparisonLiteral, line 160 onward:

		// Check if the groundTerm is an arithmetic expression and evaluate it if so.
		if (groundTerm instanceof ArithmeticTerm) {
			Integer result = evaluateGroundTerm(groundTerm);
			if (result == null) {
				return Collections.emptyList();
			}
			resultTerm = ConstantTerm.getInstance(result);
		} else {
			...
		}

ArithmeticTerm#evaluateGroundTerm calls evaluateGroundTermHelper, which actually does a check for undefined arithmetics:

	private static Integer evaluateGroundTermHelper(Term term) {
		if (term instanceof ConstantTerm
			&& ((ConstantTerm<?>) term).getObject() instanceof Integer) {
			// Extract integer from the constant.
			return (Integer) ((ConstantTerm<?>) term).getObject();
		} else if (term instanceof ArithmeticTerm) {
			return ((ArithmeticTerm) term).evaluateExpression();
		} else {
			// ASP Core 2 standard allows non-integer terms in arithmetic expressions, result is to simply ignore the ground instance.
			return null;
		}
	}

Note that this is called recursively for every non-constant term making up the initial term, such that, eventually, we should see a which is not an integer or arithmetic term and return null accordingly, causing ComparisonLiteral#getSatisfyingSubstitutions to (correctly) return an empty list, i.e. no satisfying substitutions with start substitution Y -> 1, Z -> A.

The reason this does not happen and the NPE happens in this "chaotic" fashion is that, upon substituting the arithmetic term, the new (substituted) term is constructed using ArithmeticTerm#getInstance:

	public static Term getInstance(Term left, ArithmeticOperator arithmeticOperator, Term right) {
		// Evaluate ground arithmetic terms immediately and return result.
		if (left.isGround() && right.isGround()) {
			Integer result = new ArithmeticTerm(left, arithmeticOperator, right).evaluateExpression();
			return ConstantTerm.getInstance(result);
		}
		return INTERNER.intern(new ArithmeticTerm(left, arithmeticOperator, right));
	}

Since both 1 and a are ground, the "shortcut" from the if kicks in and tries to directly evaluate. However, since in contrast to ComparisonLiteral#getSatisfyingSubstitutions, the result isn't checked here, the NPE happens (in ConstantTerm#getInstance).

Now, I'm not sure about the exact reasons for this if being there, but I think we'd solve the NPE by simply removing it. So we'd not evaluate anything during substitution, and evaluate arithmetics only when instantiating the respective ComparisonLiterals. To me, this seems like the way to, at least for a fix of the current problem without considering the above "sophisticated" cases.