Contains Subtree Constraint

src/HerbConstraints.jl

@@ -18,24 +18,28 @@ abstract type AbstractGrammarConstraint <: AbstractConstraint end
     abstract type AbstractLocalConstraint <: AbstractConstraint
 
 Abstract type representing all local constraints.
-Local constraints correspond to a specific (partial) [`AbstractRuleNode`](@ref) tree.
-Each local constraint contains a `path` that points to a specific location in the tree.
-The constraint is propagated on any tree manipulation at or below that `path`.
+Each local constraint contains a `path` that points to a specific location in the tree at which the constraint applies.
 
 Each local constraint should implement a [`propagate!`](@ref)-function.
 Inside the [`propagate!`](@ref) function, the constraint can use the following solver functions:
 - `remove!`: Elementary tree manipulation. Removes a value from a domain. (other tree manipulations are: `remove_above!`, `remove_below!`, `remove_all_but!`)
 - `deactivate!`: Prevent repropagation. Call this as soon as the constraint is satisfied.
 - `set_infeasible!`: Report a non-trivial inconsistency. Call this if the constraint can never be satisfied. An empty domain is considered a trivial inconsistency, such inconsistencies are already handled by tree manipulations.
 - `isfeasible`: Check if the current tree is still feasible. Return from the propagate function, as soon as infeasibility is detected.
