[Martin Meyer]

Hello Thomas!

Predicate programControl:getBackTrack/0-> returns a pointer to the current position in the Backtrack Stack. Is that stack the same as the Run Stack or is it a separate stack? How can I inspect what is on the stack(s)?

My intention is to set up a solution to the problem discussed in Reverting changes on backtracking. Roughly the plan to register an undo-action to a destructive change would be:

Find the latest backtrack point on the stack. The backtrack point contains the address of where to return to in backtracking. Exchange that original address with the address of a nondeterm predicate which does three things: First it repairs the stack by restoring the original address in the backtrack point. Second it calls the undo-action procedure. Third it fails so that program execution continues normally by backtracking to the original address.

Do you think this plan is feasible somehow when you clue me how to interpret the stack's contents?

[Gukalov]

Hi.
I just use "or". It works. In the simple cases at list)))
Some object fact/propertie changes on the way forward and the old value sets back on the way backward.

Code: Select all

...
OldValue = fact1,
(
   % forward: 
   % any action that changes the fact1
   % next in the chain 
or
   % backward
   fact1 := OldValue,
   fail
).

[Martin Meyer]

Yes, it works with "or":

Code: Select all

class facts
    fact1 : string := "original".
 
class predicates
    changeFact : () multi.
clauses
    changeFact() :-
        OldValue = fact1,
        (fact1 := "replaced" or fact1 := OldValue and fail).
 
clauses
    run() :-
        stdIO::write("1 Start: ", fact1, '\n'),
        changeFact(),
        stdIO::write("2 Changed: ", fact1, '\n'),
        fail.
 
    run() :-
        stdIO::write("3 End: ", fact1, '\n').

That outputs:

Code: Select all

1 Start: original
2 Changed: replaced
3 End: original

Thomas has advised a similar construction to yours in How To Remove Reference Domains from a Project. The construction requires that the destructive change is done in a multi or nondeterm predicate. If the change is done in a procedure or determ predicate, then the "or"-construction is impossible:

Code: Select all

class facts
    fact1 : string := "original".
 
class predicates
    tryChangeNonEmptyFact : () determ.
clauses
    tryChangeNonEmptyFact() :-
        fact1 <> "",
        OldValue = fact1,
        (fact1 := "replaced" or fact1 := OldValue and fail). %violates mode determ
 
clauses
    run() :-
        stdIO::write("1 Start: ", fact1, '\n'),
        if tryChangeNonEmptyFact() then
            stdIO::write("2 Changed: ", fact1, '\n')
        else
            stdIO::write("2 Not changed: ", fact1, '\n')
        end if,
        fail.
 
    run() :-
        stdIO::write("3 End: ", fact1, '\n').

Even replacing determ by nondeterm in the above would not produce desired results because the condition in an if-then-else statement is a cut-scope which would cut off the undo-action.

The solution, about which I am asking Thomas, by manipulating the stack, should work out always however; no matter whether the predicate, in which the destructive change is done, has mode procedure, determ, multi, or nondeterm.

[Thomas Linder Puls]

