Constraint propagation solver and new hole types (4 PRs)

.gitignore

@@ -22,3 +22,5 @@ docs/site/
 # committed for packages, but should be committed for applications that require a static
 # environment.
 Manifest.toml
+
+_legacy

Project.toml

@@ -4,13 +4,15 @@ authors = ["Jaap de Jong <[email protected]>"]
 version = "0.1.0"
 
 [deps]
-HerbGrammar = "4ef9e186-2fe5-4b24-8de7-9f7291f24af7"
+DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"
 HerbCore = "2b23ba43-8213-43cb-b5ea-38c12b45bd45"
+HerbGrammar = "4ef9e186-2fe5-4b24-8de7-9f7291f24af7"
+MLStyle = "d8e11817-5142-5d16-987a-aa16d5891078"
 
 [compat]
-julia = "1.8"
 HerbCore = "0.1.0"
 HerbGrammar = "0.1.0"
+julia = "1.8"
 
 [extras]
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"

src/HerbConstraints.jl

@@ -2,110 +2,98 @@ module HerbConstraints
 
 using HerbCore
 using HerbGrammar
+using DataStructures
+using MLStyle
 
 """
-    PropagatorConstraint <: Constraint
+    Abstract type GrammarConstraint <: Constraint end
 
-Abstract type representing all propagator constraints.
-Each propagator constraint has an implementation of a [`propagate`](@ref)-function that takes
-
-- the [`PropagatorConstraint`](@ref)
-- a [`Grammar`](@ref)
-- a [`GrammarContext`](@ref), which most importantly contains the tree and the location 
-  in the tree where propagation should take place.
-- The `domain` which the [`propagate`](@ref)-function prunes. 
-
-The [`propagate`](@ref)-function returns a tuple containing
-
-- The pruned `domain`
-- A list of new [`LocalConstraint`](@ref)s
+Abstract type representing all user-defined constraints.
+Each grammar constraint has a related [LocalConstraint](@ref) that is responsible for propagating the constraint at a specific location in the tree.
+Grammar constraints should implement `on_new_node` to post a [LocalConstraint](@ref) at that new node
 """
