2019-02-20 13:21 AEDT

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000315mercuryBugpublic2014-02-01 05:47
Reporterlpimmes 
Assigned To 
PriorityhighSeveritymajorReproducibilityalways
StatusnewResolutionopen 
PlatformOSOSxOS Version10.9.1
Product Version 
Target VersionFixed in Version 
Summary0000315: Software Error: detected need for minimal model in pred rodcut.r_n/3
DescriptionIn another program
:- pragma memo(fib/3). works OK here, but mode is det.

Trying memo on mode is multi. Comment out memo on two pred, output runs and is correct.
Uncomment memo and we get

   Software Error: detected need for minimal model in pred rodcut.r_n/3

Not sure how to create det function, because I need to make decision for base and recursive cases,
i.e., multiple output.
rodcut will be very slow for larger values of N, which is why I want memoization.
See listing attached file.
Thanks.
Steps To ReproducePartial listing:

...
% Implement rn, bottom of page 362 Dynamic programming, Cormen text.
% Should be implementing 15.2 rn = max (p_i + r_n-i)
% 1 <= i <= n, r0=0
%%%% Cannot use multi mode on functions, use pred, and declare main to be cc_multi.

:- pred r_n(int, array(int), int).
:- mode r_n(in, in, out) is multi.
%:- pragma memo(r_n/3).
r_n(1, P, Mx) :-
    Mx = getRevenue(1, P).
r_n(N, P, Mx) :-
    r_nAux(getRevenue(N, P), 1, N-1, P, Mx).

:- pred r_nAux(int, int, int, array(int), int).
:- mode r_nAux(in, in, in, in, out) is multi.
%:- pragma memo(r_nAux/5).
r_nAux(Mx, LowIndx, HighIndx, P, Max) :-
    (
     if LowIndx > HighIndx then
       Max = Mx
    else
       r_n(LowIndx, P, Lw),
       r_n(HighIndx, P, Hg),
        NewMax = int.max(Mx, Lw + Hg),
        r_nAux(NewMax, LowIndx + 1, HighIndx -1, P, Max)
    ).
...
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0000636

zs (developer)

I have uploaded a cleaned-up version of the original program, and a cut-down version of the test case.

The problem is that the program

- calls a memo'd nondet predicate, and gets the first solution,
- cuts the choice point for any more solutions (using cc_multi code) before printing the first.

That leaves the memoing data structures in an inconsistent state, believing that the original memo'd call is still active.

When a later call to the same nondet predicate specifies the same input arguments, the tabling code thinks it is an infinitely-recursive call, and generates the error message.

This is not a bug. This is a known limitation of memoing nondet predicates. The only problem that needs fixing is that the documentation does not do a good job of explaining this limitation.

~0000637

lpimmes (reporter)

OK, thanks for the help and the code.
+Notes

-Issue History
Date Modified Username Field Change
2014-01-31 14:01 lpimmes New Issue
2014-01-31 14:01 lpimmes File Added: rodcut.m
2014-01-31 15:15 zs File Added: bug315.m
2014-01-31 15:15 zs File Added: rodcut2.m
2014-01-31 15:20 zs Note Added: 0000636
2014-02-01 05:47 lpimmes Note Added: 0000637
+Issue History