Two new constraints

src/HerbConstraints.jl

@@ -61,11 +61,14 @@ include("lessthanorequal.jl")
 include("localconstraints/local_forbidden.jl")
 include("localconstraints/local_ordered.jl")
 include("localconstraints/local_contains.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/forbidden_sequence.jl")
+include("grammarconstraints/unique.jl")
 
 export
     AbstractGrammarConstraint,
@@ -80,11 +83,15 @@ export
     Forbidden,
     Ordered,
     Contains,
+    ForbiddenSequence,
+    Unique,
 
     #local constraints
     LocalForbidden,
     LocalOrdered,
     LocalContains,
+    LocalForbiddenSequence,
+    LocalUnique,
 
     #public solver functions
     GenericSolver,

src/grammarconstraints/contains.jl

@@ -6,21 +6,21 @@ struct Contains <: AbstractGrammarConstraint
     rule::Int
 end
 
-function on_new_node(solver::Solver, contraint::Contains, path::Vector{Int})
+function on_new_node(solver::Solver, c::Contains, path::Vector{Int})
     if length(path) == 0
         #only post a local constraint at the root
-        post!(solver, LocalContains(path, contraint.rule))
+        post!(solver, LocalContains(path, c.rule))
     end
 end
 
 """
-    check_tree(c::Forbidden, g::AbstractGrammar, tree::RuleNode)::Bool
+    check_tree(c::Contains, tree::AbstractRuleNode)::Bool
 
-Checks if the given [`AbstractRuleNode`](@ref) tree abides the [`Forbidden`](@ref) constraint.
+Checks if the given [`AbstractRuleNode`](@ref) tree abides the [`Contains`](@ref) constraint.
 """
-function check_tree(contraint::Contains, tree::AbstractRuleNode)::Bool
-    if get_rule(tree) == contraint.rule
+function check_tree(c::Contains, tree::AbstractRuleNode)::Bool
+    if get_rule(tree) == c.rule
         return true
     end
-    return any(check_tree(contraint, child) for child ∈ get_children(tree))
+    return any(check_tree(c, child) for child ∈ get_children(tree))
 end

src/grammarconstraints/forbidden.jl

@@ -18,12 +18,6 @@ For example, consider the tree `1(a, 2(b, 3(c, 4))))`:
     Therefore, this tree invalid.
 - `Forbidden(RuleNode(3, [VarNode(:v), VarNode(:v)]))` forbids `c` to be filled with `4`, since that would 
     make both assignments to `v` equal, which causes a successful match.
-
-!!! warning
-    The [`Forbidden`](@ref) constraint makes use of [`AbstractLocalConstraint`](@ref)s to make sure that constraints 
-    are also enforced in the future when the context of a [`AbstractHole`](@ref) changes. 
-    Therefore, [`Forbidden`](@ref) can only be used in implementations that keep track of the 
-    [`AbstractLocalConstraint`](@ref)s and propagate them at the right moments.
 """
 struct Forbidden <: AbstractGrammarConstraint
     tree::AbstractRuleNode
@@ -41,7 +35,7 @@ function on_new_node(solver::Solver, c::Forbidden, path::Vector{Int})
 end
 
 """