-
-!!! warning
-    By default, [`AbstractLocalConstraint`](@ref)s are only propagated once.
-    Constraints that have to be propagated more frequently should subscribe to an event. This part of the solver is still WIP.
-    Currently, the solver supports only one type of subscription: `propagate_on_tree_manipulation!`.
 """
 abstract type AbstractLocalConstraint <: AbstractConstraint end
 
+
+"""
+    function get_priority(::AbstractLocalConstraint)
+
+Used to determine which constraint to propagate first in [`fix_point!`](@ref).
+Constraints with fast propagators and/or strong inference should be propagated first.
+"""
+function get_priority(::AbstractLocalConstraint)
+    return 0
+end
+
 include("csg_annotated/csg_annotated.jl")
 
 include("varnode.jl")
@@ -57,16 +61,19 @@ include("solver/domainutils.jl")
 
 include("patternmatch.jl")
 include("lessthanorequal.jl")
+include("makeequal.jl")
 
 include("localconstraints/local_forbidden.jl")
 include("localconstraints/local_ordered.jl")
 include("localconstraints/local_contains.jl")
+include("localconstraints/local_contains_subtree.jl")
 include("localconstraints/local_forbidden_sequence.jl")
 include("localconstraints/local_unique.jl")
 
 include("grammarconstraints/forbidden.jl")
 include("grammarconstraints/ordered.jl")
 include("grammarconstraints/contains.jl")
+include("grammarconstraints/contains_subtree.jl")
 include("grammarconstraints/forbidden_sequence.jl")
 include("grammarconstraints/unique.jl")
 
@@ -83,13 +90,15 @@ export
     Forbidden,
     Ordered,
     Contains,
+    ContainsSubtree,
     ForbiddenSequence,
     Unique,
 
     #local constraints
     LocalForbidden,
     LocalOrdered,
     LocalContains,
+    LocalContainsSubtree,
     LocalForbiddenSequence,
     LocalUnique,
 

src/grammarconstraints/contains_subtree.jl

@@ -0,0 +1,31 @@
+"""
+    ContainsSubtree <: AbstractGrammarConstraint
+
+This [`AbstractGrammarConstraint`] enforces that a given `subtree` appears in the program tree at least once.
+
+!!! warning:
+    This constraint can only be propagated by the UniformSolver
+"""
+struct ContainsSubtree <: AbstractGrammarConstraint
+    tree::AbstractRuleNode
+end
+
+function on_new_node(solver::UniformSolver, c::ContainsSubtree, path::Vector{Int})
+    if length(path) == 0
+        post!(solver, LocalContainsSubtree(path, c.tree, nothing, nothing))
+    end
+end
+
+function on_new_node(::GenericSolver, ::ContainsSubtree, ::Vector{Int}) end
+
+"""
+    check_tree(c::ContainsSubtree, tree::AbstractRuleNode)::Bool
+
+Checks if the given [`AbstractRuleNode`](@ref) tree abides the [`ContainsSubtree`](@ref) constraint.
+"""
+function check_tree(c::ContainsSubtree, tree::AbstractRuleNode)::Bool
+    if pattern_match(c.tree, tree) isa PatternMatchSuccess
+        return true
+    end
+    return any(check_tree(c, child) for child ∈ get_children(tree))
+end

src/lessthanorequal.jl

@@ -98,8 +98,6 @@ function make_less_than_or_equal!(
     guards::Vector{Tuple{AbstractHole, Int}}
 )::LessThanOrEqualResult
     @assert isfeasible(solver)
-    path1 = get_path(get_tree(solver), hole1)
-    path2 = get_path(get_tree(solver), hole2)
     @match (isfilled(hole1), isfilled(hole2)) begin
         (true, true) => begin
             #(RuleNode, RuleNode)
@@ -119,6 +117,7 @@ function make_less_than_or_equal!(
                     return LessThanOrEqualSoftFail(hole2)
                 end
             end
+            path2 = get_path(solver, hole2)
             remove_below!(solver, path2, get_rule(hole1))
             if !isfeasible(solver)
                 return LessThanOrEqualHardFail()
@@ -151,6 +150,7 @@ function make_less_than_or_equal!(
                     return LessThanOrEqualSoftFail(hole1)
                 end
             end
+            path1 = get_path(solver, hole1)
             remove_above!(solver, path1, get_rule(hole2))
             if !isfeasible(solver)
                 return LessThanOrEqualHardFail()
@@ -183,6 +183,8 @@ function make_less_than_or_equal!(
                     return LessThanOrEqualSoftFail(hole1, hole2)
                 end
             end
+            path1 = get_path(solver, hole1)
+            path2 = get_path(solver, hole2)
             # Example:
             # Before: {2, 3, 5} <= {1, 3, 4}
             # After:  {2, 3} <= {3, 4}
@@ -249,7 +251,7 @@ function make_less_than_or_equal!(
                     return result
                 elseif length(guards) == 1
                     # a single guard is involved, preventing equality on the guard prevents the hardfail on the tiebreak
-                    path = get_path(get_tree(solver), guards[1][1])
+                    path = get_path(solver, guards[1][1])
                     remove!(solver, path, guards[1][2])
                     return LessThanOrEqualSuccessLessThan()
                 else

src/localconstraints/local_contains_subtree.jl

@@ -0,0 +1,132 @@
+
+"""
+LocalContains
+
+Enforces that a given `tree` appears at or below the given `path` at least once.
+
+!!! warning:
+    This is a stateful constraint can only be propagated by the UniformSolver.
+    The `indices` and `candidates` fields should not be set by the user.
+"""
+mutable struct LocalContainsSubtree <: AbstractLocalConstraint
+	path::Vector{Int}
+    tree::AbstractRuleNode
+    candidates::Union{Vector{AbstractRuleNode}, Nothing}
+    indices::Union{StateSparseSet, Nothing}
+end
+
+"""
+    LocalContainsSubtree(path::Vector{Int}, tree::AbstractRuleNode)
+
+Enforces that a given `tree` appears at or below the given `path` at least once.
+"""
+function LocalContainsSubtree(path::Vector{Int}, tree::AbstractRuleNode)
+    LocalContainsSubtree(path, tree, Vector{AbstractRuleNode}(), nothing)
+end
+
+
+"""
+    function propagate!(::GenericSolver, ::LocalContainsSubtree)
+
+!!! warning:
+    LocalContainsSubtree uses stateful properties and can therefore not be propagated in the GenericSolver.
+    (The GenericSolver shares constraints among different states, so they cannot use stateful properties)
+"""
+function propagate!(::GenericSolver, ::LocalContainsSubtree)
+    throw(ArgumentError("LocalContainsSubtree cannot be propagated by the GenericSolver"))
+end
+
+
+"""
+    function propagate!(solver::UniformSolver, c::LocalContainsSubtree)
+
+Enforce that the `tree` appears at or below the `path` at least once.
+Nodes that can potentially become the target sub-tree are considered `candidates`.
+In case of multiple candidates, a stateful set of `indices` is used to keep track of active candidates.
+"""
+function propagate!(solver::UniformSolver, c::LocalContainsSubtree)
+    track!(solver, "LocalContainsSubtree propagation")
+    if isnothing(c.candidates)
+        # Initial propagation: pattern match all nodes, only store the candidates for re-propagation
+        c.candidates = Vector{AbstractRuleNode}()
+        for node ∈ get_nodes(solver)
+            @match pattern_match(c.tree, node) begin
+                ::PatternMatchHardFail => ()
+                ::PatternMatchSuccess => begin
+                    track!(solver, "LocalContainsSubtree satisfied (initial propagation)")
+                    deactivate!(solver, c);
+                    return
+                end
+                ::PatternMatchSoftFail || ::PatternMatchSuccessWhenHoleAssignedTo => push!(c.candidates, node)
+            end
+        end
+        n = length(c.candidates)
+        if n == 0
+            track!(solver, "LocalContainsSubtree inconsistency (initial propagation)")
+            set_infeasible!(solver)
+            return
+        elseif n == 1
+            @match make_equal!(solver, c.candidates[1], c.tree) begin
+                ::MakeEqualHardFail => begin
+                    @assert false "pattern_match failed to detect a hardfail"
+                end 
+                ::MakeEqualSuccess => begin 
+                    track!(solver, "LocalContainsSubtree deduction (initial)")
+                    deactivate!(solver, c);
+                    return
+                end 
+                ::MakeEqualSoftFail => begin
+                    track!(solver, "LocalContainsSubtree softfail (1 candidate) (initial)")
+                    return
+                end 
+            end
+        else
+            track!(solver, "LocalContainsSubtree softfail (>=2 candidates) (initial)")
+            c.indices = StateSparseSet(solver.sm, n)
+            return
+        end
+    else
+        # Re-propagation
+        if !isnothing(c.indices) && (size(c.indices) >= 2)
+            # Update the candidates by pattern matching them again
+            for i ∈ c.indices
+                match = pattern_match(c.candidates[i], c.tree)
+                @match match begin
+                    ::PatternMatchHardFail => remove!(c.indices, i)
+                    ::PatternMatchSuccess => begin
+                        track!(solver, "LocalContainsSubtree satisfied")
+                        deactivate!(solver, c);
+                        return
+                    end
+                    ::PatternMatchSoftFail || ::PatternMatchSuccessWhenHoleAssignedTo => ()
+                end
+            end
+        end
+        n = isnothing(c.indices) ? 1 : size(c.indices)
+        if n == 1
+            # If there is a single candidate remaining, set it equal to the target tree
+            index = isnothing(c.indices) ? 1 : findfirst(c.indices)
+            @match make_equal!(solver, c.candidates[index], c.tree) begin
+                ::MakeEqualHardFail => begin
+                    track!(solver, "LocalContainsSubtree inconsistency")
+                    set_infeasible!(solver)
+                    return
+                end 
+                ::MakeEqualSuccess => begin 
+                    track!(solver, "LocalContainsSubtree deduction")
+                    deactivate!(solver, c);
+                    return
+                end 
+                ::MakeEqualSoftFail => begin
+                    track!(solver, "LocalContainsSubtree softfail (1 candidate)")
+                    return
+                end 
+            end
+        elseif n == 0
+            track!(solver, "LocalContainsSubtree inconsistency")
+            set_infeasible!(solver)
+            return
+        end
+        track!(solver, "LocalContainsSubtree softfail (>=2 candidates)")
+    end
+end

src/localconstraints/local_forbidden_sequence.jl

@@ -93,11 +93,18 @@ function propagate!(solver::Solver, c::LocalForbiddenSequence)
         if (node isa RuleNode) || (node isa StateHole && isfilled(node))
             rule = get_rule(node)
             if (rule ∈ c.ignore_if)
+                #softfail (ignore if)
                 return
             elseif (rule == forbidden_rule)
                 i -= 1
             end
         elseif isnothing(forbidden_assignment)
+            for r ∈ c.ignore_if
+                if node.domain[r]
+                    #softfail (ignore if)
+                    return
+                end
+            end
             forbidden_assignment = (path_idx, forbidden_rule)
             i -= 1
         end

src/localconstraints/local_unique.jl

@@ -3,12 +3,16 @@
     LocalUnique <: AbstractLocalConstraint
 
 Enforces that a given `rule` appears at or below the given `path` at most once.
+In case of the UniformSolver, cache the list of `holes`, since no new holes can appear.
 """
 struct LocalUnique <: AbstractLocalConstraint
 	path::Vector{Int}
     rule::Int
