Enable Arithmetics

[AntoniusW]

In order to realize arithmetics as per the standard, the following is required:

• [ ] The parser needs to take operator precedence into account (* and / before + and -).
• [ ] Evaluation of all ground arithmetic terms occurring anywhere as a subterm ( a fact p(f(g(3+4,a)). must yield p(f(g(7,a)) in all answer sets).
• [ ] Ignoring instances of undefined arithmetics ( p(3+a). and p(3/0). are simply ignored, likewise a constraint :- not p(3/0). is also ignored).

[votacom]

It also seems that arithmetics with variables is unsupported.

Steps to reproduce:

#> cat test.asp
h :- b(1-Y), d(Y).

#> java -jar alpha.jar -i test.asp
Exception in thread "main" java.lang.UnsupportedOperationException: Unsupported syntax encountered: 1-Y
[...]

Release v0.2.0

[votacom]

I am sorry, my comment was too specific. Apparently, Alpha v0.2.0 does not yet support arithmetics at all.

[AntoniusW]

The current master branch supports a little arithmetics, so Alpha should process it if you build from source (see https://github.com/alpha-asp/Alpha#building) and then write your rule as:

h :- b(B1), B1 = Y-1, d(Y).

Otherwise arithmetics is still very limited as this issue indicates.

[rtaupe]

Apparently it can happen that Alpha does not ground rules in which unsupported forms of arithmetics occur, but no error message is returned to the user, who may not notice in this case that anything is wrong. Can be reproduced with this program, in which the term O-1 in the following rule seems to be problematic: h_assign_1(U1,T,X,W) :- order(X,T,O), assign(U,T1,Y), order(Y,T1,O-1), maxOrder(M), maxUnit(MU), comUnit(U1), U1<=U, maxElem(ME), W=10*MU*(M-O)+2*(ME-X)+U1.

So as a first step, Alpha should at least report to the user if unsupported arithmetics occur in the input.

[AntoniusW]

Can you provide a minimal working example of the wrong behaviour? I just tested a simple version with the term 0-1 and it gets evaluated to -1 correctly on the master branch. There were some changes to the evaluation of arithmetics some time ago, such that ground arithmetic expressions should now be evaluated by the grounder directly.

[rtaupe]

I will try to find a smaller example, but I can already tell you it´s about O-1 (variable minus constant), not 0-1 (constant minus constant).

[AntoniusW]

O, I saw that as 0. But even with a variable, I fail to reproduce the error.

My test program is:

h_assign_1(U1,T,X,W) :- order(X,T,O), assign(U,T1,Y), order(Y,T1,O-1), maxOrder(M),maxUnit(MU),comUnit(U1), U1<=U, maxElem(ME), W=10*MU*(M-O)+2*(ME-X)+U1.
order(1,now1,3).
order(2,now2,2).
maxOrder(7).
maxUnit(11).
comUnit(5).
assign(6,now2,2).
maxElem(13).

Alpha on master finds the following answer set:

Answer set 1:
{ assign(6, now2, 2), comUnit(5), h_assign_1(5, now1, 1, 469), maxElem(13), maxOrder(7), maxUnit(11), order(1, now1, 3), order(2, now2, 2) }
SATISFIABLE

What is missing here?

[rtaupe]

Unfortunately I also cannot reproduce the issue using the approach of a minimal input program. However, I narrowed the issue down to the call of Substitution#unify, which returns null. Obviously this is because of a missing feature in Substitution#unifyTerms. You can reproduce the issue as follows:

@Test
public void testSubstituteNminus1() {
	Predicate predOrder = Predicate.getInstance("order", 3);
	ConstantTerm<Integer> const1 = ConstantTerm.getInstance(1);
	ConstantTerm<String> constZ = ConstantTerm.getInstance("z");
	VariableTerm varN = VariableTerm.getInstance("N");
	Atom substitute = new BasicAtom(predOrder, const1, constZ, ArithmeticTerm.getInstance(varN, ArithmeticTerm.ArithmeticOperator.MINUS, const1));
	Instance instance = new Instance(const1, constZ, const1);
	Substitution unification = Substitution.unify(substitute, instance, new Substitution());
	Substitution expectedUnification = new Substitution();
	expectedUnification.put(varN, ConstantTerm.getInstance(2));
	assertEquals(expectedUnification, unification);
}

[AntoniusW]

Ahh, I see: it tries to unify 1 with N-1 and fails. Honestly, I am not sure if we should support this, since this would mean that our unification needs to solve arithmetic equations.

I think this should never happen, i.e., throw an error (possibly at some other position already).