-    check_tree(c::Forbidden, g::AbstractGrammar, tree::RuleNode)::Bool
+    check_tree(c::Forbidden, tree::AbstractRuleNode)::Bool
 
 Checks if the given [`AbstractRuleNode`](@ref) tree abides the [`Forbidden`](@ref) constraint.
 """

src/grammarconstraints/forbidden_sequence.jl

@@ -0,0 +1,83 @@
+"""
+    ForbiddenPath <: AbstractGrammarConstraint
+
+This [`AbstractGrammarConstraint`] forbids the given `sequence` of rule nodes.
+Sequences are strictly vertical and may include gaps. Consider the tree `1(a, 2(b, 3(c, d))))`:
+- `[2, 3, d]` is a sequence
+- `[1, 3, d]` is a sequence
+- `[3, c, d]` is not a sequence
+
+Examples:
+- `ForbiddenSequence([3, 4])` enforces that rule `4` cannot be applied at `c` or `d`.
+- `ForbiddenSequence([1, 2, 4])` enforces that rule `4` cannot be applied at `b`, `c` or `d`.
+- `ForbiddenSequence([1, 4])` enforces that rule `4` cannot be applied anywhere.
+
+If any of the rules in `ignore_if` appears in the sequence, the constraint is ignored.
+Suppose the forbidden `sequence = [1, 2, 3]` and `ignore_if = [99]`
+Consider the following paths from the root:
+- `[1, 2, 2, 3]` is forbidden, as the sequence does not contain `99`
+- `[1, 99, 2, 3]` is NOT forbidden, as the sequence does contain `99`
+- `[1, 99, 1, 2, 3]` is forbidden, as there is a subsequence that does not contain `99`
+"""
+struct ForbiddenSequence <: AbstractGrammarConstraint
+    sequence::Vector{Int}
+    ignore_if::Vector{Int}
+end
+
+ForbiddenSequence(sequence::Vector{Int}; ignore_if=Vector{Int}()) = ForbiddenSequence(sequence, ignore_if)
+
+function on_new_node(solver::Solver, c::ForbiddenSequence, path::Vector{Int})
+    #minor optimization: prevent the first hardfail (https://github.com/orgs/Herb-AI/projects/6/views/1?pane=issue&itemId=55570518)
+    @match get_node_at_location(solver, path) begin
+        hole::AbstractHole => if !hole.domain[c.sequence[end]] return end
+        node::RuleNode => if node.ind != c.sequence[end] return end
+    end
+    post!(solver, LocalForbiddenSequence(path, c.sequence, c.ignore_if))
+end
+
+"""
+    check_tree(c::ForbiddenSequence, tree::AbstractRuleNode; sequence_started=false)::Bool
+
+Checks if the given [`AbstractRuleNode`](@ref) tree abides the [`ForbiddenSequence`](@ref) constraint.
+"""
+function check_tree(c::ForbiddenSequence, tree::AbstractRuleNode; sequence_started=false)::Bool
+    @assert isfilled(tree) "check_tree does not support checking trees that contain holes. $(tree) is a hole."
+
+    # attempt to start the sequence on the any node in the tree
+    if !sequence_started
+        for child ∈ tree.children
+            if !check_tree(c, child, sequence_started=false)
+                return false
+            end
+        end
+    end
+
+    # add the current node to the current sequence if possible
+    if (get_rule(tree) == c.sequence[1])
+        remaining_sequence = c.sequence[2:end]
+        sequence_started = true
+    else
+        remaining_sequence = c.sequence
+    end
+
+    # the empty sequence is in any tree, so the constraint is violated
+    if isempty(remaining_sequence)
+        return false
+    end
+
+    if sequence_started
+        # the sequence contains one of the `ignore_if` rules, and therefore is satisfied
+        if get_rule(tree) ∈ c.ignore_if
+            return true
+        end
+
+        # continue the current sequence
+        smaller_constraint = ForbiddenSequence(remaining_sequence, c.ignore_if)
+        for child ∈ tree.children
+            if !check_tree(smaller_constraint, child, sequence_started=true)
+                return false
+            end
+        end
+    end
+    return true
+end

src/grammarconstraints/ordered.jl

@@ -23,12 +23,6 @@ For example, consider the tree `1(a, 2(b, 3(c, 4))))`:
 - `Ordered(RuleNode(3, [VarNode(:v), VarNode(:w)]), [:w, :v])` removes every rule 
     with an index of 4 or less from the domain of `c`, since that would make the index of the 
     assignment to `v` less than the index of the assignment to `w`, violating the order.
-
-!!! warning
-    The [`Ordered`](@ref) constraint makes use of [`AbstractLocalConstraint`](@ref)s to make sure that constraints 
-    are also enforced in the future when the context of a [`AbstractHole`](@ref) changes. 
-    Therefore, [`Ordered`](@ref) can only be used in implementations that keep track of the 
-    [`AbstractLocalConstraint`](@ref)s and propagate them at the right moments.
 """
 struct Ordered <: AbstractGrammarConstraint
     tree::AbstractRuleNode
@@ -47,7 +41,7 @@ function on_new_node(solver::Solver, c::Ordered, path::Vector{Int})
 end
 
 """
-    check_tree(c::Ordered, g::AbstractGrammar, tree::RuleNode)::Bool
+    check_tree(c::Ordered, tree::AbstractRuleNode)::Bool
 
 Checks if the given [`AbstractRuleNode`](@ref) tree abides the [`Ordered`](@ref) constraint.
 """

src/grammarconstraints/unique.jl

@@ -0,0 +1,41 @@
+"""
+    Unique <: AbstractGrammarConstraint
+
+This [`AbstractGrammarConstraint`] enforces that a given `rule` appears in the program tree at most once.
+"""
+struct Unique <: AbstractGrammarConstraint
+    rule::Int
+end
+
+
+function on_new_node(solver::Solver, c::Unique, path::Vector{Int})
+    if length(path) == 0
+        #only post a local constraint at the root
+        post!(solver, LocalUnique(path, c.rule))
+    end
+end
+
+
+"""
+    function _count_occurrences(rule::Int, node::AbstractRuleNode)::Int
+
+Recursively counts the number of occurrences of the `rule` in the `node`.
+"""
+function _count_occurrences(node::AbstractRuleNode, rule::Int)::Int
+    @assert isfilled(node)
+    count = (get_rule(node) == rule) ? 1 : 0
+    for child ∈ get_children(node)
+        count += _count_occurrences(child, rule)
+    end
+    return count
+end
+
+
+"""
+    function check_tree(c::Unique, tree::AbstractRuleNode)::Bool
+
+Checks if the given [`AbstractRuleNode`](@ref) tree abides the [`Unique`](@ref) constraint.
+"""
+function check_tree(c::Unique, tree::AbstractRuleNode)::Bool
+    return _count_occurrences(tree, c.rule) <= 1
+end

