[mercury-users] backtracking?

[hanberg at ruc.dk]

Quoting Ralph Becket <rafe at cs.mu.OZ.AU>:

> hanberg at ruc.dk, Thursday, 15 July 2004:
> > Hi
> >
> > I'm having trouble running a somewhat heavy program. I implemented a
> theorem
> > prover using mercury, but I have trouble with the following lines:
> >
> > :- pred proveable1(list(expr(T)), list(int), list(int)).
> > :- mode proveable1(in, in, out) is nondet.
> >
> > proveable1([Head|Tail], OLDINTLIST, NEWINTLIST) :-
> > 	proveable(Head, 4, INT),
> >	proveable2(Tail, [INT|OLDINTLIST], NEWINTLIST).
>
> Should `proveable2' be `proveable1' there?

You are right - I just temporarily changed the names of the whole thing to make
more sence.

>
> > proveable1(_, OLDINTLIST, NEWINTLIST) :- NEWINTLIST=OLDINTLIST.
>
> Should `_' be `[]'?  That would remove a major source of non-determinism
> from this predicate if so.
>
> > Mercury runtime: memory zone nondetstack#0 overflowed
> > PC at signal: 134522191 (804a54f)
> > This may have been caused by a stack overflow, due to unbounded recursion.
> >
> > I don't really know how to either get the ints out without backtracking or
> > extend the memory. Hope someone can help me.
>
> You haven't given us enough detail about what you're trying to do for us
> to be able to offer detailed help.  My guess is that your program is
> more non-deterministic than it needs to be, but I'd need to know more
> about what you're trying to achieve and what your code looks like to be
> sure.  If it's just a matter of extending the nondetstack size, you can
> do this by setting the MERCURY_OPTIONS="--nondetstack-size=1024"
> environment variable when running your program (see
>

The program is rather large. I'm building a tableau using a binary tree,
whereafter I test if there are inconsistency in the tree. The test returns
either 1, 2 or 3. Here is some of the code. The nondetstack option does not seem
to help, but the program is running fine if I don't try to get the int out.

steponeend(TREE, CURRENTPREFIX, CURRENTNOMINAL, OUTPUT, INT) :-
lidentifying(TREE, NEWTREE, []), steponeend(NEWTREE, CURRENTPREFIX,
CURRENTNOMINAL, OUTPUT, INT).

:- pred lidentifying(tree(A, B, C, D), tree(A, B, C, D), list(tree(A, B, C,
D))).
:- mode lidentifying(in, out, in) is nondet.

lidentifying(t('nil', X), NEWTREE, LIST) :- NLIST = [X|LIST], in6(NLIST, X1,
P1), in3(NLIST, X1, P2), in5(NLIST, P2, X2), nominal(X1), nominal(X2),
not(in4(NLIST, X2, P1)), NEWTREE=t(t('nil', n(X2, P1, 0)), X).

lidentifying(t(T1, X), NEWTREE, LIST) :- not(T1='nil'), lidentifying(T1, NT,
[X|LIST]), NEWTREE=t(NT, X).
lidentifying(t(T1, X, T2), NEWTREE, LIST) :- lidentifying(T1, NT, [X|LIST]),
NEWTREE=t(NT, X, T2).
lidentifying(t(T1, X, T2), NEWTREE, LIST) :- lidentifying(T2, NT, [X|LIST]),
NEWTREE=t(T1, X, NT).

stepnend(TREE, CURRENTPREFIX, CURRENTNOMINAL, OUTPUT, INT) :- closes3(TREE,
[]),OUTPUT=TREE, INT=3.

:- pred closes3(tree(A, B, C, D), list(tree(A, B, C, D))).
:- mode closes3(in, in) is semidet.

closes3(t('nil', X), LIST) :- NLIST = [X|LIST], in6(NLIST, Y, P), in6(NLIST,
NOM, P), in3(NLIST, NOM, P2), in4(NLIST, ~Y, P2), nominal(NOM).
closes3(t(T1, X), LIST) :- not(T1='nil'), closes3(T1, [X|LIST]).
closes3(t(T1, X, T2), LIST) :- closes3(T1, [X|LIST]), closes3(T2, [X|LIST]).

Thank you very much for your help

Tony





http://www.mercury.cs.mu.oz.au/information/doc-latest/mercury_user_guide/Running.html#Running)
>
> -- Ralph
> --------------------------------------------------------------------------
> mercury-users mailing list
> post:  mercury-users at cs.mu.oz.au
> administrative address: owner-mercury-users at cs.mu.oz.au
> unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
> subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
> --------------------------------------------------------------------------
>


--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------