Incremental tabling in compiled code not working as I expect

General
1

SPOILER ALERT: for those solving Advent of Code the following will contain a (likely non-idiomatic) solution for part 2 of day 18.

This year, I’ve been trying to learn/relearn Prolog by solving the Advent of Code problems. On today’s problem (day 18) I’ve encountered different behavior between compiled and directly run code.

I’m (ab-)using a dynamic predicate and tabling in the solution. From reading the reference manual this seems to necessitate incremental tabling to properly invalidate the table.

My code is:

:- dynamic([corrupted/2], [incremental(true)]).

initCorrupted(Points) :-
  retractall(corrupted(_,_)),
  foreach(member(X/Y,Points), assertz(corrupted(X,Y))).

step(X/Y, X2/Y) :-
  (X2 is X + 1; X2 is X - 1),
  0 =< X2, X2 =< 3,
  \+ corrupted(X2,Y).
step(X/Y, X/Y2) :-
  (Y2 is Y + 1; Y2 is Y - 1),
  0 =< Y2, Y2 =< 3,
  \+ corrupted(X,Y2).

:- table pathToGoal/2 as incremental.
pathToGoal(Start,Start).
pathToGoal(Start,End) :-
  step(Start,Next),
  pathToGoal(Next,End).

binarySearch(Low,Low,_, Low).
binarySearch(Low,High,Points, Res) :-
  Mid is (Low + High) // 2,
  length(Prefix, Mid),
  append(Prefix,_,Points),
  initCorrupted(Prefix),
  ( pathToGoal(0/0,3/3)
  -> Low2 is Mid + 1, binarySearch(Low2,High,Points,Res)
  ; binarySearch(Low,Mid,Points,Res)
  ).

compute2(Points, Res) :-
  length(Points,N),
  High is N - 1,
  binarySearch(0, High, Points, M),
  nth1(M, Points, Res).

run() :-
  Points = [ 0/3, 1/2, 2/1, 3/0, 2/2, 1/3, 0/2],
  compute2(Points, X/Y),
  format('Result: ~d,~d~n', [X,Y]).

Directly running this I get the expected output

$ swipl -g run -g halt aoc18.pl
Result: 3,0

However, when first compiling the code, I get a different result

$ swipl -g run -g halt -o aoc -c aoc18.pl
$ ./aoc
Result: 1,3

This is also the result I get when not declaring the table of pathToGoal as incremental. Manually abolishing the table in initCorrupted/1 with abolish_table_subgoals(pathToGoal(_,_)) fixes the issue in the compiled code, leading me to believe the table is not properly invalidated.

Is this behavior expected, and I am doing something wrong? Or is this a bug?

PS: I’m also happy to hear about any improvements to make my solution more idiomatic.

2

You are right. The incremental property of the dynamic predicate corrupted is lost in the compiled state. That is a bug. There are also at least three dubious things with the code:

  • foreach/2 is something to be avoided if you can. In this case it is ok to backtrack over the 2nd argument and thus forall/2 is faster and has no issues.
  • Commit to a tabled predicate is wrong as it looses answers. I think it is safe in this particular case as the call is ground.
  • As the second clause of binarySearch/4 keeps firing, it produces an infinite sequence of the same answer.
3

Fixed with FIXED: Preserve `incremental` property when creating a saved state. · SWI-Prolog/swipl-devel@21264b8 · GitHub

4

Thank you for the quick answer, fix, and suggested improvements. I really appreciate it.

I assume this refers to the pathToGoal(0/0,3/3) on the left of ->? I see now that this is also mentioned in the documentation, however, I don’t fully understand the issue. Does the commit cause an incomplete table so that later calls to the tabled predicate miss the “unexplored” solutions? Are there any resources where I can find problematic examples of this? I can’t seem to construct one myself.

5

Yes. But, SWI-Prolog does local scheduling, which implies that it tries to complete a table before continuing the execution. To get trapped by this the predicate needs to be incomplete when the cut is used, which implies that it needs to be part of a larger strongly connected component, i.e., a set of mutually dependent tabled predicates. The way it works is that if, while filling the table, it hits a new tabled predicate, it extends its scope (strongly connected component) and solves the two predicates together.