Merge pull request #74 from kalmarek/mk/filter_rules

Enable filtering of added rules via knobs in Settings

src/buffer_pair.jl

@@ -2,37 +2,34 @@ struct RewritingBuffer{T,V<:AbstractVector}
     output::Words.BufferWord{T}
     input::Words.BufferWord{T}
     history::V
+
+    function RewritingBuffer{T}(
+        output::BW,
+        input::BW,
+        history::AbstractVector,
+    ) where {T,BW<:Words.BufferWord{T}}
+        return new{T,typeof(history)}(output, input, history)
+    end
+
+    function RewritingBuffer{T}(
+        output::BW,
+        input::BW,
+    ) where {T,BW<:Words.BufferWord{T}}
+        return new{T,Vector{Int}}(output, input)
+    end
+end
+
+function RewritingBuffer{T}() where {T}
+    BW = Words.BufferWord{T}
+    return RewritingBuffer{T}(one(BW), one(BW))
 end
 
 function RewritingBuffer{T}(history::AbstractVector) where {T}
     BW = Words.BufferWord{T}
-    return RewritingBuffer(one(BW), one(BW), history)
+    return RewritingBuffer{T}(one(BW), one(BW), history)
 end
 
 function Words.store!(rwbuf::RewritingBuffer, u::AbstractWord...)
     Words.store!(rwbuf.input, u...)
     return rwbuf
 end
-
-"""
-    function rewrite!(bp::BufferPair, rewriting; kwargs...)
-Rewrites word stored in `BufferPair` using `rewriting` object.
-
-To store a word in `bp`
-[`Words.store!`](@ref Words.store!(::BufferPair, ::AbstractWord))
-should be used.
-
-!!! warning
-    This implementation returns an instance of `Words.BufferWord` aliased with
-    the intenrals of `BufferPair`. You need to copy the return value if you
-    want to take the ownership.
-"""
-function rewrite!(bp::RewritingBuffer, rewriting; kwargs...)
-    v = if isempty(rewriting)
-        Words.store!(bp.output, bp.input)
-    else
-        rewrite!(bp.output, bp.input, rewriting; history = bp.history, kwargs...)
-    end
-    empty!(bp.input) # shifts bp._wWord pointers to the beginning of its storage
-    return v
-end

src/knuthbendix2.jl

