Backtrack searches

abstract type BacktrackOracle end

Each Oracle<:BacktrackOracle should implement the following methods:

1. (bto::Oracle)(bts::BacktrackSearch)::Tuple{Bool, Bool}

which may access (read-only!) the internal fields of bts::BacktrackSearch:

• bts.automaton::Automaton is the explored automaton,
• bts.history contains d+1 states (including the initial one) describing the currently explored branch,
• bts.path contains the tracing word of bts.history (of length d).

1. return_value(::Oracle, bts::BacktrackSearch) what should be returned from

the backtrack search

1. Base.eltype(::Type{<:Oracle}, ::Type{<:BacktrackSearch}) the type of

objects returned by return_value.

The returned tuple (bcktrk, rtrn) indicate if the search should switch to the backtrack phase and if the currently visited node should be returned. Note: oracle will not be queried while backtracking so returning is not possible then.

If needed MyOracle<:BacktrackOracle may provide __reset!(bo::Oracle) function to reset (e.g. the performance counters) itself to the initial state.

BacktrackSearch{S, A<:Automaton{S}, O<:BacktrackOracle}
BacktrackSearch(at::Automaton, oracle::Oracle[, initial_st=initial(at)])

Struct for backtrack searches inside automatons.

The backtrack oracle must be provided as oracle<:BacktrackOracle. For more information see BacktrackOracle

Backtrack search starts from initial_st and uses oracle to prune branches.

Given bts::BacktrackSearch and a word w one may call

    (bts::BacktrackSearch)(w::AbstractWord)

to trace w through bts.automaton and start bts at the resulting state.

Examples

julia> rws = RWS_Example_237_abaB(4)
rewriting system with 8 active rules.
[...]

julia> R = knuthbendix(rws)
reduced, confluent rewriting system with 40 active rules.
[...]

julia> bts = BacktrackSearch(IndexAutomaton(R), IrreducibleWordsOracle());

julia> w = Word([1,2,1])

julia> for u in bts(w)
       println(w*u)
       end
1·2·1
1·2·1·2
1·2·1·2·1
1·2·1·2·1·2
1·2·1·2·1·2·1
[...]

ConfluenceOracle <: BacktrackOracle

Oracle for backtrack search to determine the confluence of a rewriting system.

ConfluenceOracle backtracks on too long paths (or shortcuts). the rules leading to critical pairs are returned.

LoopSearchOracle <: BacktrackOracle

Oracle for backtrack search to determine the finiteness of the language of irreducible words w.r.t. a rewriting system.

LoopSearchOracle backtracks on terminal states only and returns the a state σ which is contained in a loop witnessing the infiniteness of the language, see infiniteness_certificate.

As the oracle passes through all irreducible words (in order defined by the depth first search on the corresponding IndexAutomaton) it can be used to cheaply count those words and their maximal length (i.e. if finite).

After backtrack search those numbers can be read of the internal fields of the oracle (n_visited and max_depth).

IrreducibleWordsOracle <: BacktrackOracle

Oracle for backtrack search returning the irreducible words w.r.t. a rewriting system.

It is necessary to pass min_length and max_length to the constructor to control the length of the returned words.

The oracle backtracks on terminal states and returns the irreducible words.