As already mentioned I think you are walking soft grounds doing things like that (and I don't see a way for you to do it either).

The backtrack stack is a chain of backtrack records, in vip 10 it is like this:

Code: Select all

domains
    btop =
        backtrackEntry(btop Next, ttopP LastTTop, returnAddress ReturnAddress, unsignedNative EBP).

When backtracking the "BTOP" is set to Next and the "TTOP" (trap top) is set to LastTTop. Then the EPB/RPB register is restored to EBP and finally we jump to ReturnAddress.

For you the problem is, that you don't something which is compatible with a ReturnAddress and an EBP.

You would be able to create an anonymous predicate/predicate closure, which is a pointer to a piece of data whose first element is a pointer to the code to run. But the invocation of such one, is completely different from restoring a backtrack point.

[Martin Meyer]

At least in 32-bit mode this seems to work in VIP 10:

Code: Select all

    open core
 
class predicates
    registerUndo : (predicate Undo).
clauses
    registerUndo(Undo) :-
        StackMark = programControl::getBackTrack(),
        OriginalStackEntry = memory::getPointer(StackMark),
        registerUndo_1(Undo, StackMark, OriginalStackEntry),
        !.
 
class predicates
    registerUndo_1 : (predicate Undo, programControl::stackMark StackMark, pointer OriginalStackEntry) multi.
clauses
    registerUndo_1(_Undo, StackMark, _OriginalStackEntry) :-
        NewStackMark = programControl::getBackTrack(),
        NewStackEntry = memory::getPointer(NewStackMark),
        memory::setPointer(StackMark, NewStackEntry).
 
    registerUndo_1(Undo, StackMark, OriginalStackEntry) :-
        memory::setPointer(StackMark, OriginalStackEntry),
        Undo(),
        fail.
 
class facts
    myFact : string := "original".
 
clauses
    run() :-
        stdIO::write("1: ", myFact, '\n'),
        OldMyFact = myFact,
        myFact := "changed",
        registerUndo({  :- myFact := OldMyFact }),
        stdIO::write("2: ", myFact, '\n'),
        fail.
 
    run() :-
        stdIO::write("3: ", myFact, '\n').

It outputs:

Code: Select all

1: original
2: changed
3: original

But in 64-bit mode it produces an access violation.

Do you think it is a valid solution in 32-bit or otherwise what is wrong with it?
If the solution is OK in 32-bit, how to fix the access violation in 64-bit?

[Martin Meyer]

I suspect that the arguments of the call to registerUndo_1/3 are pushed on the run stack, but after the cut in registerUndo/1 the stack shrinks and they become "dead" entries which can be overwritten. So, if that is the problem, how to cure it?

I made a test using facts instead of the arguments of registerUndo_1. That cannot be a final solution of course, but only a test:

Code: Select all

    open core
 
class facts
    undo : predicate := erroneous.
    stackMark : programControl::stackMark := erroneous.
    originalStackEntry : pointer := erroneous.
 
class predicates
    registerUndo : (predicate Undo).
clauses
    registerUndo(Undo) :-
        StackMark = programControl::getBackTrack(),
        OriginalStackEntry = memory::getPointer(StackMark),
        undo := Undo,
        stackMark := StackMark,
        originalStackEntry := OriginalStackEntry,
        registerUndo_1(),
        !.
 
class predicates
    registerUndo_1 : () multi.
clauses
    registerUndo_1() :-
        NewStackMark = programControl::getBackTrack(),
        NewStackEntry = memory::getPointer(NewStackMark),
        memory::setPointer(stackMark, NewStackEntry).
 
    registerUndo_1() :-
        memory::setPointer(stackMark, originalStackEntry),
        undo(),
        fail.
 
class facts
    myFact : string := "original".
 
clauses
    run() :-
        stdIO::write("1: ", myFact, '\n'),
        OldMyFact = myFact,
        myFact := "changed",
        registerUndo({  :- myFact := OldMyFact }),
        stdIO::write("2: ", myFact, '\n'),
        fail.
 
    run() :-
        stdIO::write("3: ", myFact, '\n').

Unfortunately however that still produces an access violation in 64-bit.

OK then, I tried it another way. What happens when I remove the cut in registerUndo/1 to keep the new stack entry alive. That's also not a final solution of course, but a test:

Code: Select all

    open core
 
class predicates
    registerUndo : (predicate Undo) multi.
clauses
    registerUndo(Undo) :-
        StackMark = programControl::getBackTrack(),
        OriginalStackEntry = memory::getPointer(StackMark),
        registerUndo_1(Undo, StackMark, OriginalStackEntry).
 
class predicates
    registerUndo_1 : (predicate Undo, programControl::stackMark StackMark, pointer OriginalStackEntry) multi.
clauses
    registerUndo_1(_Undo, StackMark, _OriginalStackEntry) :-
        NewStackMark = programControl::getBackTrack(),
        NewStackEntry = memory::getPointer(NewStackMark),
        memory::setPointer(StackMark, NewStackEntry).
 
    registerUndo_1(Undo, StackMark, OriginalStackEntry) :-
        memory::setPointer(StackMark, OriginalStackEntry),
        Undo(),
        fail.
 
class facts
    myFact : string := "original".
 
clauses
    run() :-
        stdIO::write("1: ", myFact, '\n'),
        OldMyFact = myFact,
        myFact := "changed",
        registerUndo({  :- myFact := OldMyFact }),
        stdIO::write("2: ", myFact, '\n'),
        fail.
 
    run() :-
        stdIO::write("3: ", myFact, '\n').

That worked without access violation in 32- and 64-bit.

However I need registerUndo/1 to be procedure not multi. So, how else could I keep the new stack entry alive?

[Thomas Linder Puls]

The determinism analysis obviously establishes a "semantical value" to the programmer. But it also provides crucial information about how to generate code for the clauses. A predicate that can leave a backtrack point have a very special calling convention, because it doesn't vacate the run stack, it leaves its entry (aka. activation record/stack frame/<dear child many names (Danish manner of speaking; don't know it it exist in English)>) . The stack is not vacated until the predicate finally fails (and no backtrack point exist anymore).

Now you ask: how to make a procedure (or determ) stay on the stack. You can't, because the calling convention for a procedure vacates the stack on return. Assuming that you could make a "fake" procedure that didn't vacate the stack it would be very fragile, because calling that procedure from another procedure would vacate the stack when that procedure returned.

In fact this need to know that the call stack must be retained is the reason that some kind of mode analysis has existed in our Prolog version all the way back to the very first day.

Besides this you will also have a problem with cut. Because a cut removes backtrack points including your undo actions, but when backtracking on a level further out you would need your undo actions to be executed. In the old days (with reference domains and truly free variables) variables would need to be unbound when backtracking, such variables were recorded in a (so called) trail (a notion from the original Warren abstract machine). When cutting trail entries from the backtrack-records that was cut away would be moved to the new top most backtrack point so that when that was effectuated the unbindings would be performed even though they originally came from another backtrack point.