src/lessthanorequal.jl

@@ -98,7 +98,7 @@ function make_less_than_or_equal!(
     guards::Vector{Tuple{AbstractHole, Int}}
 )::LessThanOrEqualResult
     @assert isfeasible(solver)
-    path1 = get_path(get_tree(solver), hole1) #TODO: optimize. very inefficient to go from hole->path->hole
+    path1 = get_path(get_tree(solver), hole1)
     path2 = get_path(get_tree(solver), hole2)
     @match (isfilled(hole1), isfilled(hole2)) begin
         (true, true) => begin

src/localconstraints/local_contains.jl

@@ -18,33 +18,33 @@ If there is only a single hole that can potentially hold the target rule, that h
 """
 function propagate!(solver::Solver, c::LocalContains)
     node = get_node_at_location(solver, c.path)
-    track!(solver.statistics, "LocalContains propagation")
+    track!(solver, "LocalContains propagation")
     @match _contains(node, c.rule) begin
         true => begin 
-            track!(solver.statistics, "LocalContains satisfied")
+            track!(solver, "LocalContains satisfied")
             deactivate!(solver, c)
         end
         false => begin 
-            track!(solver.statistics, "LocalContains inconsistency")
+            track!(solver, "LocalContains inconsistency")
             set_infeasible!(solver)
         end
         holes::Vector{AbstractHole} => begin
             @assert length(holes) > 0
             if length(holes) == 1
                 if isuniform(holes[1])
-                    track!(solver.statistics, "LocalContains deduction")
+                    track!(solver, "LocalContains deduction")
                     path = vcat(c.path, get_path(node, holes[1]))
                     deactivate!(solver, c)
                     remove_all_but!(solver, path, c.rule)
                 else
-                    #we cannot deduce anything yet, new holes can appear underneath this hole
-                    #TODO: optimize this by checking if the target rule can appear as a child of the fixedshaped hole
-                    track!(solver.statistics, "LocalContains softfail (hole)")
+                    # we cannot deduce anything yet, new holes can appear underneath this hole
+                    # optimize this by checking if the target rule can appear as a child of the hole
+                    track!(solver, "LocalContains softfail (non-uniform hole)")
                 end
             else
-                #multiple holes can be set to the target value, no deduction can be made as this point
-                #TODO: optimize by only repropagating if the number of holes involved is <= 2
-                track!(solver.statistics, "LocalContains softfail (>= 2 holes)")
+                # multiple holes can be set to the target value, no deduction can be made as this point
+                # optimize by only repropagating if the number of holes involved is <= 2
+                track!(solver, "LocalContains softfail (>= 2 holes)")
             end
         end
     end
@@ -65,8 +65,7 @@ end
 
 function _contains(node::AbstractRuleNode, rule::Int, holes::Vector{AbstractHole})::Union{Vector{AbstractHole}, Bool}
     if !isuniform(node)
-        #TODO: check if the rule might appear underneath this non-uniform hole later
-        # for now, it is assumed this is always possible
+        # the rule might appear underneath this non-uniform hole
         push!(holes, node)
     elseif isfilled(node)
         # if the rulenode is the target rule, return true

src/localconstraints/local_forbidden.jl

@@ -20,28 +20,27 @@ Deductions are based on the type of the [`PatternMatchResult`](@ref) returned by
 """
 function propagate!(solver::Solver, c::LocalForbidden)
     node = get_node_at_location(solver, c.path)
-    track!(solver.statistics, "LocalForbidden propagation")
+    track!(solver, "LocalForbidden propagation")
     @match pattern_match(node, c.tree) begin
         ::PatternMatchHardFail => begin 
             # A match fail means that the constraint is already satisfied.
             # This constraint does not have to be re-propagated.
             deactivate!(solver, c)
-            track!(solver.statistics, "LocalForbidden hardfail")
+            track!(solver, "LocalForbidden hardfail")
         end;
         match::PatternMatchSoftFail => begin 
-            # The constraint will re-propagated on any tree manipulation.
-            # TODO: watcher. only propagate when needed.
-            track!(solver.statistics, "LocalForbidden softfail")
+            # The constraint needs to be re-propagated
+            track!(solver, "LocalForbidden softfail")
         end
         ::PatternMatchSuccess => begin 
             # The forbidden tree is exactly matched. This means the state is infeasible.
-            track!(solver.statistics, "LocalForbidden inconsistency")
+            track!(solver, "LocalForbidden inconsistency")
             set_infeasible!(solver) #throw(InconsistencyException())
         end
         match::PatternMatchSuccessWhenHoleAssignedTo => begin
             # Propagate the constraint by removing an impossible value from the found hole.
             # Then, constraint is satisfied and does not have to be re-propagated.
-            track!(solver.statistics, "LocalForbidden deduction")
+            track!(solver, "LocalForbidden deduction")
             #path = get_path(get_tree(solver), match.hole)
             path = vcat(c.path, get_path(node, match.hole))
             deactivate!(solver, c)