@@ -65,7 +65,10 @@ function find_critical_pairs!(
     lhs₁, rhs₁ = r₁
     lhs₂, rhs₂ = r₂
     m = min(length(lhs₁), length(lhs₂)) - 1
-    W = word_type(stack)
+    if m > work.settings.max_length_overlap
+        m = work.settings.max_length_overlap
+        work.dropped_rules += 1
+    end
 
     # TODO: cache suffix automaton for lhs₁ to run this in O(m) (currently: O(m²))
     for b in suffixes(lhs₁, 1:m)
@@ -104,9 +107,13 @@ function deriverule!(
         u, v = pop!(stack)
         critical, (a, b) = _iscritical(work, rws, (u,), (v,))
         if critical
-            new_rule = Rule{W}(a => b)
-            push!(rws, new_rule)
-            deactivate_rules!(rws, stack, new_rule, work)
+            if isadmissible(a, b, work.settings)
+                new_rule = Rule{W}(a => b)
+                push!(rws, new_rule)
+                deactivate_rules!(rws, stack, new_rule, work)
+            else
+                work.dropped_rules += 1
+            end
         end
     end
 end

src/knuthbendix_base.jl

@@ -51,20 +51,14 @@ function knuthbendix(
         finish!(prog)
 
         if isreduced(rws_dc)
-            if !isconfluent(rws_dc) # sets the confluence flag
-                if settings.verbosity > 0
-                    @warn "The returned rws is not confluent"
-                end
-            end
-        else
-            if settings.verbosity > 0
-                @warn "the returned rws is not reduced"
+            confluent = isconfluent(rws_dc) # sets the confluence flag
+            if !confluent && settings.verbosity > 0
+                @warn "The returned rws is not confluent"
             end
         end
         return rws_dc
     catch e
         if e isa InterruptException
-            rethrow(e)
             @warn """Received user interrupt in Knuth-Bendix completion.
             Returned rws may be not confluent."""
             @info """Attempting to reduce the rewriting system.

src/knuthbendix_idxA.jl

@@ -75,7 +75,10 @@ function knuthbendix!(
             end
             @assert isempty(stack)
             stack, i_after = check_confluence!(stack, rws, idxA, work)
-            isempty(stack) && return rws # yey, we're done!
+            if isempty(stack)
+                __post!(rws, idxA, work)
+                return rws # yey, we're done!
+            end
             if settings.verbosity == 2
                 l = length(stack)
                 @info "confluence check failed: found $(l) new rule$(l==1 ? "" : "s")"
@@ -129,5 +132,40 @@ function knuthbendix!(
         end
         i += 1
     end
+
+    __post!(rws, idxA, work)
+
     return rws # so the rws is reduced here as well
 end
+
+function __post!(rws::AbstractRewritingSystem, rewriting, work::Workspace)
+    settings = work.settings
+    stack = Vector{Tuple{word_type(rws),word_type(rws)}}()
+
+    if work.dropped_rules > 0
+        @assert isempty(stack)
+        if settings.verbosity ≥ 2
+            @info "KnuthBendix completion has finished, however some rules were dropped; re-adding the defining rules"
+        end
+        for (lhs, rhs) in rws.rules_orig
+            Words.store!(work.rewrite1, lhs)
+            l = rewrite!(work.rewrite1, rewriting)
+            Words.store!(work.rewrite2, rhs)
+            r = rewrite!(work.rewrite2, rewriting)
+            if l ≠ r
+                push!(stack, (l, r))
+            end
+        end
+        if !isempty(stack)
+            if settings.verbosity ≥ 1
+                @warn "The rws does NOT represent the original congruence. Re-adding the missing rules."
+            end
+            rws = reduce!(settings.algorithm, rws, stack, work)
+        else
+            if settings.verbosity == 2
+                @info "Some rules have been dropped but the congruence is preserved."
+            end
+        end
+    end
+    return rws
+end

src/parsing.jl

@@ -26,6 +26,7 @@ struct KbmagRWS
     inverses::Vector{Int}
     equations::Vector{Pair{Vector{Int},Vector{Int}}}
     ordering::String
+    options::Dict{Symbol,Int}
     _str::String
 end
 
@@ -41,7 +42,7 @@ function Base.show(io::IO, ::MIME"text/plain", rws::KbmagRWS)
     println(io, ']', ',')
 
     print(io, lpad(:inverses, padlen), " := [")
-    join(io, rws.generatorOrder[rws.inverses], ',')
+    join(io, (i > 0 ? rws.generatorOrder[i] : ' ' for i in rws.inverses), ',')
     println(io, ']', ',')
 
     println(io, lpad(:ordering, padlen), " := \"", rws.ordering, "\"", ',')
@@ -188,6 +189,39 @@ function _parse_ordering(str::AbstractString)
     return strip(m[:ordering])
 end
 
+function _parse_opts(str::AbstractString)
+    options = Dict{Symbol,Int}()
+    r = _entry_regex(
+        "maxstoredlen",
+        "\\[\\s*(?<lhs_len>\\d+)\\s*,\\s*(?<rhs_len>\\d+)\\s*\\]",
+    )
+    m = match(r, str)
+    if !isnothing(m)
+        options[:max_length_lhs] = parse(Int, m[:lhs_len])
+        options[:max_length_rhs] = parse(Int, m[:rhs_len])
+    end
+
+    r = _entry_regex("tidyint", "(?<tidyint>\\d+)")
+    m = match(r, str)
+    if !isnothing(m)
+        options[:stack_size] = parse(Int, m[:tidyint])
+    end
+
+    r = _entry_regex("maxeqns", "(?<maxeqns>\\d+)")
+    m = match(r, str)
+    if !isnothing(m)
+        options[:max_rules] = parse(Int, m[:maxeqns])
+    end
+
+    r = _entry_regex("maxstates", "(?<maxstates>\\d+)")
+    m = match(r, str)
+    if !isnothing(m)
+        options[:max_states] = parse(Int, m[:maxstates])
+    end
+
+    return options
+end
+
 function parse_kbmag(input::AbstractString)
     rws_str = _validate_rws(input)
 
@@ -202,7 +236,16 @@ function parse_kbmag(input::AbstractString)
     end
     ordering = _parse_ordering(rws_str)
 
-    return KbmagRWS(Symbol.(gens), inverses, equations, ordering, rws_str)
+    options = _parse_opts(rws_str)
+
+    return KbmagRWS(
+        Symbol.(gens),
+        inverses,
+        equations,
+        ordering,
+        options,
+        rws_str,
+    )
 end
 
 RewritingSystem(rwsgap::KbmagRWS) = RewritingSystem{Word{UInt16}}(rwsgap)
@@ -221,3 +264,13 @@ function RewritingSystem{W}(rwsgap::KbmagRWS) where {W}
 
     return RewritingSystem(rwrules, ordering)
 end
+
+function Settings(rwsgap::KbmagRWS)
+    return Settings(
+        KBIndex();
+        (
+            opt for
+            opt in pairs(rwsgap.options) if first(opt) in fieldnames(Settings)
+        )...,
+    )
+end

src/rewriting.jl

@@ -1,3 +1,6 @@
+RewritingBuffer{T}(::Any) where {T} = RewritingBuffer{T}() # no history
+RewritingBuffer{T}(::IndexAutomaton{S}) where {T,S} = RewritingBuffer{T}(S[])
+
 """
     rewrite(u::AbstractWord, rewriting)
 Rewrites word `u` using the `rewriting` object. The object must implement
@@ -27,15 +30,13 @@ true
 function rewrite(
     u::W,
     rewriting,
-    vbuff = Words.BufferWord{T}(0, length(u)),
-    wbuff = Words.BufferWord{T}(0, length(u));
+    rwbuffer::RewritingBuffer = RewritingBuffer{T}(rewriting);
     kwargs...,
 ) where {T,W<:AbstractWord{T}}
-    isempty(rewriting) && return W(u, false)
-    Words.store!(wbuff, u)
-    v = rewrite!(vbuff, wbuff, rewriting; kwargs...)
-    res = W(v, false)
-    return res
+    isempty(rewriting) && return W(u)
+    Words.store!(rwbuffer, u)
+    v = rewrite!(rwbuffer, rewriting; kwargs...)
+    return W(v)
 end
 
 function rewrite!(v::AbstractWord, w::AbstractWord, A::Any; kwargs...)
@@ -149,7 +150,7 @@ See procedure `REWRITE_FROM_LEFT` from **Section 2.4**[^Sims1994], p. 66.
 function rewrite!(
     v::AbstractWord,
     w::AbstractWord,
-    rws::RewritingSystem;
+    rws::AbstractRewritingSystem;
     kwargs...,
 )
     v = empty!(v)
@@ -230,3 +231,35 @@ function rewrite!(
     end
     return v
 end
+
+"""
+    function rewrite!(bp::BufferPair, rewriting; kwargs...)
+Rewrites word stored in `BufferPair` using `rewriting` object.
+
+To store a word in `bp`
+[`Words.store!`](@ref Words.store!(::BufferPair, ::AbstractWord))
+should be used.
+
+!!! warning
+    This implementation returns an instance of `Words.BufferWord` aliased with
+    the intenrals of `BufferPair`. You need to copy the return value if you
+    want to take the ownership.
+"""
+function rewrite!(bp::RewritingBuffer, rewriting; kwargs...)
+    v = if isempty(rewriting)
+        Words.store!(bp.output, bp.input)
+    else
+        rewrite!(bp.output, bp.input, rewriting; kwargs...)
+    end
+    empty!(bp.input) # shifts bp._wWord pointers to the beginning of its storage
+    return v
+end
+function rewrite!(bp::RewritingBuffer, rewriting::IndexAutomaton; kwargs...)
+    v = if isempty(rewriting)
+        Words.store!(bp.output, bp.input)
+    else
+        rewrite!(bp.output, bp.input, rewriting; history = bp.history, kwargs...)
+    end
+    empty!(bp.input) # shifts bp._wWord pointers to the beginning of its storage
+    return v
+end

src/settings_workspace.jl

@@ -33,17 +33,16 @@ mutable struct Settings{CA<:CompletionAlgorithm}
     max_length_rhs::Int
     max_length_overlap::Int
     verbosity::Int
-    dropped_rules::Bool
     update_progress::Any
 
     function Settings(
         alg::CompletionAlgorithm;
         max_rules = 10000,
         stack_size = 100,
         confluence_delay = 10,
-        max_length_lhs = 100,
-        max_length_rhs = 1000,
-        max_length_overlap = 0,
+        max_length_lhs = typemax(Int),
+        max_length_rhs = typemax(Int),
+        max_length_overlap = typemax(Int),
         verbosity = 0,
     )
         return new{typeof(alg)}(
@@ -55,7 +54,6 @@ mutable struct Settings{CA<:CompletionAlgorithm}
             max_length_rhs,
             max_length_overlap,
             verbosity,
-            false,
             (args...) -> nothing,
         )
     end
@@ -77,22 +75,12 @@ function isadmissible(lhs, rhs, s::Settings)
     return length(lhs) ≤ s.max_length_lhs && length(rhs) ≤ s.max_length_rhs
 end
 
-function Base.filter!(sett::Settings, stack::AbstractVector)
-    to_delete = falses(length(stack))
-    for i in eachindex(stack)
-        to_delete[i] = !isadmissible(stack[i]..., sett)
-    end
-    if any(to_delete)
-        deleteat!(stack, to_delete)
-    end
-    return stack
-end
-
 mutable struct Workspace{CA,T,H,S<:Settings{CA}}
     rewrite1::RewritingBuffer{T,H}
     rewrite2::RewritingBuffer{T,H}
     settings::S
     confluence_timer::Int
+    dropped_rules::Int
 end
 
 function Workspace(word_t, history, settings::Settings)
@@ -102,6 +90,7 @@ function Workspace(word_t, history, settings::Settings)
         BP_t(deepcopy(history)),
         settings,
         0,
+        0,
     )
 end
 

test/automata.jl

@@ -1,5 +1,3 @@
-import KnuthBendix.Automata
-
 @testset "States" begin
     S = Automata.State{Symbol,UInt32,String}
     @test S() isa Automata.State