From 1da5aa13a2c07b07bfbcfd84a96dcbf4fe6a4198 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Tue, 7 May 2024 20:41:33 +0200
Subject: [PATCH 01/20] Add Base.:(==) for StateHoles

---
 src/solver/uniform_solver/state_hole.jl | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/solver/uniform_solver/state_hole.jl b/src/solver/uniform_solver/state_hole.jl
index e8f3f46..3d40690 100644
--- a/src/solver/uniform_solver/state_hole.jl
+++ b/src/solver/uniform_solver/state_hole.jl
@@ -84,6 +84,27 @@ end
 HerbCore.get_children(hole::StateHole) = hole.children
 
 
+function Base.:(==)(A::StateHole, B::StateHole)
+	isfilled(A) && isfilled(B) &&
+    	(get_rule(A) == get_rule(B)) && 
+		(length(A.children) == length(B.children)) &&
+		all(isequal(a, b) for (a, b) in zip(A.children, B.children))
+end
+
+function Base.:(==)(A::RuleNode, B::StateHole)
+	isfilled(B) &&
+    	(get_rule(A) == get_rule(B)) && 
+		(length(A.children) == length(B.children)) &&
+		all(isequal(a, b) for (a, b) in zip(A.children, B.children))
+end
+
+function Base.:(==)(A::StateHole, B::RuleNode)
+	isfilled(A) &&
+    	(get_rule(A) == get_rule(B)) && 
+		(length(A.children) == length(B.children)) &&
+		all(isequal(a, b) for (a, b) in zip(A.children, B.children))
+end
+
 """
 	freeze_state(hole::StateHole)::RuleNode
 

From e385ad9b1fac72d9f7a110088b5eee6e87892435 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Tue, 7 May 2024 20:42:10 +0200
Subject: [PATCH 02/20] Add test for Base.:(==)

---
 test/test_state_fixed_shaped_hole.jl | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/test/test_state_fixed_shaped_hole.jl b/test/test_state_fixed_shaped_hole.jl
index 5dcf063..a9a8282 100644
--- a/test/test_state_fixed_shaped_hole.jl
+++ b/test/test_state_fixed_shaped_hole.jl
@@ -66,4 +66,25 @@
         hole = HerbConstraints.StateHole(HerbConstraints.StateManager(), UniformHole(BitVector((0, 0, 0)), []))
         @test isfilled(hole) == false
     end
+
+    @testset "(==)" begin
+        sm = HerbConstraints.StateManager()
+        node = RuleNode(3, [
+            RuleNode(2),
+            RuleNode(1)
+        ])
+        statehole = StateHole(sm, node)
+        @test node == statehole
+        @test statehole == node
+        @test statehole == StateHole(sm, node)
+
+        node2 = RuleNode(3, [
+            RuleNode(1),
+            RuleNode(1)
+        ])
+        statehole2 = StateHole(sm, node2)
+        @test node != statehole2
+        @test statehole2 != node
+        @test statehole != statehole2
+    end
 end

From f370cb33e143c9468afe6cc018b064e1300aed57 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Tue, 7 May 2024 20:42:44 +0200
Subject: [PATCH 03/20] Fix SolverStatistics constructor

---
 src/solver/uniform_solver/uniform_solver.jl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solver/uniform_solver/uniform_solver.jl b/src/solver/uniform_solver/uniform_solver.jl
index 8ecf672..966ab91 100644
--- a/src/solver/uniform_solver/uniform_solver.jl
+++ b/src/solver/uniform_solver/uniform_solver.jl
@@ -31,7 +31,7 @@ function UniformSolver(grammar::AbstractGrammar, fixed_shaped_tree::AbstractRule
     fix_point_running = false
     statistics = @match with_statistics begin
         ::SolverStatistics => with_statistics
-        ::Bool => with_statistics ? SolverStatistics("UniformSolver") : nothing
+        ::Bool => with_statistics ? SolverStatistics() : nothing
         ::Nothing => nothing
     end
     solver = UniformSolver(grammar, sm, tree, path_to_node, node_to_path, isactive, canceledconstraints, true, schedule, fix_point_running, statistics)

From a9d61d6e50c8d56de9028532a9799aef6591b0f8 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Tue, 7 May 2024 20:43:12 +0200
Subject: [PATCH 04/20] Add `make_equal!` tree manipulation

---
 src/makeequal.jl       | 133 +++++++++++++++++++++++++++++++++++++++++
 test/test_makeequal.jl | 131 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 264 insertions(+)
 create mode 100644 src/makeequal.jl
 create mode 100644 test/test_makeequal.jl

diff --git a/src/makeequal.jl b/src/makeequal.jl
new file mode 100644
index 0000000..fca3b1b
--- /dev/null
+++ b/src/makeequal.jl
@@ -0,0 +1,133 @@
+
+"""
+    abstract type MakeEqualResult end
+
+A result of the `make_equal!` function. Can be one of 3 cases:
+- [`MakeEqualSuccess`](@ref)
+- [`MakeEqualHardFail`](@ref)
+- [`MakeEqualSoftFail`](@ref)
+"""
+abstract type MakeEqualResult end
+
+"""
+    struct MakeEqualSuccess <: MakeEqualResult end
+
+`node1` == `node2` is guaranteed under all possible assignments of the holes involved.
+"""
+struct MakeEqualSuccess <: MakeEqualResult end
+
+"""
+    struct MakeEqualHardFail <: MakeEqualResult end
+
+`node1` != `node2` is guaranteed under all possible assignments of the holes involved.
+"""
+struct MakeEqualHardFail <: MakeEqualResult end
+
+"""
+    struct MakeEqualSoftFail <: MakeEqualResult end
+
+Making `node1` == `node2` is ambiguous.
+Examples:
+- `RuleNode(1, [Hole({1, 2, 3})]) == RuleNode(1, [VarNode(:a)])`. The hole can be filled with any rule.
+- `Hole({1, 2, 3}) == DomainRuleNode({1, 2, 3})`. The hole can be filled with any rule.
+"""
+struct MakeEqualSoftFail <: MakeEqualResult end
+
+"""
+    function make_equal!(solver::Solver, node1::AbstractRuleNode, node2::AbstractRuleNode)::MakeEqualResult
+
+Tree manipulation that enforces `node1` == `node2` if unambiguous.
+"""
+function make_equal!(
+    solver::Solver, 
+    hole1::Union{RuleNode, AbstractHole},
+    hole2::Union{RuleNode, AbstractHole}
+)::MakeEqualResult
+    make_equal!(solver, hole1, hole2, Dict{Symbol, AbstractRuleNode}())
+end
+
+function make_equal!(
+    solver::Solver, 
+    hole1::Union{RuleNode, AbstractHole},
+    hole2::Union{RuleNode, AbstractHole},
+    vars::Dict{Symbol, AbstractRuleNode}
+)::MakeEqualResult
+    @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)
+            if get_rule(hole1) != get_rule(hole2)
+                set_infeasible!(solver)
+                return MakeEqualHardFail()
+            end
+        end
+        (true, false) => begin
+            #(RuleNode, AbstractHole)
+            if !hole2.domain[get_rule(hole1)]
+                set_infeasible!(solver)
+                return MakeEqualHardFail()
+            end
+            remove_all_but!(solver, path2, get_rule(hole1))
+            hole2 = get_node_at_location(solver, path2)
+        end
+        (false, true) => begin
+            #(AbstractHole, RuleNode)
+            if !hole1.domain[get_rule(hole2)]
+                set_infeasible!(solver)
+                return MakeEqualHardFail()
+            end
+            remove_all_but!(solver, path1, get_rule(hole2))
+            hole1 = get_node_at_location(solver, path1)
+        end
+        (false, false) => begin
+            #(AbstractHole, AbstractHole)
+            rules = get_intersection(hole1.domain, hole2.domain)
+            if length(rules) == 0
+                return MakeEqualHardFail()
+            elseif length(rules) == 1
+                remove_all_but!(solver, path1, rules[1])
+                remove_all_but!(solver, path2, rules[2])
+                hole1 = get_node_at_location(solver, path1)
+                hole2 = get_node_at_location(solver, path2)
+            else
+                return MakeEqualSoftFail()
+            end
+        end
+    end
+
+    softfailed = false
+    for (child1, child2) ∈ zip(get_children(hole1), get_children(hole2))
+        result = make_equal!(solver, child1, child2, vars)
+        @match result begin
+            ::MakeEqualSuccess => ();
+            ::MakeEqualHardFail => return result;
+            ::MakeEqualSoftFail => begin
+                softfailed = true
+            end
+        end
+    end
+    return softfailed ? MakeEqualSoftFail() : MakeEqualSuccess()
+end
+
+function make_equal!(
+    solver::Solver, 
+    node::Union{RuleNode, AbstractHole},
+    var::VarNode,
+    vars::Dict{Symbol, AbstractRuleNode}
+)::MakeEqualResult
+    if var.name ∈ keys(vars) 
+        return make_equal!(solver, node, vars[var.name], vars)
+    end
+    vars[var.name] = node
+    return MakeEqualSuccess()
+end
+
+function make_equal!(
+    ::Solver, 
+    ::Union{RuleNode, AbstractHole},
+    ::DomainRuleNode
+)::MakeEqualResult
+    throw("NotImplementedException: DomainRuleNodes are not yet support in make_equal!")
+end
diff --git a/test/test_makeequal.jl b/test/test_makeequal.jl
new file mode 100644
index 0000000..42b79ea
--- /dev/null
+++ b/test/test_makeequal.jl
@@ -0,0 +1,131 @@
+using HerbCore, HerbGrammar
+
+@testset verbose=false "MakeEqual (UniformSolver)" begin
+
+    function create_dummy_solver(leftnode::AbstractRuleNode, rightnode::AbstractRuleNode)
+        grammar = @csgrammar begin
+            Number = x | 1
+            Number = Number + Number
+            Number = Number - Number
+        end
+
+        uniform_tree = RuleNode(4, [
+            leftnode,
+            RuleNode(3, [
+                RuleNode(2), 
+                rightnode
+            ])
+        ])
+        solver = UniformSolver(grammar, uniform_tree)
+        leftnode = get_node_at_location(solver, [1])
+        rightnode = get_node_at_location(solver, [2, 2])
+        return solver, leftnode, rightnode
+    end
+
+    @testset "MakeEqualSuccess" begin
+        left = RuleNode(4, [RuleNode(1), RuleNode(2)])
+        right = RuleNode(4, [RuleNode(1), RuleNode(2)])
+        solver, left, right = create_dummy_solver(left, right)
+
+        @test HerbConstraints.make_equal!(solver, left, right) isa HerbConstraints.MakeEqualSuccess
+        @test left == right
+    end
+
+    @testset "MakeEqualSuccess, with holes" begin
+        left = RuleNode(4, [
+            UniformHole(BitVector((1, 1, 0, 0)), []), 
+            RuleNode(2)
+        ])
+        right = UniformHole(BitVector((0, 0, 1, 1)), [
+            RuleNode(1), 
+            UniformHole(BitVector((1, 1, 0, 0)), [])]
+        )
+        solver, left, right = create_dummy_solver(left, right)
+
+        @test HerbConstraints.make_equal!(solver, left, right) isa HerbConstraints.MakeEqualSuccess
+        @test left == RuleNode(4, [RuleNode(1), RuleNode(2)])
+        @test left == right
+    end
+
+    @testset "MakeEqualHardFail" begin
+        left = RuleNode(4, [RuleNode(1), RuleNode(2)])
+        right = RuleNode(4, [RuleNode(1), RuleNode(1)])
+        solver, left, right = create_dummy_solver(left, right)
+
+        @test HerbConstraints.make_equal!(solver, left, right) isa HerbConstraints.MakeEqualHardFail
+        @test left != right
+    end
+
+    @testset "MakeEqualHardFail, with holes" begin
+        left = RuleNode(4, [
+            UniformHole(BitVector((1, 1, 0, 0)), []), 
+            RuleNode(2)
+        ])
+        right = RuleNode(4, [
+            RuleNode(1), 
+            RuleNode(1)
+        ])
+        solver, left, right = create_dummy_solver(left, right)
+
+        @test HerbConstraints.make_equal!(solver, left, right) isa HerbConstraints.MakeEqualHardFail
+        @test left != right
+    end
+
+    @testset "MakeEqualSuccess, 1 VarNode" begin
+        node = RuleNode(4, [
+            UniformHole(BitVector((1, 1, 0, 0)), []), 
+            RuleNode(1)
+        ])
+        varnode = RuleNode(4, [
+            VarNode(:a), 
+            RuleNode(1)
+        ])
+        solver, node, _ = create_dummy_solver(node, RuleNode(1))
+
+        @test HerbConstraints.make_equal!(solver, node, varnode) isa HerbConstraints.MakeEqualSuccess
+    end
+
+    @testset "MakeEqualSuccess, 2 VarNodes" begin
+        node = RuleNode(4, [
+            UniformHole(BitVector((1, 1, 0, 0)), []), 
+            RuleNode(1)
+        ])
+        varnode = RuleNode(4, [
+            VarNode(:a), 
+            VarNode(:a)
+        ])
+        solver, node, _ = create_dummy_solver(node, RuleNode(1))
+
+        @test HerbConstraints.make_equal!(solver, node, varnode) isa HerbConstraints.MakeEqualSuccess
+        @test node == RuleNode(4, [RuleNode(1), RuleNode(1)])
+    end
+
+    @testset "MakeEqualSoftFail, 2 VarNodes" begin
+        node = RuleNode(4, [
+            UniformHole(BitVector((1, 1, 0, 0)), []), 
+            UniformHole(BitVector((1, 1, 0, 0)), [])
+        ])
+        varnode = RuleNode(4, [
+            VarNode(:a), 
+            VarNode(:a)
+        ])
+        solver, node, _ = create_dummy_solver(node, RuleNode(1))
+
+        @test HerbConstraints.make_equal!(solver, node, varnode) isa HerbConstraints.MakeEqualSoftFail
+    end
+
+    @testset "MakeEqualSuccess, 1 VarNode and a hole" begin
+        node = RuleNode(4, [
+            UniformHole(BitVector((1, 0, 0, 0)), []), 
+            UniformHole(BitVector((1, 1, 0, 0)), [])
+        ])
+        varnode = RuleNode(4, [
+            VarNode(:a), 
+            RuleNode(1)
+        ])
+        solver, node, _ = create_dummy_solver(node, RuleNode(1))
+
+        @test HerbConstraints.make_equal!(solver, node, varnode) isa HerbConstraints.MakeEqualSuccess
+        @test node == RuleNode(4, [RuleNode(1), RuleNode(1)])
+    end
+end

From 38b57746913a35e2552bfb9923a6c5a424f2af47 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Tue, 7 May 2024 20:43:53 +0200
Subject: [PATCH 05/20] Optimize empty dict allocations

---
 src/patternmatch.jl | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/patternmatch.jl b/src/patternmatch.jl
index c83205e..ab9cf94 100644
--- a/src/patternmatch.jl
+++ b/src/patternmatch.jl
@@ -38,6 +38,9 @@ struct PatternMatchSoftFail <: PatternMatchResult
     hole::AbstractHole
 end
 
+#Shared reference to a dict of vars to reduce memory allocations.
+VARS = Dict{Symbol, AbstractRuleNode}()
+
 """
     pattern_match(rn::AbstractRuleNode, mn::AbstractRuleNode)::PatternMatchResult
 