+    holes::Vector{AbstractHole}
 end
 
+LocalUnique(path::Vector{Int}, rule::Int) = LocalUnique(path, rule, Vector{AbstractHole}())
+
 """
     function propagate!(solver::Solver, c::LocalUnique)
 
@@ -17,25 +21,30 @@ Uses a helper function to retrieve a list of holes that can potentially hold the
 If there is only a single hole that can potentially hold the target rule, that hole will be filled with that rule.
 """
 function propagate!(solver::Solver, c::LocalUnique)
-    node = get_node_at_location(solver, c.path)
-    holes = Vector{AbstractHole}()
-    count = _count_occurrences!(node, c.rule, holes)
     track!(solver, "LocalUnique propagation")
+    if (solver isa GenericSolver) | isempty(c.holes)
+        empty!(c.holes)
+        node = get_node_at_location(solver, c.path)
+        count = _count_occurrences!(node, c.rule, c.holes)
+    else
+        #only search for the target rule in the cached list of holes
+        count = _count_occurrences(c.holes, c.rule)
+    end
     if count >= 2
         set_infeasible!(solver)
         track!(solver, "LocalUnique inconsistency")
     elseif count == 1
-        if all(isuniform(hole) for hole ∈ holes)
+        if all(isuniform(hole) for hole ∈ c.holes)
             track!(solver, "LocalUnique deactivate")
             deactivate!(solver, c)
         end 
-        for hole ∈ holes
+        for hole ∈ c.holes
             deductions = 0
-            if hole.domain[c.rule] == true
-                path = get_path(get_tree(solver), hole)
+            if (hole.domain[c.rule] == true) && !isfilled(hole)
+                path = get_path(solver, hole)
                 remove!(solver, path, c.rule)
                 deductions += 1
-                track!(solver, "LocalUnique deduction ($(deductions))")
+                track!(solver, "LocalUnique deduction")
             end
         end
     end
@@ -76,3 +85,25 @@ function _count_occurrences!(node::AbstractRuleNode, rule::Int, holes::Vector{Ab
     end
     return count
 end
+
+"""
+    function _count_occurrences(holes::Vector{AbstractHole}, rule::Int)
+
+Counts the occurences of the `rule` in the cached list of `holes`.
+
+!!! warning: 
+    Stops counting if the rule occurs more than once. 
+    Counting beyond 2 is not needed for LocalUnique. 
+"""
+function _count_occurrences(holes::Vector{AbstractHole}, rule::Int)
+    count = 0
+    for hole ∈ holes
+        if isfilled(hole) && get_rule(hole) == rule
+            count += 1
+            if count >= 2
+                break
+            end
+        end
+    end
+    count
+end