Gringo considers unnecessary instantiations of rule heads.

[AbdallahS]

Consider the following program.

query(add(x,y)).
value(x,2). value(y,30).

value(E,@computeAdd("value",N1,N2)) :- query(E), E=add(E1,E2), value(E1,N1), value(E2,N2).
value1(add(E1,E2),@computeAdd("value1",N1,N2)) :- query(add(E1,E2)), value(E1,N1), value(E2,N2).
value2(E,@computeAdd("value2",N1,N2)) :- query(E), E > never, E=add(E1,E2), value(E1,N1), value(E2,N2).

#script (python)
import clingo

def computeAdd(message, N1,N2):
    print(f"{message} computes {N1} + {N2}")
    return clingo.Number(N1.number+N2.number)
#end.

The rules producing value, value1, and value2 are equivalent, however in the rule for value, gringo attempts to ground the head with substitutions that are inconsistent with the rule body.

The output I get is:

clingo version 5.7.1 (849f282)
Reading from engine/testRedundant.lp
Solving...
Answer: 1
value(x,2) value(y,30) value(add(x,y),32) query(add(x,y)) value1(add(x,y),32) value2(add(x,y),32)
SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.172s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.172s
"value" computes 2 + 30
"value" computes 30 + 30
"value" computes 2 + 2
"value" computes 30 + 2
"value" computes 2 + 32
"value" computes 30 + 32
"value" computes 32 + 32
"value" computes 32 + 2
"value" computes 32 + 30
"value2" computes 2 + 30
"value1" computes 2 + 30

I haven't detected any semantic inconsistency/bug, but this behaviour could potentially have a detrimental impact to grounding speed independent of the use of external functions. The running the test file below with --const test=0 takes 1.5sec on my machine whereas any other value of test runs in less than 0.1sec

#const test=0.
cTest(test).
query(add(x,x,x,x,x, x,x,x,x,x, x,x,x,x,x, x,x,x,x,x)).
v(x). v(y). w(x). w(y). w(z).

slow0(E) :- query(E), E=add(E00,E01,E02,E03,E04,E05,E06,E07,E08,E09,E10,E11,E12,E13,E14,E15,E16,E17,E18,E19), v(E00), v(E01), v(E02), v(E03), v(E04), v(E05), v(E06), v(E07), v(E08), v(E09), v(E10), v(E11), v(E12), v(E13), v(E14), v(E15), v(E16), v(E17), v(E18), v(E19), cTest(0).
fast1(add(E00,E01,E02,E03,E04,E05,E06,E07,E08,E09,E10,E11,E12,E13,E14,E15,E16,E17,E18,E19)) :- query(add(E00,E01,E02,E03,E04,E05,E06,E07,E08,E09,E10,E11,E12,E13,E14,E15,E16,E17,E18,E19)), v(E00), v(E01), v(E02), v(E03), v(E04), v(E05), v(E06), v(E07), v(E08), v(E09), v(E10), v(E11), v(E12), v(E13), v(E14), v(E15), v(E16), v(E17), v(E18), v(E19), cTest(1).
fast2() :- query(add(E00,E01,E02,E03,E04,E05,E06,E07,E08,E09,E10,E11,E12,E13,E14,E15,E16,E17,E18,E19)), v(E00), v(E01), v(E02), v(E03), v(E04), v(E05), v(E06), v(E07), v(E08), v(E09), v(E10), v(E11), v(E12), v(E13), v(E14), v(E15), v(E16), v(E17), v(E18), v(E19), cTest(2).
fast3(E) :- query(E), E=add(E00,E01,E02,E03,E04,E05,E06,E07,E08,E09,E10,E11,E12,E13,E14,E15,E16,E17,E18,E19), w(E00), w(E01), w(E02), w(E03), w(E04), w(E05), w(E06), w(E07), w(E08), w(E09), w(E10), w(E11), w(E12), w(E13), w(E14), w(E15), w(E16), w(E17), w(E18), w(E19), cTest(3).
fast4(E) :- cTest(4), query(E), E=add(E00,E01,E02,E03,E04,E05,E06,E07,E08,E09,E10,E11,E12,E13,E14,E15,E16,E17,E18,E19), v(E00), v(E01), v(E02), v(E03), v(E04), v(E05), v(E06), v(E07), v(E08), v(E09), v(E10), v(E11), v(E12), v(E13), v(E14), v(E15), v(E16), v(E17), v(E18), v(E19).

[rkaminsk]

The grounder orders body literals according to some heuristic before grounding. It is not guaranteed to be the best order and it is easy to construct something where it fails. Maybe it can be improved...

