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)?