Scryer-prolog: Where is the time spent? (Exhibit 5)

[triska]

With presprover.pl, I expect each of the following queries to terminate instantly:

      ?- valid(x > 0).
      false.

      ?- satisfiable(x > 0).
      true.

      ?- valid(x >= 0).
      true.

      ?- valid(exists(x, x > 0)).
      true.

      ?- valid(forall(x, exists(y, 3*x + y > 2))).
      true.

      ?- valid(2*y + 3*x = 30 /\ x = 0 ==> y = 15).
      true.

      ?- valid(x = 3 \/ not(x=3)).
      true.

      ?- valid(x = 5 ==> 2*x = 10).
      true.

      ?- valid(y > 1 /\ x = 3 /\ x + y < 19 ==> x + 19 > y).
      true.

Currently, none of them seem to terminate at all, or take a long time.

An infinite supply of test cases is available via:

?- presprover:run.

However, it seems to hang. What is going on?

[triska]

Thank you, this now works very nicely!

Could you please briefly explain which code triggered this problem, and what is now being indexed with Usize? It is surprising that this occured only with this specific program so far.

[mthom]

usize values are now being indexed as constants. They are unsigned, 8-byte integers.

The code was failing inside the assoc library, between length and the list_to_assoc helper. length outputs list lengths as usize's. Because usize's weren't being recorded as constant index values, switch_on_constant failed in the first and second clauses, causing the list_to_assoc helper to enter an infinite loop through its third clause.

[triska]

Thank you a lot!

I have now ported Presprover to Scryer Prolog, and it is available from its page:

https://www.metalevel.at/presprover/

Please use that link to obtain the latest version; I am closing this issue.

[mthom]

It is surprising that this occured only with this specific program so far.

I had a similar problem with fixnums a few weeks ago. I should have handled Usize then. I was really shocked that #314 went uncaught for literal years.

[triska]

The testing we are doing now is only manual, and covers only a small part of the system. The best test cases are systematic and exhaustive (not random). This will uncover many additional issues.

Ideally, each such reported and resolved issue goes into its own small test file!