The grounder does not handle equivalences as well as it could. Currently, it is better to write query(add(X,Y)) instead of query(E), E=add(X,Y). Incidentally, the former also ensures that the heuristic picks up the literal first because it has "a small domain", "a nested function symbol" and "more variables". It's would probably be a good idea to substitute variable E in such kind of cases. Maybe @MaxOstrowski's ngo tool can already suggest something.

[MaxOstrowski]

ngo trabsforms the slow0 rule into the fast1 rule.

Unfortunately, it gets stuck doing quadratic tests on the many variables doing other tests :2nd_place_medal: But for your first program it just works. (Don't forget to mention some of your output predicates, otherwise ngo will remove too much)

[AbdallahS]

Thank you both for your answers. Sorry for the confusion in my original post. My issue does not have to do with optimizing the order of the body literals. It is rather than gringo unnecessarily generates unreachable head atoms only to discard them immediately.

Consider the following small example. I would expect an instance of the head match(@test(X)) to be generated by gringo only when there exists an instantiation of the rule variables that satisfies the body, and then X would be given by that instantiation. In the example, the domain of predicates value/1 and query/1 do not overlap, so I do not expect there ever to be a need to call the python function test.

value(a). query(b).
match(@test(X)) :- query(X), value(X).

#script (python)
import clingo

def test(X):
    print("secret",X)
    return clingo.Number(0)
#end.

The ouput is

clingo version 5.7.1 (849f282)
Reading from engine/testRedundant3.lp
Solving...
Answer: 1
value(a) query(b)
SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.199s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.199s
secret a

The fact that secret a appears in the output of clingo indicates that the atom match(0) was generated at some point by gringo, even though it didn't need to be.

[rkaminsk]

But it is all about the body ordering heuristic. Gringo may evaluate body literals and functions appearing in a rule in any order. There are however some ways to enforce orders. For example, introducing an auxiliary predicate:

value(a). query(b).
query_value(X) :- query(X), value(X).
match(@test(X)) :- query_value(X).

[ejgroene]

Thank you. Now I understand it better. Your example interests me:

match(@test(X)) :- query(X), value(X).

because it illustrates the pragmatics my programs rely on.

I have developed in-source testing for my code and would write an assert quite similar:

assert(@all(some_test_case(X)) :- some(X), more(X).

The call to @all happens before the instantiation starts and that helps me to register the test case and check afterwards that the rule evaluates to true (the assert(...) is present in all models, to be exact).

I really never thought about it because it seemed obvious to me.

What exactly is the problem with gringo generating "unreachable" atoms? Why do you call them unreachable?

[AbdallahS]

What exactly is the problem with gringo generating "unreachable" atoms?

Erik, see below some examples where the current approach is counter-intuitive to me. The python functions are defined afterwards.

positive(1..100).
square(N,N*N) :- input(N).                      % Square N is defined for any integer N.
log(N,@computeLog(N)) :- input(N), positive(N). % Log N is only defined if N is positive.

input(-2). input(10). input(32).

#show square/2.
#show log/2.

I expect to obtain square(-2,4) squar(10,100) square(32,1024) log(10,3) log(32,5), but instead I get a python math error (because of a call to math.log(-2))

addableType(int). % regular addition
addableType(string). % string concatenation
result(add(A,B),@plus(T,A,B)) :- query(add(A,B)), type(A,T), type(B,T), addableType(T).
error(add(A,B),"cannot add values of different type") :- query(add(A,B)), type(A,T1), type(B,T2), T1 != T2.

type(0..5,int). type("hello",string). type("world",string).
query(add(2,5)).
query(add("hello","world")).
query(add(2,"world")).

#show result/2.
#show error/2.

I expect to obtain result(add(2,5),7) result(add("hello","world"),"helloworld") error(add(2,"world"),"cannot add values of different type"), but instead I get a python RuntimeError: unexpected (because of a call to A.string when A is the clingo object 2)

domain(0..10,0..10).
resultOfComputation(X,Y,@slowComputation(X,Y)) :- invokeComputation(X,Y), domain(X,Y).

invokeComputation(5,7).

#show resultOfComputation/3.

If the complexity of a slow computation is $C$ and the number of invokations is $m$ (here $m=1$), then I expect the runtime complexity of grounding this snippet to be $O(mC)$. In other words, if I increase the size of the domain but I do not invoke more slow computations, the grounding time shouldn't be sensibly slower. This is currently the case because of how internal heuristics are defined, but it is not a guarantee provided by gringo (as far as I understand), it is more of a coincidence.

#script (python)

import math
import clingo
import time

''' Compute the base 2 logarithm of the argument '''
def computeLog(N):
    return clingo.Number(int(math.log(N.number,2)))

''' Combine values provided they have the same type T '''
def plus(T,A,B):
    if str(T) == "string":
        return clingo.String(A.string + B.string)
    elif str(T) == "int":
        return clingo.Number(A.number + B.number)
    else:
        print(f"addition not implemented for type {T}")
        return []

''' Do something complicated with the numeric input and return the result '''
def slowComputation(X,Y):
    assert X.type == clingo.SymbolType.Number and Y.type == clingo.SymbolType.Number
    x = X.number
    y = Y.number
    time.sleep(2) # simulates that the computation of z is expensive
    z = x + y
    return clingo.Number(z)
#end.

Why do you call them unreachable?

Consider this snippet

small(0). small(1). small(2).
positive(1). positive(2). positive(3).
smallAndPositive(N) :- small(N), positive(N).

What should this snippet be grounded to? Here is a correct (but undesirable) grounding. It is undesirable because it contains some rules that are unreachable: we know at grounding time that their body cannot ever be satisfied.

small(0). small(1). small(2).
positive(1). positive(2). positive(3).
smallAndPositive(0) :- small(0), positive(0).
smallAndPositive(1) :- small(1), positive(1).
smallAndPositive(2) :- small(2), positive(2).
smallAndPositive(3) :- small(3), positive(3).
smallAndPositive(4) :- small(4), positive(4).
smallAndPositive("hello") :- small("hello"), positive("hello").

Here is an incorrect grounding. It is incorrect because there is a relevant rule missing (when N=2)

small(0). small(1). small(2).
positive(1). positive(2). positive(3).
smallAndPositive(0) :- small(0), positive(0).
smallAndPositive(1) :- small(1), positive(1).

In my opinion, of all the correct groundings, the most desirable one is the one that only includes relevant rules. Incidentally, this is the one clingo returns (with --text --keep-facts to disable optimizations/simplifications).

small(0). small(1). small(2).
positive(1). positive(2). positive(3).
smallAndPositive(1) :- small(1), positive(1).
smallAndPositive(2) :- small(2), positive(2).

Without going too much into details, one can determine fairly desirable groudings by inductively defining sets of reachable ground atoms. An atom $A$ is reachable in $n$ steps if there is a rule $(H,B)$ and a variable substitution $\Theta$ such that

• for any positive literal $P \in B$ in the body, $P[\Theta]$ is reachable in $< n$ steps.
• for any negative literal $N \in B$ in the body, $N[\Theta]$ is not reachable in $< n$ steps.
• $A = H[\Theta]$

For example, consider this snippet where I add a rule that cannot trigger.

small(0). small(1). small(2).
positive(1). positive(2). positive(3).
positive(0) :- never.
smallAndPositive(N) :- small(N), positive(N).

Because gringo knows that positive(0) is not reachable in any number of inflation steps, the output is the same "most desirable" grounding and, in particular, we do not get a rule with head smallAndPositive(0).

(One can improve the definition of reachability above to make the set of reachable atoms even smaller, but this is getting out of scope.)

Anyway. Consider this snippet

number(-1..1).
positive(1..4).

p1(100/N) :- positive(N).
q1(@divide(100,N)) :- positive(N).

#script (python)
import clingo

def divide(X,Y):
    return clingo.Number(X.number // Y.number)

#end.

Although 0 is in the Herbrand universe (via number(0), for example), we do not expect any division by zero to take place in the computation of p1 because the substitution ${N\mapsto 0}$ does not satisfy the body of the rule (indeed positive(N)$[{N \mapsto 0}]$ is unreachable. So we do not need to try and instantiate the head p1(100/N)$[N \mapsto 0]$.

Now, introduce

p2(100/N) :- number(N), positive(N).

We still don't have any division by 0 issue, because no substitution that satisfies the body maps $N$ to 0. (If there had been a division by 0, then gringo would have emitted a message info: operation undefined: (100/N). You can test it with p3(100/N) :- number(N).)

You can contrast

q2(@divide(100,N)) :- number(N), positive(N).

The body is the same as for the rule for p2 and there is no substitution that satisfies the body while mapping $N$ to 0. Nevertheless, the python division function gets called and we get a ZeroDivisionError: integer division or modulo by zero error. In other words, gringo has instantiated the head of the rule with a substitution that does not satisfy the body. This is unnecessary and it surprised me enough that I created this issue!

(There are workarounds, like staging as Roland offers, but they make the code more cumbersome in my applications.)

[rkaminsk]

You should return an empty list if a function is not defined for its arguments.

[AbdallahS]

You should return an empty list if a function is not defined for its arguments.

Yes, I use the approach of returning an empty list when the function is not defined for some meaningful arguments, as in the @plus function example.

[rkaminsk]

We can also think of some way to give the user more control in which order body literals are instantiated (external functions are translated into X=@call(...) by gringo). Currently, everything is working as designed but I see that there are cases where one wants more fine-grained control.

[AbdallahS]

Ok, I understand better why you keep talking about body literals while I refer to the head of a rule. It's because in my example programs, the @call does not occur is not a body literal (so my examples don't require any particular ordering of the body literals in the user program); however the current implementation moves the @call to the body, so after this transformation the counter-intuitive behaviou may occur or not depending on the ordering of the body literals of the intermediate program

Although giving more control to users about the order in which the body literals are processed could be a nice addition, it seems that it is much more than I ask: I only ask that the head literal is instantiated after the body literals. (And at the same time, providing the user more control is less than I ask, because it would still require the user to provide redundant information that was already in the source file.)

In the following example, the p2 rule does not generate a division by 0 but the q2, r2, and t2 rules might. I think it's normal that gringo does not provide a guarantee for r2 and t2 (for the reasons that you have given, it depends on the ordering of the body literals), but I don't see why q2 cannot come with the same mechanism as p2.

number(-1..1). positive(1..4).

p2(100/N) :- number(N), positive(N).
q2(@divide(100,N)) :- number(N), positive(N).

r2(X) :- number(N), positive(N), X=100/N.
t2(X) :- number(N), positive(N), X=@divide(100,N).

#script (python)
import clingo
def divide(X,Y):
    return clingo.Number(X.number // Y.number)
#end.

To me, this issue is orthogonal to a user-choice of body literal ordering because there will never be a case where instantiating a head literal before instantiating a body literal is a better order: Take any ordering, adjust it so that the head literal is last and you are guaranteed to get a non-slower (sometimes faster) process. (Assuming there is no crash, of course). As such, instantiating the head literals last should not be seen as a heuristic but as an optimal choice.

[ejgroene]

Thank you very much Abdallah for your elaborate explanation. I believe I understand it better now, and if indeed so, I conclude that multiple issues play a role here.

1. Correctness of the logic does not seem to be an issue here. The semantics of the logic are not questioned. It is the pragmatics, i.e. how and when things happen, that are subject of discussion. Am I correct?

At times while reading your explanation I got the impression that you seem to think that the way it works now is somehow not correct. But that isn't really the case, is it?

Often pragmatics of a language are implicitly defined by the implementation and ASP seems no exception. As there are no formal specifications, changing the implementation might solve your problem and create a new one for me. For that reason I support the idea of explicit control of body literals and have it formalised.

2. It is an optimisation problem, as avoiding instantiation and Python call can speed up the computation, right?

I do believe that it is a very important issue for ASP (and any other logic language) that optimisation and heuristics are quite essential in many applications. I haven't had such a problem myself yet, but that might change and at some point it might become necessary to prune expensive calculations. After all, a correct answer, but too late, is not a correct answer. Therefore I support the idea of being able to control unnecessary calls to Python by smart ordering of the literals.

4. It is about protection of Python code against incorrect inputs from within ASP, as dealing with incorrect inputs is possible in Python and there is a way of communicating the non-results that incorrect inputs cause. Ok?

Seeing from this perspective I can't really support this case. I believe it is usually not hard to write better code that does some checking, and that Python code must rather not leave it to the caller if it crashes or not.

Then again, I like the idea of having a separate step of calling the Python functions before the grounder starts optimising. @call is the bridge between logic and imperative code, and it might be useful to know a thing or two about when it is called exactly. I use it to create in-source tests/asserts and I'd rather not see it breaking.

[rkaminsk]

In your program

t2(X) :- number(N), positive(N), X=@divide(100,N).

a small tweak of the scoring heuristic would suffice to ensure that X=@divide(100,N) would come after the other two atoms. I would say that for a constant time division it should not matter but there could be more expensive external functions. It is hard to tell with python code.

On another note, even the head is part of the join gringo is computing. The complete join is something like

number(N), positive(N), X=@divide(100,N), #not_fact t2(X).

If the head is a fact, the rule is discarded. All its elements are subject to the ordering heuristic. There might be cases where it might be beneficial to do the fact check early. Admittedly not in typical programs.

When writing logic programs, especially when using function symbols, arithmetic, or external functions, we have to have some knowledge about the way a program is instantiated to argue that it yields a finite instantiation. However, I would recommend to make as few assumptions as possible. For external functions, I would always check for valid inputs.