In those old days the cut operation would pop the backtrack records one at the time collecting the trail entries until it the new top was encountered the collected trail elements would then be added to the new top (I can't remember all the details. Today we don't need to collect anything so the backtrack-top is simply set to the new value.

(I can't remember all the details of the vip5 handling, it is decades ago it was changed and I had nothing to do with the development of it).

[Martin Meyer]

OK, when a procedure returns, it cannot leave anything on the stack. Thus I tried a different approach.

Instead of creating a new backtrack point which will be vacated on the return from the "register undo-action" procedure, I am re-using an existant one. For this purpose I am creating an "undo backtrack point" in an initialize routine. The undo backtrack point undos the destructive changes on re-entering. In procedure registerUndoAction I detour the latest backtrack point by setting its return address to the return address of the undo backtrack point:

Code: Select all

    open core
 
domains
    backtrackEntry = backtrackEntry(bTop Next, tTopP LastTTop, returnAddress ReturnAddress, unsignedNative EBP).
    bTop = pointer.
    tTopP = pointer.
    returnAddress = pointer.
 
class facts
    myFact : string := "original".
 
class predicates
    show : (string Mark).
clauses
    show(Mark) :-
        stdIO::write("(", Mark, ") BackTrackPoints=", programControl::getBackTrackPoints(), ", BackTrack=", programControl::getBackTrack(),
            ", myFact=", myFact, '\n').
 
domains
    undoStackEntry = undoStackEntry(pointerTo{backtrackEntry} PtToBtEntry, returnAddress OriginalReturnAddress, predicate Undo).
 
class facts
    undoStack : undoStackEntry* := [].
    undoReturnAddress : pointer := erroneous.
 
class predicates
    initialize : () multi.
clauses
    initialize() :-
        PtToUndoBtEntry = uncheckedConvert(pointerTo{backtrackEntry}, programControl::getBackTrack()),
        backtrackEntry(:ReturnAddress = UndoReturnAddress | _) == memory::get(PtToUndoBtEntry),
        undoReturnAddress := UndoReturnAddress.
 
    initialize() :-
        initialize_1().
 
class predicates
    initialize_1 : () failure.
clauses
    initialize_1() :-
        show("b"),
        [UndoStackEntry | RestUndoStack] = undoStack,
        undoStack := RestUndoStack,
        StackMark = programControl::getBackTrack(),
        if uncheckedConvert(pointer, UndoStackEntry) < StackMark then
            initialize_1() %undo-action has been cut off
        else
            undoStackEntry(PtToBtEntry, OriginalReturnAddress, Undo) == UndoStackEntry,
            backtrackEntry(:ReturnAddress = ReturnAddress | _) == memory::get(PtToBtEntry),
            PtToReturnAddress = memory::mkPointerTo(ReturnAddress),
            memory::set(PtToReturnAddress, OriginalReturnAddress),
            Undo(),
            fail
        end if.
 
class predicates
    registerUndoAction : (programControl::stackMark, predicate Undo).
clauses
    registerUndoAction(StackMark, Undo) :-
        show("r"),
        PtToBtEntry = uncheckedConvert(pointerTo{backtrackEntry}, StackMark),
        backtrackEntry(:ReturnAddress = OriginalReturnAddress | _) == memory::get(PtToBtEntry),
        PtToReturnAddress = memory::mkPointerTo(OriginalReturnAddress),
        memory::set(PtToReturnAddress, undoReturnAddress),
        undoStack := [undoStackEntry(PtToBtEntry, OriginalReturnAddress, Undo) | undoStack].
 
class predicates
    test : ().
clauses
    test() :-
        show("1"),
        OldMyFact = myFact,
        myFact := "changed",
        registerUndoAction(programControl::getBackTrack(), {  :- myFact := OldMyFact }),
        show("2"),
        fail.
 
    test() :-
        show("3").
 
clauses
    run() :-
        initialize(),
        test(),
        !.

That runs without access violations in 32- and 64-bit. It outputs however not what I intended:

Code: Select all

(1) BackTrackPoints=2, BackTrack=00000000005FF528, myFact=original
(r) BackTrackPoints=2, BackTrack=00000000005FF4A8, myFact=changed
(2) BackTrackPoints=2, BackTrack=00000000005FF528, myFact=changed
(3) BackTrackPoints=1, BackTrack=00000000005FF588, myFact=changed

I suspect the reason, why it does not work, is that getBackTrack just returns the top of the stack. But on top of the stack is not necessarily a backtrack point. I suppose my ReturnAddress contains some bytes from the stack, but not actually the return address of the latest backtrack point. That true or is the construction not working for else reason?

If a construction like this could work out in principle, my question is: How to correctly grab the latest backtrack point and its return address?

[Martin Meyer]

Regarding the problem with the cut:

I understand the problem which you are pointing out. But I think we do not need to worry about it when inventing a solution to revert destructive changes on backtracking. The problem must (only) be handled when implementing a class to emulate reference variables on top of this solution. The plan to handle the problem there is:

When a binding is made, four things will be done: 1st the current stack position is recorded in variable StackPos. 2nd the destructive changes of the binding are performed. 3rd StackPos and a revert-operation, which reverts the destructive changes, are pushed on the trail. 4th the undo-action "execute the revert-operations popped off from the trail up to StackPos" is registered to be carried out on backtracking. If undo-actions are cut off, the trail stays unchanged. When backtracking further out, the revert-operations, which have been skipped by the cut, will be executed.

[Martin Meyer]

An add-on to the cut problem:

When backtracking further out, the revert-operations, which have been skipped by the cut, will be executed only if we backtrack over a backtrack point, at which another undo-action is registered.

But, as far as I see, that's just fine. Because we register undo-actions for every binding (or else change in the data structure which holds the reference variables' state). If we backtrack over backtrack points, at which no undo-actions have been registered, it means that we have not changed the reference variables' state on the way forth and thus we can stay with their state on way back.

[Thomas Linder Puls]

This code is wrong:

Code: Select all

       PtToUndoBtEntry = uncheckedConvert(pointerTo{backtrackEntry}, programControl::getBackTrack()),
        backtrackEntry(:ReturnAddress = UndoReturnAddress | _) == memory::get(PtToUndoBtEntry),

A functor domain is a pointer to the record, so you resolve pointer level too much, try this instead:

Code: Select all

       backtrackEntry(:ReturnAddress = UndoReturnAddress | _) = 
            uncheckedConvert(backtrackEntry, programControl::getBackTrack()),

[Martin Meyer]

Thank you! After applying your correction and some more it works already much better:

Code: Select all

    open core
 
domains
    backtrackEntry = backtrackEntry(bTop Next, tTopP LastTTop, unsignedNative EBP, returnAddress ReturnAddress).
    bTop = pointer.
    tTopP = pointer.
    returnAddress = pointer.
 
constants
    returnAddressOffSet : byteOffset = sizeOfDomain(bTop) + sizeOfDomain(tTopP) + sizeOfDomain(unsignedNative).
 
class facts
    myFact : string := "original".
 
class predicates
    show : (string Mark).
clauses
    show(Mark) :-
        stdIO::write("(", Mark, ") BackTrackPoints=", programControl::getBackTrackPoints(), ", BackTrack=", programControl::getBackTrack(),
            ", myFact=", myFact, '\n').
 
domains
    undoStackEntry = undoStackEntry(pointerTo{returnAddress} PtToReturnAddress, returnAddress OriginalReturnAddress, predicate Undo).
 
class facts
    undoStack : undoStackEntry* := [].
    undoReturnAddress : returnAddress := erroneous.
 
class predicates
    initialize : () multi.
clauses
    initialize() :-
        show("i"),
        backtrackEntry(:ReturnAddress = UndoReturnAddress | _) == uncheckedConvert(backtrackEntry, programControl::getBackTrack()),
        undoReturnAddress := UndoReturnAddress.
 
    initialize() :-
        initialize_1().
 
    initialize().
 
class predicates
    initialize_1 : () failure.
clauses
    initialize_1() :-
        show("b"),
        [UndoStackEntry | RestUndoStack] = undoStack,
        undoStack := RestUndoStack,
        StackMark = programControl::getBackTrack(),
        if uncheckedConvert(pointer, UndoStackEntry) < StackMark then
            initialize_1() %undo-action has been cut off
        else
            undoStackEntry(PtToReturnAddress, OriginalReturnAddress, Undo) == UndoStackEntry,
            memory::set(PtToReturnAddress, OriginalReturnAddress),
            Undo(),
            fail
        end if.
 
class predicates
    registerUndoAction : (programControl::stackMark, predicate Undo).
clauses
    registerUndoAction(StackMark, Undo) :-
        show("r"),
        BtEntry = uncheckedConvert(backtrackEntry, StackMark),
        backtrackEntry(:ReturnAddress = OriginalReturnAddress | _) == BtEntry,
        PtToReturnAddress = uncheckedConvert(pointerTo{returnAddress}, memory::pointerAdd(BtEntry, returnAddressOffSet)),
        memory::set(PtToReturnAddress, undoReturnAddress),
        undoStack := [undoStackEntry(PtToReturnAddress, OriginalReturnAddress, Undo) | undoStack].
 
class predicates
    test : ().
clauses
    test() :-
        show("1"),
        OldMyFact = myFact,
        myFact := "changed",
        registerUndoAction(programControl::getBackTrack(), {  :- myFact := OldMyFact }),
        show("2"),
        fail.
 
    test() :-
        show("3").
 
clauses
    run() :-
        initialize(),
        test(),
        !.

In 32-bit mode it outputs:

Code: Select all

(i) BackTrackPoints=1, BackTrack=0019FA94, myFact=original
(1) BackTrackPoints=2, BackTrack=0019FA68, myFact=original
(r) BackTrackPoints=2, BackTrack=0019FA38, myFact=changed
(2) BackTrackPoints=2, BackTrack=0019FA68, myFact=changed
(b) BackTrackPoints=2, BackTrack=0019FA44, myFact=changed
(3) BackTrackPoints=1, BackTrack=0019FA94, myFact=original

But in 64-bit something goes wrong and the output is:

Code: Select all

(i) BackTrackPoints=1, BackTrack=00000000005FF598, myFact=original
(1) BackTrackPoints=2, BackTrack=00000000005FF538, myFact=original
(r) BackTrackPoints=2, BackTrack=00000000005FF4B8, myFact=changed
(2) BackTrackPoints=2, BackTrack=00000000005FF538, myFact=changed
(3) BackTrackPoints=1, BackTrack=00000000005FF598, myFact=changed

Evident question is: Why 64-bit makes a difference and how to fix it?

Moreover I am still not sure whether the run stack and the backtrack stack are two different stacks or one and the same. I suspect that getBackTrack just returns the top of the run stack and in registerUndoAction I should walk down stack entries until I reach a backtrack point. Is that true and if yes, how to recognize a backtrack point entry and how to determine the size of non-backtrack-point entries?

[Martin Meyer]

The reason, why I suppose getBackTrack just returns the top of the run stack, is that:

Code: Select all

class predicates
    test : ().
clauses
    test() :-
        stdIO::write("2: ", programControl::getBackTrack(), '\n').
 
clauses
    run() :-
        stdIO::write("1: ", programControl::getBackTrack(), '\n'),
        test(),
        stdIO::write("3: ", programControl::getBackTrack(), '\n').

outputs (in 32-bit and in 64-bit it's similary):

Code: Select all

1: 0019FAC8
2: 0019FAB4
3: 0019FAC8

There is no backtrack point involved here. If getBackTrack would return a pointer to a separate backtrack stack, it should return the same value in all of the three places.

[Thomas Linder Puls]

I should probably have been more awake, but ...

The predicate getBackTrack is unusable for the things you are dealing with.

The correct predicate is getBackTrackTop, which is not defined in PFC, but can be defined like this:

Code: Select all

class predicates
    getBackTrackTop : () -> bTop BTop language c as linknames_vipKernel::getBackTrackTop.
 
resolve
    getBackTrackTop externally

Besides this you have at some point in time reversed the order of the two last arguments of backtrackEntry. This together with the wrong predicate makes everything "nonsense".

Here is an update of your program:

Code: Select all

implement main
    open core
 
domains
    backtrackEntry = backtrackEntry(bTop Next, tTopP LastTTop, returnAddress ReturnAddress, handle EBP).
    bTop = pointer.
    tTopP = pointer.
    returnAddress = pointer.
 
constants
    returnAddressOffSet : byteOffset = sizeOfDomain(bTop) + sizeOfDomain(tTopP).
 
class facts
    myFact : string := "original".
 
class predicates
    getBackTrackTop : () -> bTop BTop language c as linknames_vipKernel::getBackTrackTop.
 
resolve
    getBackTrackTop externally
 
class predicates
    show : (string Mark).
clauses
    show(Mark) :-
        BTCount = programControl::getBackTrackPoints(),
        stdio::writef("(%s) BackTrackPoints=%, myFact=%\n", Mark, BTCount, myFact),
        BTop = getBackTrackTop(),
        showBS(BTop).
 
class predicates
    showBS : (bTop BE).
clauses
    showBS(BE) :-
        if not(memory::isNull(BE)) then
            Entry = uncheckedConvert(backtrackEntry, BE),
            stdio::writef("    R: %\n", Entry),
            backtrackEntry(Next | _) = Entry,
            showBS(Next)
        end if.
 
domains
    undoStackEntry = undoStackEntry(pointerTo{returnAddress} PtToReturnAddress, returnAddress OriginalReturnAddress, predicate Undo).
 
class facts
    undoStack : undoStackEntry* := [].
    undoReturnAddress : returnAddress := erroneous.
 
class predicates
    initialize : () multi.
clauses
    initialize() :-
        show("i"),
        backtrackEntry(:ReturnAddress = UndoReturnAddress | _) = uncheckedConvert(backtrackEntry, getBackTrackTop()),
        undoReturnAddress := UndoReturnAddress.
 
    initialize() :-
        initialize_1().
 
    initialize().
 
class predicates
    initialize_1 : () failure.
clauses
    initialize_1() :-
        show("b"),
        [UndoStackEntry | RestUndoStack] = undoStack,
        undoStack := RestUndoStack,
        BTop = getBackTrackTop(),
        if uncheckedConvert(pointer, UndoStackEntry) < BTop then
            initialize_1() %undo-action has been cut off
        else
            undoStackEntry(PtToReturnAddress, OriginalReturnAddress, Undo) == UndoStackEntry,
            memory::set(PtToReturnAddress, OriginalReturnAddress),
            Undo(),
            fail
        end if.
 
class predicates
    registerUndoAction : (bTop, predicate Undo).
clauses
    registerUndoAction(BTop, Undo) :-
        show("r"),
        BtEntry = uncheckedConvert(backtrackEntry, BTop),
        backtrackEntry(:ReturnAddress = OriginalReturnAddress | _) == BtEntry,
        PtToReturnAddress = uncheckedConvert(pointerTo{returnAddress}, memory::pointerAdd(BtEntry, returnAddressOffSet)),
        memory::set(PtToReturnAddress, undoReturnAddress),
        undoStack := [undoStackEntry(PtToReturnAddress, OriginalReturnAddress, Undo) | undoStack].
implement main
    open core
 
domains
    backtrackEntry = backtrackEntry(bTop Next, tTopP LastTTop, returnAddress ReturnAddress, handle EBP).
    bTop = pointer.
    tTopP = pointer.
    returnAddress = pointer.
 
constants
    returnAddressOffSet : byteOffset = sizeOfDomain(bTop) + sizeOfDomain(tTopP).
 
class facts
    myFact : string := "original".
 
class predicates
    getBackTrackTop : () -> bTop BTop language c as linknames_vipKernel::getBackTrackTop.
 
resolve
    getBackTrackTop externally
 
class predicates
    show : (string Mark).
clauses
    show(Mark) :-
        BTCount = programControl::getBackTrackPoints(),
        stdio::writef("(%s) BackTrackPoints=%, myFact=%\n", Mark, BTCount, myFact),
        BTop = getBackTrackTop(),
        showBS(BTop).
 
class predicates
    showBS : (bTop BE).
clauses
    showBS(BE) :-
        if not(memory::isNull(BE)) then
            Entry = uncheckedConvert(backtrackEntry, BE),
            stdio::writef("    R: %\n", Entry),
            backtrackEntry(Next | _) = Entry,
            showBS(Next)
        end if.
 
domains
    undoStackEntry = undoStackEntry(pointerTo{returnAddress} PtToReturnAddress, returnAddress OriginalReturnAddress, predicate Undo).
 
class facts
    undoStack : undoStackEntry* := [].
    undoReturnAddress : returnAddress := erroneous.
 
class predicates
    initialize : () multi.
clauses
    initialize() :-
        show("i"),
        backtrackEntry(:ReturnAddress = UndoReturnAddress | _) = uncheckedConvert(backtrackEntry, getBackTrackTop()),
        undoReturnAddress := UndoReturnAddress.
 
    initialize() :-
        initialize_1().
 
    initialize().
 
class predicates
    initialize_1 : () failure.
clauses
    initialize_1() :-
        show("b"),
        [UndoStackEntry | RestUndoStack] = undoStack,
        undoStack := RestUndoStack,
        BTop = getBackTrackTop(),
        if uncheckedConvert(pointer, UndoStackEntry) < BTop then
            initialize_1() %undo-action has been cut off
        else
            undoStackEntry(PtToReturnAddress, OriginalReturnAddress, Undo) == UndoStackEntry,
            memory::set(PtToReturnAddress, OriginalReturnAddress),
            Undo(),
            fail
        end if.
 
class predicates
    registerUndoAction : (bTop, predicate Undo).
clauses
    registerUndoAction(BTop, Undo) :-
        show("r"),
        BtEntry = uncheckedConvert(backtrackEntry, BTop),
        backtrackEntry(:ReturnAddress = OriginalReturnAddress | _) == BtEntry,
        PtToReturnAddress = uncheckedConvert(pointerTo{returnAddress}, memory::pointerAdd(BtEntry, returnAddressOffSet)),
        memory::set(PtToReturnAddress, undoReturnAddress),
        undoStack := [undoStackEntry(PtToReturnAddress, OriginalReturnAddress, Undo) | undoStack].
 
class predicates
    test : ().
clauses
    test() :-
        show("1"),
        OldMyFact = myFact,
        myFact := "changed",
        registerUndoAction(getBackTrackTop(), {  :- myFact := OldMyFact }),
        show("2"),
        fail.
 
    test() :-
        show("3").
 
clauses
    run() :-
        stdio::outputStream:allowNullPointers := true,
        initialize(),
        test(),
        !.
 
end implement main

Disclaimer I don't think this is a good idea. In fact, I am almost certain that things (one or the other) will break down. Because you have broken an invariant (that some code relies on) about backtrack entries, namely that they exist on the run-time stack and is in order on that stack. Your cheating entry is far too deep in the stack. Predicates like cutBackTrack (for example) uses a stack mark to perform its actions, and with your very deep entry placed early in the stack I believe it will stop cutting too soon (cut too few entries).

Furthermore the backtrack mechanism has been updated (mentioned previously) for the next release (vip 11).

[Martin Meyer]

Thanks a lot to you for correcting my code and sorry for late reply!

Of course, code injection via stack manipulation is a hack, but as far as I could see, it worked well. I made a slightly larger demo that solves the eight queens puzzle. The chess board is stored in a fact variable of object type array2B{@ItemType}. That object type is the same as array2M{@ItemType}, but it reverts its changes on backtracking:

Code: Select all

class btReversion
    open core
 
predicates
    initialize_mt : () multi.
 
predicates
    addUndoAction : (predicate Undo).
 
end class btReversion
 
%---
 
implement btReversion
    open core
 
domains
    backtrackEntry = backtrackEntry(bTop Next, tTopP LastTTop, returnAddress ReturnAddress, handle EBP).
    bTop = pointer.
    tTopP = pointer.
    returnAddress = pointer.
 
constants
    returnAddressOffSet : byteOffset = sizeOfDomain(bTop) + sizeOfDomain(tTopP).
 
class predicates
    getBackTrackTop : () -> bTop BTop language c as linknames_vipKernel::getBackTrackTop.
 
resolve
    getBackTrackTop externally
 
domains
    trailEntry =
        trailEntry(
            programControl::stackMark StackMark,
            pointerTo{returnAddress} PtToReturnAddress,
            returnAddress OriginalReturnAddress,
            predicate Undo).
 
class facts
    trail : trailEntry* := [].
    execUndoAddress : returnAddress := erroneous.
 
clauses
    initialize_mt() :-
        backtrackEntry(:ReturnAddress = ExecUndoAddress | _) = uncheckedConvert(backtrackEntry, getBackTrackTop()),
        execUndoAddress := ExecUndoAddress.
 
    initialize_mt() :-
        execUndo_fl().
 
    initialize_mt() :-
        effectReturnToOriginalAddress().
 
class predicates
    effectReturnToOriginalAddress : () failure.
clauses
    effectReturnToOriginalAddress() :-
        fail.
 
class predicates
    execUndo_fl : () failure.
clauses
    execUndo_fl() :-
        [trailEntry(StackMark, PtToReturnAddress, OriginalReturnAddress, Undo) | RestTrail] = trail,
        StackMark <= programControl::getBackTrack(),
        memory::set(PtToReturnAddress, OriginalReturnAddress),
        trail := RestTrail,
        Undo(),
        execUndo_fl().
 
clauses
    addUndoAction(Undo) :-
        BTop = getBackTrackTop(),
        if not(memory::isNull(BTop)) then
            StackMark = programControl::getBackTrack(),
            BtEntry = uncheckedConvert(backtrackEntry, BTop),
            backtrackEntry(:ReturnAddress = OriginalReturnAddress | _) == BtEntry,
            PtToReturnAddress = uncheckedConvert(pointerTo{returnAddress}, memory::pointerAdd(BtEntry, returnAddressOffSet)),
            memory::set(PtToReturnAddress, execUndoAddress),
            trail := [trailEntry(StackMark, PtToReturnAddress, OriginalReturnAddress, Undo) | trail]
        end if.
 
end implement btReversion
 
%===
 
interface array2B{@ItemType} supports array2M{@ItemType}
end interface array2B
 
%---
 
class array2B{@ItemType} : array2B{@ItemType}
    open core
 
constructors
    new : (positive SizeX, positive SizeY).
 
constructors
    newInitialize : (positive SizeX, positive SizeY, @ItemType InitValue).
 
constructors
    newPointer : (pointer Data, positive SizeX, positive SizeY).
 
end class array2B
 
%---
 
implement array2B{@ItemType}
    open core, btReversion
 
delegate
    isEmpty to ar2M,
    sizeX to ar2M,
    sizeY to ar2M,
    tryGetFirst/0-> to ar2M,
    get/1-> to ar2M,
    get/2-> to ar2M,
    tryGet/1-> to ar2M,
    get_optional/1-> to ar2M,
    get_default/2-> to ar2M,
    get_defaultLazy/2-> to ar2M,
    getAll_nd/0-> to ar2M,
    getKey_nd/0-> to ar2M,
    getValue_nd/0-> to ar2M,
    upFrom_nd/1-> to ar2M,
    downFrom_nd/1-> to ar2M,
    getFromTo_nd/2-> to ar2M,
    keyList to ar2M,
    valueList to ar2M,
    asList to ar2M,
    contains/1 to ar2M,
    createCopy/0-> to ar2M,
    clone/0-> to ar2M,
    clear/0 to ar2M,
    tryRemoveFirst/0-> to ar2M,
    removeKey/1 to ar2M,
    removeKeyList/1 to ar2M,
    removeKeyCollection/1 to ar2M,
    remove/1 to ar2M,
    removeList/1 to ar2M,
    removeCollection/1 to ar2M,
    presenter/0-> to ar2M
 
facts
    ar2M : array2M{@ItemType}.
 
clauses
    new(SizeX, SizeY) :-
        ar2M := array2M::new(SizeX, SizeY).
 
clauses
    newInitialize(SizeX, SizeY, Init) :-
        ar2M := array2M::newInitialize(SizeX, SizeY, Init).
 
clauses
    newPointer(Buffer, SizeX, SizeY) :-
        ar2M := array2M::newPointer(Buffer, SizeX, SizeY).
 
    set(X, Y, Value) :-
        OldValue = ar2M:get(X, Y),
        ar2M:set(X, Y, Value),
        addUndoAction({  :- ar2M:set(X, Y, OldValue) }).
 
clauses
    set(tuple(X, Y), Value) :-
        set(X, Y, Value).
 
clauses
    set_optional(tuple(X, Y), some(Value)) :-
        set(X, Y, Value).
 
    set_optional(XY, none) :-
        ar2M:set_optional(XY, none). %raises exception
 
clauses
    insert(tuple(XY, Value)) :-
        set(XY, Value).
 
clauses
    insertList(TupleList) :-
        OldAr2M = ar2M:createCopy(),
        ar2M:insertList(TupleList),
        addUndoAction({  :- ar2M := OldAr2M }).
 
clauses
    insertCollection(TupleCollection) :-
        OldAr2M = ar2M:createCopy(),
        ar2M:insertCollection(TupleCollection),
        addUndoAction({  :- ar2M := OldAr2M }).
 
clauses
    insertEnumerator(TupleEnum_nd) :-
        OldAr2M = ar2M:createCopy(),
        ar2M:insertEnumerator(TupleEnum_nd),
        addUndoAction({  :- ar2M := OldAr2M }).
 
end implement array2B
 
%===
 
implement main
    open core
 
constants
    boardSize : positive = 8.
 
class facts
    boardB : array2B{unsigned8} := array2B::new(boardSize, boardSize).
    solutionCount : positive := 0.
 
clauses
    run() :-
        btReversion::initialize_mt(),
        stdIO::nl(),
        solve_nd(0, 0),
        fail.
 
    run() :-
        stdIO::writeF("Total solutions for a %ux%u board: %u.\n", boardSize, boardSize, solutionCount).
 
class predicates
    show : ().
clauses
    show() :-
        stdIO::writeF("Solution %u:\n", solutionCount),
        foreach Y = std::downTo(boardSize - 1, 0) do
            stdIO::write(Y),
            foreach X = std::fromTo(0, boardSize - 1) do
                Field = if boardB:get(X, Y) = 0 then '.' else 'Q' end if,
                stdIO::write(Field)
            end foreach,
            stdIO::nl()
        end foreach,
        stdIO::write(' '),
        foreach X = std::fromTo(0, boardSize - 1) do
            stdIO::write(string::getCharFromValue(string::getCharValue('a') + X))
        end foreach,
        stdIO::nl(),
        stdIO::nl().
 
class predicates
    solve_nd : (positive QueenX, positive QueenY) nondeterm.
clauses
    solve_nd(QueenX, QueenY) :-
        boardB:set(QueenX, QueenY, 1),
        not(canCaptureHorizontal(0, QueenX, QueenY)),
        not(canCaptureDiagonal1(0, QueenX, QueenY)),
        not(canCaptureDiagonal2(0, QueenX, QueenY)),
        if QueenX = boardSize - 1 then
            solutionCount := solutionCount + 1,
            show()
        else
            solve_nd(QueenX + 1, 0)
        end if.
 
    solve_nd(QueenX, QueenY) :-
        QueenY < boardSize - 1,
        solve_nd(QueenX, QueenY + 1).
 
class predicates
    canCaptureHorizontal : (positive N, positive QueenX, positive QueenY) determ.
clauses
    canCaptureHorizontal(N, QueenX, QueenY) :-
        N < QueenX,
        if boardB:get(N, QueenY) = 0 then
            canCaptureHorizontal(N + 1, QueenX, QueenY)
        end if.
 
class predicates
    canCaptureDiagonal1 : (positive N, positive QueenX, positive QueenY) determ.
clauses
    canCaptureDiagonal1(N, QueenX, QueenY) :-
        N < QueenX,
        N < QueenY,
        N1 = N + 1,
        if boardB:get(QueenX - N1, QueenY - N1) = 0 then
            canCaptureDiagonal1(N1, QueenX, QueenY)
        end if.
 
class predicates
    canCaptureDiagonal2 : (positive N, positive QueenX, positive QueenY) determ.
clauses
    canCaptureDiagonal2(N, QueenX, QueenY) :-
        N < QueenX,
        N1 = N + 1,
        N1 < boardSize - QueenY,
        if boardB:get(QueenX - N1, QueenY + N1) = 0 then
            canCaptureDiagonal2(N1, QueenX, QueenY)
        end if.
 
end implement main

By contrast with my before post I have changed the effect of cuts on the registered undo predicates. A cut will now only delay execution of undo predicates, but not skip them. That should be the same behavior as cuts had on variables of reference domains. Having that changed, I found no problem using cutBackTrack. I tested:

Code: Select all

class btReversion  %same as above
    open core
 
predicates
    initialize_mt : () multi.
 
predicates
    addUndoAction : (predicate Undo).
 
end class btReversion
 
%---
 
implement btReversion
    open core
 
domains
    backtrackEntry = backtrackEntry(bTop Next, tTopP LastTTop, returnAddress ReturnAddress, handle EBP).
    bTop = pointer.
    tTopP = pointer.
    returnAddress = pointer.
 
constants
    returnAddressOffSet : byteOffset = sizeOfDomain(bTop) + sizeOfDomain(tTopP).
 
class predicates
    getBackTrackTop : () -> bTop BTop language c as linknames_vipKernel::getBackTrackTop.
 
resolve
    getBackTrackTop externally
 
domains
    trailEntry =
        trailEntry(
            programControl::stackMark StackMark,
            pointerTo{returnAddress} PtToReturnAddress,
            returnAddress OriginalReturnAddress,
            predicate Undo).
 
class facts
    trail : trailEntry* := [].
    execUndoAddress : returnAddress := erroneous.
 
clauses
    initialize_mt() :-
        backtrackEntry(:ReturnAddress = ExecUndoAddress | _) = uncheckedConvert(backtrackEntry, getBackTrackTop()),
        execUndoAddress := ExecUndoAddress.
 
    initialize_mt() :-
        execUndo_fl().
 
    initialize_mt() :-
        effectReturnToOriginalAddress().
 
class predicates
    effectReturnToOriginalAddress : () failure.
clauses
    effectReturnToOriginalAddress() :-
        fail.
 
class predicates
    execUndo_fl : () failure.
clauses
    execUndo_fl() :-
        [trailEntry(StackMark, PtToReturnAddress, OriginalReturnAddress, Undo) | RestTrail] = trail,
        StackMark <= programControl::getBackTrack(),
        memory::set(PtToReturnAddress, OriginalReturnAddress),
        trail := RestTrail,
        Undo(),
        execUndo_fl().
 
clauses
    addUndoAction(Undo) :-
        BTop = getBackTrackTop(),
        if not(memory::isNull(BTop)) then
            StackMark = programControl::getBackTrack(),
            BtEntry = uncheckedConvert(backtrackEntry, BTop),
            backtrackEntry(:ReturnAddress = OriginalReturnAddress | _) == BtEntry,
            PtToReturnAddress = uncheckedConvert(pointerTo{returnAddress}, memory::pointerAdd(BtEntry, returnAddressOffSet)),
            memory::set(PtToReturnAddress, execUndoAddress),
            trail := [trailEntry(StackMark, PtToReturnAddress, OriginalReturnAddress, Undo) | trail]
        end if.
 
end implement btReversion
 
%===
 
implement main
    open btReversion
 
clauses
    run() :-
        btReversion::initialize_mt(),
        stdIO::nl(),
        test1(),
        fail.
 
    run().
 
class predicates
    test1 : ().
clauses
    test1() :-
        stdIO::write("1 begin\n"),
        addUndoAction({  :- stdIO::write("1 undo\n") }),
        StackMark = programControl::getBackTrack(),
        test2(StackMark),
        stdIO::write("1 fail\n"),
        fail.
 
    test1() :-
        stdIO::write("1 end\n").
 
class predicates
    test2 : (programControl::stackMark StackMark).
clauses
    test2(StackMark) :-
        stdIO::write("2 begin\n"),
        addUndoAction({  :- stdIO::write("2 undo\n") }),
        test3(StackMark),
        stdIO::write("2 fail\n"),
        fail.
 
    test2(_StackMark) :-
        stdIO::write("2 end\n").
 
class predicates
    test3 : (programControl::stackMark StackMark).
clauses
    test3(StackMark) :-
        stdIO::write("3 begin\n"),
        addUndoAction({  :- stdIO::write("3 undo\n") }),
        programControl::cutBackTrack(StackMark), %compare output with this line outcommented
        stdIO::write("3 fail\n"),
        fail.
 
    test3(_StackMark) :-
        stdIO::write("3 end\n").
 
end implement main

With the cutBackTrack outcommented it outputs:

Code: Select all

1 begin
2 begin
3 begin
3 fail
3 undo
3 end
2 fail
2 undo
2 end
1 fail
1 undo
1 end

While with the cutBackTrack activated it outputs:

Code: Select all

1 begin
2 begin
3 begin
3 fail
3 undo
2 undo
1 undo
1 end

Three questions:

1) Do you know of an example where the cheat in btReversion does not work?

2) In case the hack does actually work reliably, will there be a way to port it to next release VIP 11 (otherwise it doesn't make sense to develop code using it)?

3) Is there a way to implement getBackTrackTop in VIP 9 (cause I am still using VIP 9)?