Problems when evaluating multiple levels of arithmetic definitions

[stefborg]

The following program works:

@declare A(any, integer) .
@declare B(any, integer) .
@declare C(any, integer) .

C(?x, ?y) :- A(?x, ?z), B(?x, ?v), ?y = ?z + ?v, ?y > 10 .

However, when I try to replace ?y in the head with ?y * 5, I run into various problems.

Option 1

C(?x, ?y * 5) :- A(?x, ?z), B(?x, ?v), ?y = ?z + ?v, ?y > 10 .

throws

        Parse error on line 5, column 1: Complex term "?y * 5" uses an undefined variable "y".

Option 2

C(?x, ?u) :- A(?x, ?z), B(?x, ?v), ?y = ?z + ?v, ?y > 10, ?u = ?y * 5 .

throws

Parse error on line 5, column 1: The variable "u" must only depend on variables that occur in a positive body literal.

Option 3

C(?x, (?z + ?v) * 5) :- A(?x, ?z), B(?x, ?v), ?z + ?v > 10 .

works, but requires duplicating (or triplicating ...) terms, which is less intuitive, in particular if ?y has a clear meaning in the application.

I can live with Option 3 for now, but in the long run I would like to use more complex expressions for which both Option 1 (arithmetics over defined variables) and Option 2 (multiple levels of variable definitions) would be very useful.

[stefborg]

The example still does not work correctly, although there are no parse errors anymore.

For the following program, Nemo derives C(a, 13):

A(a, 5) .
B(a, 8) .

C(?x, ?y) :- A(?x, ?z), B(?x, ?v), ?y = ?z + ?v, ?y > 10 .

@output C .

But when I add * 5 in the head, then no C-facts are derived:

C(?x, ?y * 5) :- A(?x, ?z), B(?x, ?v), ?y = ?z + ?v, ?y > 10 .

The following rule without the assignment for ?y works as expected:

C(?x, ?y * 5) :- A(?x, ?y), ?y > 3 .

(Using Nemo 0.5.2-dev from the main branch (89b36257) and rustc 1.82.0-nightly (8b3870784), but this also happens in the web interface on 0.5.1.)

[matzemathics]

A minimal example of that bug would be

T(1).

R(?y + 1) :- T(?x), ?y = ?x + 1.

@output R .

[matzemathics]

@aannleax my hunch here would be that the constructors are evaluated in the wrong order:

positive_constructors: [
    Constructor { variable: Universal("_CONSTRUCT_0"), term:  Addition
     ├─ Variable(Universal("y"))
     └─ GroundTerm(AnyDataValue(Long(LongDataValue(1))))
     },
    Constructor { variable: Universal("y"), term:  Addition
     ├─ Variable(Universal("x"))
     └─ GroundTerm(AnyDataValue(Long(LongDataValue(1))))
     }]