@@ -45,7 +48,8 @@ Recursively tries to match [`AbstractRuleNode`](@ref) `rn` with [`AbstractRuleNo
 Returns a `PatternMatchResult` that describes if the pattern was matched.
 """
 function pattern_match(rn::AbstractRuleNode, mn::AbstractRuleNode)::PatternMatchResult
-    pattern_match(rn, mn, Dict{Symbol, AbstractRuleNode}())
+    empty!(VARS)
+    pattern_match(rn, mn, VARS)
 end
 
 """

From a5c10f4514b3111ed67d76180145eb50594b538d Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Tue, 7 May 2024 20:44:22 +0200
Subject: [PATCH 06/20] Add `ContainsSubtree` constraint

---
 src/HerbConstraints.jl                        |   5 +
 src/grammarconstraints/contains_subtree.jl    |  31 ++++
 .../local_contains_subtree.jl                 | 106 +++++++++++++
 test/runtests.jl                              |   2 +
 test/test_contains_subtree.jl                 | 149 ++++++++++++++++++
 5 files changed, 293 insertions(+)
 create mode 100644 src/grammarconstraints/contains_subtree.jl
 create mode 100644 src/localconstraints/local_contains_subtree.jl
 create mode 100644 test/test_contains_subtree.jl

diff --git a/src/HerbConstraints.jl b/src/HerbConstraints.jl
index 7cc51b7..ea6108f 100644
--- a/src/HerbConstraints.jl
+++ b/src/HerbConstraints.jl
@@ -57,16 +57,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,6 +86,7 @@ export
     Forbidden,
     Ordered,
     Contains,
+    ContainsSubtree,
     ForbiddenSequence,
     Unique,
 
@@ -90,6 +94,7 @@ export
     LocalForbidden,
     LocalOrdered,
     LocalContains,
+    LocalContainsSubtree,
     LocalForbiddenSequence,
     LocalUnique,
 
diff --git a/src/grammarconstraints/contains_subtree.jl b/src/grammarconstraints/contains_subtree.jl
new file mode 100644
index 0000000..dfdcb41
--- /dev/null
+++ b/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
diff --git a/src/localconstraints/local_contains_subtree.jl b/src/localconstraints/local_contains_subtree.jl
new file mode 100644
index 0000000..733662b
--- /dev/null
+++ b/src/localconstraints/local_contains_subtree.jl
@@ -0,0 +1,106 @@
+
+"""
+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
+"""
+mutable struct LocalContainsSubtree <: AbstractLocalConstraint
+	path::Vector{Int}
+    tree::AbstractRuleNode
+    candidates::Union{Vector{AbstractRuleNode}, Nothing}
+    indices::Union{StateSparseSet, Nothing}
+end
+
+
+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.
+Uses a helper function to retrieve a list of holes that can potentially hold the target rule.
+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::UniformSolver, c::LocalContainsSubtree)
+    track!(solver, "LocalContainsSubtree propagation")
+    if isnothing(c.indices)
+        if isnothing(c.candidates)
+            # initial propagating: find the candidates
+            c.candidates = Vector{AbstractRuleNode}()
+            _set_candidates!(c, get_node_at_location(solver, c.path))
+        end
+        n = length(c.candidates)
+        if n == 0
+            track!(solver, "LocalContainsSubtree inconsistency (0 candidates)")
+            set_infeasible!(solver)
+            return
+        elseif n == 1
+            @match make_equal!(solver, c.candidates[1], c.tree) begin
+                ::MakeEqualSuccess => begin 
+                    track!(solver, "LocalContainsSubtree deduction (1 candidate)")
+                    deactivate!(solver, c);
+                    return;
+                end 
+                ::MakeEqualHardFail => begin 
+                    track!(solver, "LocalContainsSubtree inconsistency (1 candidate)")
+                    set_infeasible!(solver);
+                    return;
+                end 
+                ::MakeEqualSoftFail => begin
+                    track!(solver, "LocalContainsSubtree softfail (1 candidate)");
+                    return
+                end 
+            end
+        else
+            c.indices = StateSparseSet(solver.sm, n)
+        end
+    else
+        # check which candidates are still candidates. if there is only a single candidate left, enforce it becomes the target tree
+        for i ∈ c.indices
+            if pattern_match(c.candidates[i], c.tree) isa PatternMatchHardFail
+                remove!(c.indices, i)
+            end
+        end
+        if length(c.indices) == 1
+            @match make_equal!(solver, c.candidates[findfirst(c.indices)], c.tree) begin
+                ::MakeEqualSuccess => begin 
+                    track!(solver, "LocalContainsSubtree deduction (1 candidate remaining)")
+                    deactivate!(solver, c);
+                    return;
+                end 
+                ::MakeEqualHardFail => begin 
+                    track!(solver, "LocalContainsSubtree inconsistency (1 candidate remaining)")
+                    set_infeasible!(solver);
+                    return;
+                end 
+                ::MakeEqualSoftFail => begin
+                    track!(solver, "LocalContainsSubtree softfail (1 candidate remaining)");
+                    return
+                end 
+            end
+            return
+        end
+    end
+    track!(solver, "LocalContainsSubtree softfail (>=2 candidates)")
+end
+
+"""
+    _set_candidates!(c::LocalContainsSubtree, tree::AbstractRuleNode)
+
+Recursive helper function that stores all candidate matches.
+All nodes in the `tree` that can potentially become the target tree `c.tree` are considered a candidate.
+"""
+function _set_candidates!(c::LocalContainsSubtree, tree::AbstractRuleNode)
+    if !(pattern_match(c.tree, tree) isa PatternMatchHardFail)
+        push!(c.candidates, tree)
+    end
+    for child ∈ get_children(tree)
+        _set_candidates!(c, child)
+    end
+end
+
diff --git a/test/runtests.jl b/test/runtests.jl
index 78437a1..0bd7341 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -10,9 +10,11 @@ using Test
     include("test_pattern_match_domainrulenode.jl")
     #include("test_pattern_match_edgecases.jl")
     include("test_lessthanorequal.jl")
+    include("test_makeequal.jl")
     include("test_forbidden.jl")
     include("test_ordered.jl")
     include("test_contains.jl")
+    include("test_contains_subtree.jl")
     include("test_forbidden_sequence.jl")
     include("test_unique.jl")
 
diff --git a/test/test_contains_subtree.jl b/test/test_contains_subtree.jl
new file mode 100644
index 0000000..6d02658
--- /dev/null
+++ b/test/test_contains_subtree.jl
@@ -0,0 +1,149 @@
+@testset verbose=false "ContainsSubtree" begin
+
+    function has_active_constraints(solver::UniformSolver)::Bool
+        for c ∈ keys(solver.isactive)
+            if get_value(solver.isactive[c]) == 1
+                return true
+            end
+        end
+        return false
+    end
+
+    @testset "check_tree$with_varnode" for with_varnode ∈ ["", " (with VarNode)"]
+        contains_subtree = ContainsSubtree(
+            RuleNode(3, [
+                RuleNode(1),
+                isempty(with_varnode) ? RuleNode(2) : VarNode(:a)
+            ])
+        )
+
+        tree_true = RuleNode(3, [
+            RuleNode(3, [
+                RuleNode(1),
+                RuleNode(2)
+            ]),
+            RuleNode(2)
+        ])
+
+        tree_false = RuleNode(3, [
+            RuleNode(3, [
+                RuleNode(2),
+                RuleNode(2)
+            ]),
+            RuleNode(2)
+        ])
+
+        @test check_tree(contains_subtree, tree_true) == true
+        @test check_tree(contains_subtree, tree_false) == false
+    end
+
+    @testset "check_tree, 2 VarNodes" begin
+        contains_subtree = ContainsSubtree(
+            RuleNode(3, [
+                VarNode(:a),
+                VarNode(:a)
+            ])
+        )
+
+        tree_true = RuleNode(3, [
+            RuleNode(3, [
+                RuleNode(1),
+                RuleNode(2)
+            ]),
+            RuleNode(3, [
+                RuleNode(1),
+                RuleNode(2)
+            ]),
+        ])
+
+        tree_false = RuleNode(3, [
+            RuleNode(3, [
+                RuleNode(1),
+                RuleNode(2)
+            ]),
+            RuleNode(4, [
+                RuleNode(1),
+                RuleNode(2)
+            ]),
+        ])
+
+        @test check_tree(contains_subtree, tree_true) == true
+        @test check_tree(contains_subtree, tree_false) == false
+    end
+
+    @testset "propagate (UniformSolver)" begin
+        subtree = RuleNode(3, [
+            RuleNode(1),
+            VarNode(:a)
+        ])
+        grammar = @csgrammar begin
+            S = 1 | x
+            S = S + S
+            S = S * S
+        end
+        addconstraint!(grammar, ContainsSubtree(subtree))
+
+        @testset "0 candidates" begin
+            # 3{1, :a} is never contained in the tree
+
+            tree = UniformHole(BitVector((0, 0, 1, 1)), [
+                RuleNode(2),
+                RuleNode(4, [
+                    UniformHole(BitVector((1, 1, 0, 0)), []),
+                    UniformHole(BitVector((1, 1, 0, 0)), [])
+                ])
+            ])
+
+            solver = UniformSolver(grammar, tree)
+            @test !isfeasible(solver)
+        end
+
+        @testset "1 candidate" begin
+            # 3{1, :a} can only appear at the root
+
+            tree = UniformHole(BitVector((0, 0, 1, 1)), [
+                RuleNode(1),
+                RuleNode(4, [
+                    UniformHole(BitVector((1, 1, 0, 0)), []),
+                    UniformHole(BitVector((1, 1, 0, 0)), [])
+                ])
+            ])
+
+            solver = UniformSolver(grammar, tree)
+            tree = get_tree(solver)
+            @test isfeasible(solver)
+            @test isfilled(tree) && (get_rule(tree) == 3) # the root is filled with a 3
+            @test !isfilled(tree.children[2].children[1]) # the other two holes remain unfilled.
+            @test !isfilled(tree.children[2].children[2]) # the other two holes remain unfilled.
+            @test !has_active_constraints(solver) # constraint is satisfied and deleted
+        end
+
+        @testset "2 candidates" begin
+            # 3{1, :a} can appear at path=[] and path=[2].
+
+            tree = UniformHole(BitVector((0, 0, 1, 1)), [
+                RuleNode(1),
+                RuleNode(3, [
+                    UniformHole(BitVector((1, 1, 0, 0)), []),
+                    UniformHole(BitVector((1, 1, 0, 0)), [])
+                ])
+            ])
+
+            #initial propagation: softfail, all holes remain unfilled
+            solver = UniformSolver(grammar, tree)
+            tree = get_tree(solver)
+            @test isfeasible(solver)
+            @test !isfilled(tree)
+            @test !isfilled(tree.children[2].children[1])
+            @test !isfilled(tree.children[2].children[2])
+            @test has_active_constraints(solver) # softfail: constraint remains active
+
+            #remove rule 3 from the root, now 3{1, :a} can only appear at path=[2]
+            remove!(solver, Vector{Int}(), 3)
+            hole = tree.children[2].children[1]
+            @test isfeasible(solver)
+            @test isfilled(hole) && (get_rule(hole) == 1) #the hole is filled with rule 1
+            @test !has_active_constraints(solver) # constraint is satisfied and deleted
+        end
+    end
+end

From 9cfdabd917fafc4866183627bc1eb6fd51697cca Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Wed, 8 May 2024 14:18:23 +0200
Subject: [PATCH 07/20] Add get_path function for solvers

---
 src/lessthanorequal.jl                      | 8 +++++---
 src/makeequal.jl                            | 6 ++++--
 src/solver/generic_solver/generic_solver.jl | 9 +++++++++
 3 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/lessthanorequal.jl b/src/lessthanorequal.jl
index 38868fa..0596f74 100644
--- a/src/lessthanorequal.jl
+++ b/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
diff --git a/src/makeequal.jl b/src/makeequal.jl
index fca3b1b..025f763 100644
--- a/src/makeequal.jl
+++ b/src/makeequal.jl
@@ -53,8 +53,6 @@ function make_equal!(
     vars::Dict{Symbol, AbstractRuleNode}
 )::MakeEqualResult
     @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)
@@ -69,6 +67,7 @@ function make_equal!(
                 set_infeasible!(solver)
                 return MakeEqualHardFail()
             end
+            path2 = get_path(solver, hole2)
             remove_all_but!(solver, path2, get_rule(hole1))
             hole2 = get_node_at_location(solver, path2)
         end
@@ -78,6 +77,7 @@ function make_equal!(
                 set_infeasible!(solver)
                 return MakeEqualHardFail()
             end
+            path1 = get_path(solver, hole1)
             remove_all_but!(solver, path1, get_rule(hole2))
             hole1 = get_node_at_location(solver, path1)
         end
@@ -87,6 +87,8 @@ function make_equal!(
             if length(rules) == 0
                 return MakeEqualHardFail()
             elseif length(rules) == 1
+                path1 = get_path(solver, hole1)
+                path2 = get_path(solver, hole2)
                 remove_all_but!(solver, path1, rules[1])
                 remove_all_but!(solver, path2, rules[2])
                 hole1 = get_node_at_location(solver, path1)
diff --git a/src/solver/generic_solver/generic_solver.jl b/src/solver/generic_solver/generic_solver.jl
index 98d2258..a5a3395 100644
--- a/src/solver/generic_solver/generic_solver.jl
+++ b/src/solver/generic_solver/generic_solver.jl
@@ -255,6 +255,15 @@ function isfeasible(solver::GenericSolver)
 end
 
 
+"""
+    get_path(solver::UniformSolver, node::AbstractRuleNode)
+
+Get the path at which the `node` is located.
+"""
+function HerbCore.get_path(solver::GenericSolver, node::AbstractRuleNode)::Vector{Int}
+    return get_path(get_tree(solver), node)
+end
+
 """
     HerbCore.get_node_at_location(solver::GenericSolver, location::Vector{Int})::AbstractRuleNode
 

From e2afc29ffe3d89f224830b3f16f34b5b0327774b Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Wed, 8 May 2024 14:42:51 +0200
Subject: [PATCH 08/20] Add a caching optimization for LocalUnique

---
 src/localconstraints/local_unique.jl | 47 +++++++++++++++++++++++-----
 1 file changed, 39 insertions(+), 8 deletions(-)

diff --git a/src/localconstraints/local_unique.jl b/src/localconstraints/local_unique.jl
index 95baac2..84e21f1 100644
--- a/src/localconstraints/local_unique.jl
+++ b/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

From a5c7d277578b1d652838c59be4b19edc27d79705 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Wed, 8 May 2024 16:28:47 +0200
Subject: [PATCH 09/20] Prevent nesting propagate calls

---
 src/solver/generic_solver/generic_solver.jl | 3 +++
 src/solver/uniform_solver/uniform_solver.jl | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/src/solver/generic_solver/generic_solver.jl b/src/solver/generic_solver/generic_solver.jl
index a5a3395..e16fd38 100644
--- a/src/solver/generic_solver/generic_solver.jl
+++ b/src/solver/generic_solver/generic_solver.jl
@@ -109,7 +109,10 @@ function post!(solver::GenericSolver, constraint::AbstractLocalConstraint)
     # add to the list of active constraints
     push!(get_state(solver).active_constraints, constraint)
     # initial propagation of the new constraint
+    solver.fix_point_running = true
     propagate!(solver, constraint)
+    solver.fix_point_running = false
+    fix_point!(solver)
 end
 
 
diff --git a/src/solver/uniform_solver/uniform_solver.jl b/src/solver/uniform_solver/uniform_solver.jl
index 966ab91..ed8bb2c 100644
--- a/src/solver/uniform_solver/uniform_solver.jl
+++ b/src/solver/uniform_solver/uniform_solver.jl
@@ -146,7 +146,10 @@ Converts the constraint to a state constraint and schedules it for propagation.
 function post!(solver::UniformSolver, constraint::AbstractLocalConstraint)
     if !isfeasible(solver) return end
     # initial propagation of the new constraint
+    solver.fix_point_running = true
     propagate!(solver, constraint)
+    solver.fix_point_running = false
+    fix_point!(solver)
     if constraint ∈ solver.canceledconstraints
         # the constraint was deactivated during the initial propagation, cancel posting the constraint
         track!(solver, "cancel post (2/2)")

From fc98460e36f56474d20e6911b80606513d47ad49 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Thu, 9 May 2024 14:18:34 +0200
Subject: [PATCH 10/20] Fix a bug when trying to make 2 holes equal

---
 src/makeequal.jl | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/makeequal.jl b/src/makeequal.jl
index 025f763..b58308c 100644
--- a/src/makeequal.jl
+++ b/src/makeequal.jl
@@ -87,10 +87,11 @@ function make_equal!(
             if length(rules) == 0
                 return MakeEqualHardFail()
             elseif length(rules) == 1
+                rule = rules[1]
                 path1 = get_path(solver, hole1)
                 path2 = get_path(solver, hole2)
-                remove_all_but!(solver, path1, rules[1])
-                remove_all_but!(solver, path2, rules[2])
+                remove_all_but!(solver, path1, rule)
+                remove_all_but!(solver, path2, rule)
                 hole1 = get_node_at_location(solver, path1)
                 hole2 = get_node_at_location(solver, path2)
             else

From 2aa3fe3dce36ede6528de4bea293ada09a8a8da4 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Thu, 9 May 2024 14:21:07 +0200
Subject: [PATCH 11/20] Fix a case where LocalContainsSubtree missed spotting
 an inconsistency

---
 src/localconstraints/local_contains_subtree.jl | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/localconstraints/local_contains_subtree.jl b/src/localconstraints/local_contains_subtree.jl
index 733662b..b5f08f1 100644
--- a/src/localconstraints/local_contains_subtree.jl
+++ b/src/localconstraints/local_contains_subtree.jl
@@ -66,24 +66,28 @@ function propagate!(solver::UniformSolver, c::LocalContainsSubtree)
                 remove!(c.indices, i)
             end
         end
-        if length(c.indices) == 1
+        n = length(c.indices)
+        if n == 0
+            track!(solver, "LocalContainsSubtree inconsistency (0 candidates remaining)")
+            set_infeasible!(solver)
+            return
+        elseif n == 1
             @match make_equal!(solver, c.candidates[findfirst(c.indices)], c.tree) begin
                 ::MakeEqualSuccess => begin 
                     track!(solver, "LocalContainsSubtree deduction (1 candidate remaining)")
                     deactivate!(solver, c);
-                    return;
+                    return
                 end 
                 ::MakeEqualHardFail => begin 
                     track!(solver, "LocalContainsSubtree inconsistency (1 candidate remaining)")
                     set_infeasible!(solver);
-                    return;
+                    return
                 end 
                 ::MakeEqualSoftFail => begin
                     track!(solver, "LocalContainsSubtree softfail (1 candidate remaining)");
                     return
                 end 
             end
-            return
         end
     end
     track!(solver, "LocalContainsSubtree softfail (>=2 candidates)")

From 2032f1bf84158d026663fa4e44d409e19d90f1f8 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Thu, 9 May 2024 14:48:57 +0200
Subject: [PATCH 12/20] Remove slow map function

---
 src/patternmatch.jl | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/patternmatch.jl b/src/patternmatch.jl
index ab9cf94..7e643b3 100644
--- a/src/patternmatch.jl
+++ b/src/patternmatch.jl
@@ -81,7 +81,8 @@ function pattern_match(rns::Vector{AbstractRuleNode}, mns::Vector{AbstractRuleNo
     # end
     @assert length(rns) == length(mns) "Unable to pattern match rulenodes with different arities"
     match_result = PatternMatchSuccess()
-    for child_match_result ∈ map(tup -> pattern_match(tup[2][1], tup[2][2], vars), enumerate(zip(rns, mns)))
+    for (n1, n2) ∈ zip(rns, mns)
+        child_match_result = pattern_match(n1, n2, vars)
         @match child_match_result begin
             ::PatternMatchHardFail => return child_match_result;
             ::PatternMatchSoftFail => (match_result = child_match_result); #continue searching for a hardfail

From 39f7ca015b0021377f2770e14a10afce30868254 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Thu, 9 May 2024 17:39:36 +0200
Subject: [PATCH 13/20] Add constraint priority

---
 src/HerbConstraints.jl | 11 +++++++++++
 src/solver/solver.jl   |  3 ++-
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/HerbConstraints.jl b/src/HerbConstraints.jl
index ea6108f..7f53f2b 100644
--- a/src/HerbConstraints.jl
+++ b/src/HerbConstraints.jl
@@ -36,6 +36,17 @@ Inside the [`propagate!`](@ref) function, the constraint can use the following s
 """
 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")
diff --git a/src/solver/solver.jl b/src/solver/solver.jl
index d7c3e09..7d511c6 100644
--- a/src/solver/solver.jl
+++ b/src/solver/solver.jl
@@ -32,6 +32,7 @@ function fix_point!(solver::Solver)
     while !isempty(solver.schedule)
         if !isfeasible(solver)
             #an inconsistency was found, stop propagating constraints and return
+            track!(solver, "inconsistency")
             empty!(solver.schedule)
             break
         end
@@ -51,7 +52,7 @@ function schedule!(solver::Solver, constraint::AbstractLocalConstraint)
     @assert isfeasible(solver)
     if constraint ∉ keys(solver.schedule)
         track!(solver, "schedule!")
-        enqueue!(solver.schedule, constraint, 99)
+        enqueue!(solver.schedule, constraint, get_priority(constraint))
     end
 end
 

From f2357d2c2528ca57ca511a3f15f590ea7b1a16fc Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Fri, 10 May 2024 13:41:47 +0200
Subject: [PATCH 14/20] Remove fix_point! on post!

---
 src/solver/generic_solver/generic_solver.jl | 6 +++---
 src/solver/uniform_solver/uniform_solver.jl | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/solver/generic_solver/generic_solver.jl b/src/solver/generic_solver/generic_solver.jl
index e16fd38..baf2d9c 100644
--- a/src/solver/generic_solver/generic_solver.jl
+++ b/src/solver/generic_solver/generic_solver.jl
@@ -109,10 +109,10 @@ function post!(solver::GenericSolver, constraint::AbstractLocalConstraint)
     # add to the list of active constraints
     push!(get_state(solver).active_constraints, constraint)
     # initial propagation of the new constraint
+    temp = solver.fix_point_running
     solver.fix_point_running = true
     propagate!(solver, constraint)
-    solver.fix_point_running = false
-    fix_point!(solver)
+    solver.fix_point_running = temp
 end
 
 
@@ -259,7 +259,7 @@ end
 
 
 """
-    get_path(solver::UniformSolver, node::AbstractRuleNode)
+    get_path(solver::GenericSolver, node::AbstractRuleNode)
 
 Get the path at which the `node` is located.
 """
diff --git a/src/solver/uniform_solver/uniform_solver.jl b/src/solver/uniform_solver/uniform_solver.jl
index ed8bb2c..a4f3609 100644
--- a/src/solver/uniform_solver/uniform_solver.jl
+++ b/src/solver/uniform_solver/uniform_solver.jl
@@ -146,10 +146,10 @@ Converts the constraint to a state constraint and schedules it for propagation.
 function post!(solver::UniformSolver, constraint::AbstractLocalConstraint)
     if !isfeasible(solver) return end
     # initial propagation of the new constraint
+    temp = solver.fix_point_running
     solver.fix_point_running = true
     propagate!(solver, constraint)
-    solver.fix_point_running = false
-    fix_point!(solver)
+    solver.fix_point_running = temp
     if constraint ∈ solver.canceledconstraints
         # the constraint was deactivated during the initial propagation, cancel posting the constraint
         track!(solver, "cancel post (2/2)")

From c545c278a8c8a1a6826aa673e68a7a25baf7e348 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Fri, 10 May 2024 13:42:56 +0200
Subject: [PATCH 15/20] add `get_nodes`, to get all the nodes of the tree
 without recursion

---
 src/solver/uniform_solver/uniform_solver.jl | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/solver/uniform_solver/uniform_solver.jl b/src/solver/uniform_solver/uniform_solver.jl
index a4f3609..a8c96dd 100644
--- a/src/solver/uniform_solver/uniform_solver.jl
+++ b/src/solver/uniform_solver/uniform_solver.jl
@@ -93,6 +93,16 @@ function get_hole_at_location(solver::UniformSolver, path::Vector{Int})
 end
 
 
+"""
+    get_nodes(solver)
+
+Return an iterator over all nodes in the tree
+"""
+function get_nodes(solver)
+    return keys(solver.node_to_path)
+end
+
+
 """
     function get_grammar(solver::UniformSolver)::AbstractGrammar
 

From 759e0b7778b7de30a8a4db24f314d128824888ca Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Fri, 10 May 2024 13:43:20 +0200
Subject: [PATCH 16/20] Update docstring

---
 src/HerbConstraints.jl | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/HerbConstraints.jl b/src/HerbConstraints.jl
index 7f53f2b..43061f2 100644
--- a/src/HerbConstraints.jl
+++ b/src/HerbConstraints.jl
@@ -18,9 +18,7 @@ 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:
@@ -28,11 +26,6 @@ Inside the [`propagate!`](@ref) function, the constraint can use the following s
 - `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
 

From 3b43b1a618f76ba163d1343173d9b7a79aa8e5fb Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Fri, 10 May 2024 13:46:53 +0200
Subject: [PATCH 17/20] Optimize ContainsSubtree: less pattern matches, less
 softfails, less allocations

---
 .../local_contains_subtree.jl                 | 121 ++++++------
 test/test_contains_subtree.jl                 | 176 ++++++++++++------
 2 files changed, 188 insertions(+), 109 deletions(-)

diff --git a/src/localconstraints/local_contains_subtree.jl b/src/localconstraints/local_contains_subtree.jl
index b5f08f1..0530165 100644
--- a/src/localconstraints/local_contains_subtree.jl
+++ b/src/localconstraints/local_contains_subtree.jl
@@ -5,7 +5,8 @@ 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
+    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}
@@ -14,97 +15,113 @@ mutable struct LocalContainsSubtree <: AbstractLocalConstraint
     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.
