deferred class BACKTRACKING

All features

This class is intended to explore structures that matches the and/or graph of BACKTRACKING_NODE. The alternatives have a context that is gotten and restored throught features 'get_context' and 'restore_context'.

See tutorial/backtracking for examples.

The instances of the BACKTRACKING childs are typically used through lines like the following ones that enumerate the solutions:

        from
           set_current_node(root)
           search_first
        until
           is_off
        loop
           ... -- do something
           search_next
        end
These features are declared to be bound to ANY but dont hesitate to change the type of the context to what your context is.

Direct parents

conformant parents

ABSTRACT_BACKTRACKING

non-conformant parents

BACKTRACKING_GLOBALS

Known children

conformant children

BACKTRACKING_REGULAR_EXPRESSION

Summary

exported features

internal

Common client features

Control of the exploration

Internal

Internal deferred

Specific to sequences

Specific to alternatives

internal: allocation and collection

the pools

Details

set_current_node (node: BACKTRACKING_NODE)

Set the next node of the BACKTRACKING_NODE graph to be evaluated.

ensure

  • definition: current_node = node

push_and (node: BACKTRACKING_NODE)

Pushes 'node' in front of the continuation path.

require

  • node_not_void: node /= Void

push_and_list (list: BACKTRACKING_NODE_AND_LIST)

Pushes 'list' in front of the continuation path.

require

  • list_not_void: list /= Void

push_or (node: BACKTRACKING_NODE)

Pushes 'node' in front of the possible alternatives.

require

  • node_not_void: node /= Void

push_or_list (list: BACKTRACKING_NODE_OR_LIST)

Pushes 'list' in front of the possible alternatives.

require

  • list_not_void: list /= Void

current_node: BACKTRACKING_NODE

Current node of the BACKTRACKING_NODE graph to be evaluated.

evaluate_current_state

That feature is called to evaluate the current state

search_first

Resets all and searchs the first solution. The current state must be set. It is the first state, the root of the search. When the feature returns, 'search_is_success' must be checked to know if a solution was found. When search_is_success=False, it means that there is no solution at all. Conversly, if search_is_success=True, then the first solution is found and 'search_next' can be called to get the next solution if it exists.

ensure

  • success_or_off: search_is_success and not is_off or is_off and not search_is_success

search_next

Searchs the next solution. When the feature returns, 'search_is_success' must be checked to know if a solution was found. When search_is_success=False at the end, it means that there is no more solution. Conversly, if search_is_success=True, then a solution is found and 'search_next' can be called again to get the next solution.

require

  • last_search_was_a_success: search_is_success

ensure

  • success_or_off: search_is_success and not is_off or is_off and not search_is_success

search_is_success: BOOLEAN

True when search is successfull

is_off: BOOLEAN

True when search is finished

ensure

  • definition: Result = not search_is_success

clear

Clears the current state to nothing.

ensure

  • cleared: is_cleared
  • no_solution: is_off

is_cleared: BOOLEAN

True if no partial data remain in the current state

ensure

  • no_solution_when_cleared: Result implies is_off

push_sequence (sequence: ABSTRACT_BACKTRACKING_SEQUENCE)

Pushs the 'sequence' in front of the continuation path.

require

  • sequence_not_void: sequence /= Void

ensure

  • is_on_top: top_sequence = sequence
  • is_first_continuation: current_continuation = sequence
  • previous_top_linked: top_sequence.previous = old top_sequence
  • previous_continuation_linked: top_sequence.continuation = old current_continuation

push_alternative (alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE)

Pushs the 'alternative' before the continuation path.

require

  • alternative_not_void: alternative /= Void

ensure

  • is_on_top: top_alternative = alternative
  • previous_top_linked: top_alternative.previous = old top_alternative
  • top_sequence_recorded: top_alternative.top_sequence = old top_sequence
  • continuation_recorded: top_alternative.continuation = old current_continuation

continue

Continues the exploration of the current path.

backtrack

Stops the exploration of the current path and tries to explore the next alternative path.

push_cut_point

Inserts a cut point into the continuation path. The inserted cut point records the current to of the alternatives.

cut

Removes the alternatives until the one recorded by the next cut point in the continuation path.

cut_all

Cuts all alternatives.

stop_search_loop: BOOLEAN

True if at the end of a search

search

Common search loop to search_first and serch_next

ensure

  • stop_search_loop

cut_until (alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE)

Cut all alternatives until 'alternative'. To cut an alternative is currently to remove it.

ensure

  • definition: top_alternative = alternative

deferred context_clear
deferred context_push
deferred context_restore
deferred context_restore_and_pop
deferred context_cut
top_sequence: ABSTRACT_BACKTRACKING_SEQUENCE

Stack of sequences represented by its top (can be Void)

current_continuation: ABSTRACT_BACKTRACKING_SEQUENCE

The current continuation path

pop_sequence

Removes the current sequence and replace it by the next sequence in the continuation path.

require

  • top_sequence /= Void
  • current_continuation /= Void

top_alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE

Stack of alternatives represented by its top (can be Void)

continue_alternative

Returns to the alternative on the top of the stack and put its saved continuation path as the current continuation path.

require

  • top_alternative /= Void

ensure

  • alternative_remain: top_alternative = old top_alternative

pop_alternative

Returns to the alternative on the top of the stack and put its saved continuation path as the current continuation path. Remove the alternative from the stack of alternatives. Same as 'continue_alternative' but also removes the alternative.

require

  • top_alternative /= Void

ensure

  • alternative_poped: top_alternative = old top_alternative.previous
  • top_sequence_restored: top_sequence = old top_alternative.top_sequence
  • continuation_restored: current_continuation = old top_alternative.continuation

remove_top_sequence

Removes the top sequence.

require

  • top_sequence /= Void

ensure

  • top_sequence = old top_sequence.previous

remove_top_alternative

Removes the top alternative.

require

  • top_alternative /= Void

ensure

  • top_alternative = old top_alternative.previous

pool_of_cut_points: ABSTRACT_BACKTRACKING_POOL_OF_CUT_POINT

Bank of cut points

pool_of_sequence: BACKTRACKING_POOL_OF_SEQUENCE
pool_of_sequence_list: BACKTRACKING_POOL_OF_SEQUENCE_LIST
pool_of_alternative: BACKTRACKING_POOL_OF_ALTERNATIVE
pool_of_alternative_list: BACKTRACKING_POOL_OF_ALTERNATIVE_LIST

Class invariant