-abstract type PropagatorConstraint <: Constraint end
+abstract type GrammarConstraint <: Constraint end
 
 """
     abstract type LocalConstraint <: Constraint
 
 Abstract type representing all local constraints.
 Local constraints correspond to a specific (partial) [`AbstractRuleNode`](@ref) tree.
 Each local constraint contains a `path` to a specific location in the tree.  
-Each local constraint has an implementation of a [`propagate`](@ref)-function that takes
-
-- the [`LocalConstraint`](@ref)
-- a [`Grammar`](@ref)
-- a [`GrammarContext`](@ref), which most importantly contains the tree and the location 
-  in the tree where propagation should take place.
-- The `domain` which the [`propagate`](@ref)-function prunes. 
-
-The [`propagate`](@ref)-function returns a tuple containing
-
-- The pruned `domain`
-- A list of new [`LocalConstraint`](@ref)s
+Each local constraint should implement a [`propagate!`](@ref)-function.
 
 !!! warning
     By default, [`LocalConstraint`](@ref)s are only propagated once.
-    Constraints that have to be propagated more frequently should return 
-    themselves in the list of new local constraints.
+    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 LocalConstraint <: Constraint end
 
-@enum PropagateFailureReason unchanged_domain=1
-PropagatedDomain = Union{PropagateFailureReason, Vector{Int}}
+include("csg_annotated/csg_annotated.jl")
 
-include("matchfail.jl")
-include("matchnode.jl")
-include("context.jl")
+include("varnode.jl")
 include("patternmatch.jl")
-include("rulenodematch.jl")
 
-include("csg_annotated/csg_annotated.jl")
+include("solver/solverstatistics.jl")
+include("solver/state.jl")
+include("solver/solver.jl")
+include("solver/treemanipulations.jl")
+include("solver/domainutils.jl")
 
-include("propagatorconstraints/comesafter.jl")
-include("propagatorconstraints/forbidden_path.jl")
-include("propagatorconstraints/require_on_left.jl")
-include("propagatorconstraints/forbidden.jl")
-include("propagatorconstraints/ordered.jl")
-include("propagatorconstraints/condition.jl")
-include("propagatorconstraints/one_of.jl")
+include("lessthanorequal.jl")
 
 include("localconstraints/local_forbidden.jl")
 include("localconstraints/local_ordered.jl")
-include("localconstraints/local_condition.jl")
-include("localconstraints/local_one_of.jl")
 
-export
-    AbstractMatchNode,
-    MatchNode,
-    MatchVar,
-    matchnode2expr,
-
-    GrammarContext,
-    addparent!,
-    copy_and_insert,
+include("grammarconstraints/forbidden.jl")
+include("grammarconstraints/ordered.jl")
 
-    contains_var,
 
-    PropagatorConstraint,
+export
+    GrammarConstraint,
     LocalConstraint,
-    PropagateFailureReason,
-    PropagatedDomain,
 
-    propagate,
+    VarNode,
+    pattern_match,
     check_tree,
-
-    generateconstraints!,
-
-    ComesAfter,
-    ForbiddenPath,
-    RequireOnLeft,
+
+    #grammar constraints
     Forbidden,
     Ordered,
-    Condition,
-    OneOf,
 
+    #local constraints
     LocalForbidden,
     LocalOrdered,
-    LocalCondition
-    LocalOrdered,
-    LocalOneOf
+
+    #public solver functions
+    Solver,
+    State,
+    new_state!,
+    save_state!,
+    load_state!,
+    is_feasible,
+    get_state,
+    get_tree,
+    get_grammar,
+    get_state,
+    get_node_at_location,
+    get_hole_at_location,
+    get_max_depth,
+    get_max_size,
+    get_tree_size,
+
+    #tree manipulations
+    remove!,
+    fill_hole!,
+    remove_all_but!,
+    substitute!,
+
+    #domainutils
+    is_subdomain,
+    partition,
+    are_disjoint,
+
+    #solverstatistics
+    track!
 
 end # module HerbConstraints

src/csg_annotated/csg_annotated.jl

@@ -95,6 +95,7 @@ macro csgrammar_annotated(expression)
 	is_terminal = [isterminal(rule, alltypes) for rule ∈ rules]
 	is_eval = [iseval(rule) for rule ∈ rules]
 	childtypes = [get_childtypes(rule, alltypes) for rule ∈ rules]
+    bychildtypes = [BitVector([childtypes[i1] == childtypes[i2] for i2 ∈ 1:length(rules)]) for i1 ∈ 1:length(rules)]
 	domains = Dict(type => BitArray(r ∈ bytype[type] for r ∈ 1:length(rules)) for type ∈ alltypes)
 
     return ContextSensitiveGrammar(
@@ -105,6 +106,7 @@ macro csgrammar_annotated(expression)
         bytype,
 		domains,
         childtypes,
+        bychildtypes,
         nothing,
         constraints
     )

src/grammarconstraints/forbidden.jl

@@ -0,0 +1,56 @@
+"""
+    Forbidden <: GrammarConstraint
+
+This [`GrammarConstraint`] forbids any subtree that matches the pattern given by `tree` to be generated.
+A pattern is a tree of [`AbstractRuleNode`](@ref)s. 
+Such a node can either be a [`RuleNode`](@ref), which contains a rule index corresponding to the 
+rule index in the [`Grammar`](@ref) and the appropriate number of children, similar to [`RuleNode`](@ref)s.
+It can also contain a [`VarNode`](@ref), which contains a single identifier symbol.
+A [`VarNode`](@ref) can match any subtree, but if there are multiple instances of the same
+variable in the pattern, the matched subtrees must be identical.
+Any rule in the domain that makes the match attempt successful is removed.
+
+For example, consider the tree `1(a, 2(b, 3(c, 4))))`:
+
+- `Forbidden(RuleNode(3, [RuleNode(5), RuleNode(4)]))` forbids `c` to be filled with `5`.
+- `Forbidden(RuleNode(3, [VarNode(:v), RuleNode(4)]))` forbids `c` to be filled, since a [`VarNode`] can 
+  match any rule, thus making the match attempt successful for the entire domain of `c`. 
+  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 [`LocalConstraint`](@ref)s to make sure that constraints 
+    are also enforced in the future when the context of a [`Hole`](@ref) changes. 
+    Therefore, [`Forbidden`](@ref) can only be used in implementations that keep track of the 
+    [`LocalConstraint`](@ref)s and propagate them at the right moments.
+"""
+struct Forbidden <: GrammarConstraint
+	tree::AbstractRuleNode
+end
+
+function on_new_node(solver::Solver, c::Forbidden, path::Vector{Int})
+  #minor optimization: prevent the first hardfail (https://github.com/orgs/Herb-AI/projects/6/views/1?pane=issue&itemId=55570518)
+  if c.tree isa RuleNode
+    @match get_node_at_location(solver, path) begin
+      hole::Hole => if !hole.domain[c.tree.ind] return end
+      node::RuleNode => if node.ind != c.tree.ind return end
+    end
+  end
+  post!(solver, LocalForbidden(path, c.tree))
+end
+
+"""
+    check_tree(c::Forbidden, g::Grammar, tree::RuleNode)::Bool
+
+Checks if the given [`AbstractRuleNode`](@ref) tree abides the [`Forbidden`](@ref) constraint.
+"""
+function check_tree(c::Forbidden, tree::AbstractRuleNode)::Bool
+    @match pattern_match(tree, c.tree) begin
+      ::PatternMatchHardFail => ()
+      ::PatternMatchSoftFail => ()
+      ::PatternMatchSuccess => return false
+      ::PatternMatchSuccessWhenHoleAssignedTo => ()
+    end
+    return all(check_tree(c, child) for child ∈ tree.children)
+end

src/grammarconstraints/ordered.jl

@@ -0,0 +1,66 @@
+"""
+    Ordered <: GrammarConstraint
+
+A [`GrammarConstraint`](@ref) that enforces a specific order in [`MatchVar`](@ref) 
+assignments in the pattern defined by `tree`.
+Nodes in the pattern can either be a [`RuleNode`](@ref), which contains a rule index corresponding to the 
+rule index in the [`Grammar`](@ref) and the appropriate number of children.
+It can also contain a [`VarNode`](@ref), which contains a single identifier symbol.
+A [`VarNode`](@ref) can match any subtree, but if there are multiple instances of the same
+variable in the pattern, the matched subtrees must be identical.
+
+The `order` defines an order between the variable assignments. 
+For example, if the order is `[x, y]`, the constraint will require 
+the assignment to `x` to be less than or equal to the assignment to `y`.
+The order is recursively defined by [`RuleNode`](@ref) indices. 
+For more information, see [`Base.isless(rn₁::AbstractRuleNode, rn₂::AbstractRuleNode)`](@ref).
+
+For example, consider the tree `1(a, 2(b, 3(c, 4))))`:
+
+- `Ordered(RuleNode(3, [VarNode(:v), VarNode(:w)]), [:v, :w])` removes every rule 
+  with an index of 5 or greater from the domain of `c`, since that would make the index of the 
+  assignment to `v` greater than the index of the assignment to `w`, violating the order.
+- `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 [`LocalConstraint`](@ref)s to make sure that constraints 
+    are also enforced in the future when the context of a [`Hole`](@ref) changes. 
+    Therefore, [`Ordered`](@ref) can only be used in implementations that keep track of the 
+    [`LocalConstraint`](@ref)s and propagate them at the right moments.
+"""
+struct Ordered <: GrammarConstraint
+    tree::AbstractRuleNode
+    order::Vector{Symbol}
+end
+
+function on_new_node(solver::Solver, c::Ordered, path::Vector{Int})
+    #minor optimization: prevent the first hardfail (https://github.com/orgs/Herb-AI/projects/6/views/1?pane=issue&itemId=55570518)
+    if c.tree isa RuleNode
+        @match get_node_at_location(solver, path) begin
+            hole::Hole => if !hole.domain[c.tree.ind] return end
+            node::RuleNode => if node.ind != c.tree.ind return end
+        end
+    end
+    post!(solver, LocalOrdered(path, c.tree, c.order))
+end
+
+"""
+    check_tree(c::Ordered, g::Grammar, tree::RuleNode)::Bool
+
+Checks if the given [`AbstractRuleNode`](@ref) tree abides the [`Ordered`](@ref) constraint.
+"""
+function check_tree(c::Ordered, tree::AbstractRuleNode)::Bool
+    vars = Dict{Symbol, AbstractRuleNode}()
+    if pattern_match(tree, c.tree, vars) isa PatternMatchSuccess
+        # Check variable ordering
+        for (var₁, var₂) ∈ zip(c.order[1:end-1], c.order[2:end])
+            if vars[var₁] > vars[var₂]
+                return false
+            end
+        end
+    end
+    return all(check_tree(c, child) for child ∈ tree.children)
+end
+