-Uses a helper function to retrieve a list of holes that can potentially hold the target rule.
-If there is only a single hole that can potentially hold the target rule, that hole will be filled with that rule.
+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.indices)
-        if isnothing(c.candidates)
-            # initial propagating: find the candidates
-            c.candidates = Vector{AbstractRuleNode}()
-            _set_candidates!(c, get_node_at_location(solver, c.path))
+    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 (0 candidates)")
+            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 (1 candidate)")
+                    track!(solver, "LocalContainsSubtree deduction (initial)")
                     deactivate!(solver, c);
-                    return;
-                end 
-                ::MakeEqualHardFail => begin 
-                    track!(solver, "LocalContainsSubtree inconsistency (1 candidate)")
-                    set_infeasible!(solver);
-                    return;
+                    return
                 end 
                 ::MakeEqualSoftFail => begin
-                    track!(solver, "LocalContainsSubtree softfail (1 candidate)");
+                    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
-        # check which candidates are still candidates. if there is only a single candidate left, enforce it becomes the target tree
-        for i ∈ c.indices
-            if pattern_match(c.candidates[i], c.tree) isa PatternMatchHardFail
-                remove!(c.indices, i)
+        # 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 = length(c.indices)
-        if n == 0
-            track!(solver, "LocalContainsSubtree inconsistency (0 candidates remaining)")
-            set_infeasible!(solver)
-            return
-        elseif n == 1
-            @match make_equal!(solver, c.candidates[findfirst(c.indices)], c.tree) begin
-                ::MakeEqualSuccess => begin 
-                    track!(solver, "LocalContainsSubtree deduction (1 candidate remaining)")
-                    deactivate!(solver, c);
+        if isnothing(c.indices) || (size(c.indices) == 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 
-                ::MakeEqualHardFail => begin 
-                    track!(solver, "LocalContainsSubtree inconsistency (1 candidate remaining)")
-                    set_infeasible!(solver);
+                ::MakeEqualSuccess => begin 
+                    track!(solver, "LocalContainsSubtree deduction")
+                    deactivate!(solver, c);
                     return
                 end 
                 ::MakeEqualSoftFail => begin
-                    track!(solver, "LocalContainsSubtree softfail (1 candidate remaining)");
+                    track!(solver, "LocalContainsSubtree softfail (1 candidate)")
                     return
                 end 
             end
         end
+        track!(solver, "LocalContainsSubtree softfail (>=2 candidates)")
     end
-    track!(solver, "LocalContainsSubtree softfail (>=2 candidates)")
 end
-
-"""
-    _set_candidates!(c::LocalContainsSubtree, tree::AbstractRuleNode)
-
-Recursive helper function that stores all candidate matches.
-All nodes in the `tree` that can potentially become the target tree `c.tree` are considered a candidate.
-"""
-function _set_candidates!(c::LocalContainsSubtree, tree::AbstractRuleNode)
-    if !(pattern_match(c.tree, tree) isa PatternMatchHardFail)
-        push!(c.candidates, tree)
-    end
-    for child ∈ get_children(tree)
-        _set_candidates!(c, child)
-    end
-end
-
diff --git a/test/test_contains_subtree.jl b/test/test_contains_subtree.jl
index 6d02658..d54afbd 100644
--- a/test/test_contains_subtree.jl
+++ b/test/test_contains_subtree.jl
@@ -72,78 +72,140 @@
     end
 
     @testset "propagate (UniformSolver)" begin
-        subtree = RuleNode(3, [
-            RuleNode(1),
-            VarNode(:a)
-        ])
-        grammar = @csgrammar begin
-            S = 1 | x
-            S = S + S
-            S = S * S
-        end
-        addconstraint!(grammar, ContainsSubtree(subtree))
+        @testset "1 VarNode" begin
+            subtree = RuleNode(3, [
+                RuleNode(1),
+                VarNode(:a)
+            ])
+            grammar = @csgrammar begin
+                S = 1 | x
+                S = S + S
+                S = S * S
+            end
+            addconstraint!(grammar, ContainsSubtree(subtree))
 
-        @testset "0 candidates" begin
-            # 3{1, :a} is never contained in the tree
+            @testset "0 candidates" begin
+                # 3{1, :a} is never contained in the tree
 
-            tree = UniformHole(BitVector((0, 0, 1, 1)), [
-                RuleNode(2),
-                RuleNode(4, [
-                    UniformHole(BitVector((1, 1, 0, 0)), []),
-                    UniformHole(BitVector((1, 1, 0, 0)), [])
+                tree = UniformHole(BitVector((0, 0, 1, 1)), [
+                    RuleNode(2),
+                    RuleNode(4, [
+                        UniformHole(BitVector((1, 1, 0, 0)), []),
+                        UniformHole(BitVector((1, 1, 0, 0)), [])
+                    ])
                 ])
-            ])
 
-            solver = UniformSolver(grammar, tree)
-            @test !isfeasible(solver)
-        end
+                solver = UniformSolver(grammar, tree)
+                @test !isfeasible(solver)
+            end
 
-        @testset "1 candidate" begin
-            # 3{1, :a} can only appear at the root
+            @testset "1 candidate" begin
+                # 3{1, :a} can only appear at the root
 
-            tree = UniformHole(BitVector((0, 0, 1, 1)), [
-                RuleNode(1),
-                RuleNode(4, [
-                    UniformHole(BitVector((1, 1, 0, 0)), []),
-                    UniformHole(BitVector((1, 1, 0, 0)), [])
+                tree = UniformHole(BitVector((0, 0, 1, 1)), [
+                    RuleNode(1),
+                    RuleNode(4, [
+                        UniformHole(BitVector((1, 1, 0, 0)), []),
+                        UniformHole(BitVector((1, 1, 0, 0)), [])
+                    ])
                 ])
-            ])
 
-            solver = UniformSolver(grammar, tree)
-            tree = get_tree(solver)
-            @test isfeasible(solver)
-            @test isfilled(tree) && (get_rule(tree) == 3) # the root is filled with a 3
-            @test !isfilled(tree.children[2].children[1]) # the other two holes remain unfilled.
-            @test !isfilled(tree.children[2].children[2]) # the other two holes remain unfilled.
-            @test !has_active_constraints(solver) # constraint is satisfied and deleted
+                solver = UniformSolver(grammar, tree)
+                tree = get_tree(solver)
+                @test isfeasible(solver)
+                @test isfilled(tree) && (get_rule(tree) == 3) # the root is filled with a 3
+                @test !isfilled(tree.children[2].children[1]) # the other two holes remain unfilled.
+                @test !isfilled(tree.children[2].children[2]) # the other two holes remain unfilled.
+                @test !has_active_constraints(solver) # constraint is satisfied and deleted
+            end
+
+            @testset "2 candidates" begin
+                # 3{1, :a} can appear at path=[] and path=[2].
+
+                tree = UniformHole(BitVector((0, 0, 1, 1)), [
+                    RuleNode(1),
+                    RuleNode(3, [
+                        UniformHole(BitVector((1, 1, 0, 0)), []),
+                        UniformHole(BitVector((1, 1, 0, 0)), [])
+                    ])
+                ])
+
+                #initial propagation: softfail, all holes remain unfilled
+                solver = UniformSolver(grammar, tree)
+                tree = get_tree(solver)
+                @test isfeasible(solver)
+                @test !isfilled(tree)
+                @test !isfilled(tree.children[2].children[1])
+                @test !isfilled(tree.children[2].children[2])
+                @test has_active_constraints(solver) # softfail: constraint remains active
+
+                #remove rule 3 from the root, now 3{1, :a} can only appear at path=[2]
+                remove!(solver, Vector{Int}(), 3)
+                hole = tree.children[2].children[1]
+                @test isfeasible(solver)
+                @test isfilled(hole) && (get_rule(hole) == 1) #the hole is filled with rule 1
+                @test !has_active_constraints(solver) # constraint is satisfied and deleted
+            end
         end
 
-        @testset "2 candidates" begin
-            # 3{1, :a} can appear at path=[] and path=[2].
+        @testset "2 VarNodes, softfails" begin
+            subtree = RuleNode(3, [
+                VarNode(:a),
+                VarNode(:a)
+            ])
+            grammar = @csgrammar begin
+                S = 1 | x
+                S = S + S
+                S = S * S
+            end
+            addconstraint!(grammar, ContainsSubtree(subtree))
 
-            tree = UniformHole(BitVector((0, 0, 1, 1)), [
-                RuleNode(1),
-                RuleNode(3, [
+            @testset "1 candidate, partial softfail" begin
+                # 3{:a, :a} can only appear at the root
+                # the first hole can be filled with a 3
+                # filling the other two holes is ambiguous
+
+                tree = UniformHole(BitVector((0, 0, 1, 1)), [
                     UniformHole(BitVector((1, 1, 0, 0)), []),
                     UniformHole(BitVector((1, 1, 0, 0)), [])
                 ])
-            ])
 
-            #initial propagation: softfail, all holes remain unfilled
-            solver = UniformSolver(grammar, tree)
-            tree = get_tree(solver)
-            @test isfeasible(solver)
-            @test !isfilled(tree)
-            @test !isfilled(tree.children[2].children[1])
-            @test !isfilled(tree.children[2].children[2])
-            @test has_active_constraints(solver) # softfail: constraint remains active
-
-            #remove rule 3 from the root, now 3{1, :a} can only appear at path=[2]
-            remove!(solver, Vector{Int}(), 3)
-            hole = tree.children[2].children[1]
-            @test isfeasible(solver)
-            @test isfilled(hole) && (get_rule(hole) == 1) #the hole is filled with rule 1
-            @test !has_active_constraints(solver) # constraint is satisfied and deleted
+                solver = UniformSolver(grammar, tree)
+                tree = get_tree(solver)
+                @test isfeasible(solver)
+                @test isfilled(tree) && (get_rule(tree) == 3) # the root is filled with a 3
+                @test !isfilled(tree.children[1]) # the other two holes remain unfilled.
+                @test !isfilled(tree.children[2]) # the other two holes remain unfilled.
+                @test has_active_constraints(solver) # the constraint remains active
+            end
+
+            @testset "2 candidates, softfail" begin
+                # 3{:a, :a} can appear at the root, or at child 1
+                # Three out of the four possible trees are valid:
+                # - 3{3{1, 1}, 4{1, 1}} VALID (contains the subtree at child 1)
+                # - 3{4{1, 1}, 4{1, 1}} VALID (contains the subtree at root)
+                # - 4{3{1, 1}, 4{1, 1}} VALID (contains the subtree at child 1)
+                # - 4{4{1, 1}, 4{1, 1}} INVALID
+                # no deductions can be made at this point.
+
+                tree = UniformHole(BitVector((0, 0, 1, 1)), [
+                    UniformHole(BitVector((0, 0, 1, 1)), [
+                        RuleNode(1),
+                        RuleNode(1)
+                    ])
+                    RuleNode(4, [
+                        RuleNode(1),
+                        RuleNode(1)
+                    ])
+                ])
+
+                solver = UniformSolver(grammar, tree)
+                tree = get_tree(solver)
+                @test isfeasible(solver)
+                @test !isfilled(tree)
+                @test !isfilled(tree.children[1])
+                @test has_active_constraints(solver)
+            end
         end
     end
 end

From 29bd260e68776c398914a2da6684d278873690b3 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Fri, 10 May 2024 22:45:06 +0200
Subject: [PATCH 18/20] Make ContainsSubtree detect an inconsistency when all
 pattern matches hard fail on re-propagation

---
 src/localconstraints/local_contains_subtree.jl | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/localconstraints/local_contains_subtree.jl b/src/localconstraints/local_contains_subtree.jl
index 0530165..ea2e6a1 100644
--- a/src/localconstraints/local_contains_subtree.jl
+++ b/src/localconstraints/local_contains_subtree.jl
@@ -102,7 +102,8 @@ function propagate!(solver::UniformSolver, c::LocalContainsSubtree)
                 end
             end
         end
-        if isnothing(c.indices) || (size(c.indices) == 1)
+        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
@@ -121,6 +122,10 @@ function propagate!(solver::UniformSolver, c::LocalContainsSubtree)
                     return
                 end 
             end
+        elseif n == 0
+            track!(solver, "LocalContainsSubtree inconsistency")
+            set_infeasible!(solver)
+            return
         end
         track!(solver, "LocalContainsSubtree softfail (>=2 candidates)")
     end

From 5f988190def130656b2bf92637c974a3a74d0b43 Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Sun, 12 May 2024 16:59:02 +0200
Subject: [PATCH 19/20] Add a softfail case for `ignore_if`

---
 src/localconstraints/local_forbidden_sequence.jl | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/localconstraints/local_forbidden_sequence.jl b/src/localconstraints/local_forbidden_sequence.jl
index ffd4ff9..f413b2f 100644
--- a/src/localconstraints/local_forbidden_sequence.jl
+++ b/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

From 4062e75d4a60a3deeb8e0a1fafed608aef18bb5b Mon Sep 17 00:00:00 2001
From: Whebon <bart-man99@hotmail.com>
Date: Tue, 14 May 2024 15:13:00 +0200
Subject: [PATCH 20/20] Update test for issue #54

---
 test/test_domain_utils.jl | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/test/test_domain_utils.jl b/test/test_domain_utils.jl
index cb7542d..f8aa7fc 100644
--- a/test/test_domain_utils.jl
+++ b/test/test_domain_utils.jl
@@ -82,18 +82,18 @@ using HerbGrammar
     @testset "partition" begin
         #partion groups the rules by childtypes
         g = @csgrammar begin
-            A = 1           #1
-            A = 1           #2
-            A = A           #3
-            A = A           #4
-            A = (A, A)      #5
-            A = (A, A)      #6
-            A = (A, B)      #7
-            A = (A, B)      #8
-            B = 1           #9
-            B = 1           #10
-            B = (A, B)      #11
-            B = (A, B)      #12
+            A = (1)
+            A = (2)
+            A = (3, A)
+            A = (4, A)
+            A = (5, A, A)
+            A = (6, A, A)
+            A = (7, A, B)
+            A = (8, A, B)
+            B = (9)
+            B = (10)
+            B = (11, A, B)
+            B = (12, A, B)
         end
         domains = partition(Hole(get_domain(g, :A)), g)
         @test length(domains) == 4