HerbConstraints.jl Documentation

abstract type AbstractGrammarConstraint <: AbstractConstraint

Abstract type representing all user-defined constraints. Each grammar constraint has a related AbstractLocalConstraint that is responsible for propagating the constraint at a specific location in the tree. Grammar constraints should implement on_new_node to post a AbstractLocalConstraint at that new node

abstract type AbstractLocalConstraint <: AbstractConstraint

Abstract type representing all local constraints. 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!-function. Inside the propagate! function, the constraint can use the following solver functions:

• remove!: Elementary tree manipulation. Removes a value from a domain. (other tree manipulations are: remove_above!, remove_below!, remove_all_but!)
• deactivate!: Prevent repropagation. Call this as soon as the constraint is satisfied.
• set_infeasible!: Report a non-trivial inconsistency. Call this if the constraint can never be satisfied. An empty domain is considered a trivial inconsistency, such inconsistencies are already handled by tree manipulations.
• isfeasible: Check if the current tree is still feasible. Return from the propagate function, as soon as infeasibility is detected.

Manages all changes made to StateInts using StateIntBackups. Support the following functions:

• StateInt Creates a new stateful integer
• save_state! Creates a checkpoint for all stateful integers
• restore! Restores the values to the latest checkpoint

Contains <: AbstractGrammarConstraint This [AbstractGrammarConstraint] enforces that a given rule appears in the program tree at least once.

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 DomainRuleNode <: AbstractRuleNode

Matches any 1 rule in its domain. Example usage:

DomainRuleNode(Bitvector((0, 0, 1, 1)), [RuleNode(1), RuleNode(1)])

This matches RuleNode(3, [RuleNode(1), RuleNode(1)]) and RuleNode(4, [RuleNode(1), RuleNode(1)]) and UniformHole({3, 4}, [RuleNode(1), RuleNode(1)])

Forbidden <: AbstractGrammarConstraint

This [AbstractGrammarConstraint] forbids any subtree that matches the pattern given by tree to be generated. A pattern is a tree of AbstractRuleNodes.

Example

A node in the tree can be of any type <:AbstractRuleNode. For example, a RuleNode, which contains a rule index corresponding to the rule index in the AbstractGrammar and the appropriate number of children, or a VarNode, which contains a single identifier symbol.

Let's 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.

A VarNode 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.

ForbiddenSequence <: 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 since c and d are siblings (horizontal)

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

GenericSolver

Maintains a feasible partial program in a SolverState. A ProgramIterator may manipulate the partial tree with the following tree manipulations:

• substitute!
• remove!
• remove_below!
• remove_above!
• remove_all_but!

Each SolverState holds an independent propagation program. Program iterators can freely move back and forth between states using:

• new_state!
• save_state!
• load_state!

GenericSolver(grammar::AbstractGrammar, init_node::AbstractRuleNode)

Constructs a new solver, with an initial state of the provided AbstractRuleNode.

GenericSolver(grammar::AbstractGrammar, sym::Symbol)

Constructs a new solver, with an initial state using starting symbol sym

struct LessThanOrEqualHardFail <: LessThanOrEqualResult end

node1 > node2 is guaranteed under all possible assignments of the holes involved.

abstract type LessThanOrEqualResult end

A result of the less_than_or_equal function. Can be one of 3 cases:

• LessThanOrEqualSuccess
• LessThanOrEqualHardFail
• LessThanOrEqualSoftFail

struct LessThanOrEqualSoftFail <: LessThanOrEqualResult

node1 <= node2 and node1 > node2 are both possible depending on the assignment of hole1 and hole2. Includes two cases:

• hole2::AbstractHole: A failed AbstractHole-AbstractHole comparison. (e.g. AbstractHole(BitVector((1, 0, 1))) vs AbstractHole(BitVector((0, 1, 1))))
• hole2::Nothing: A failed AbstractHole-RuleNode comparison. (e.g. AbstractHole(BitVector((1, 0, 1))) vs RuleNode(2))

abstract type LessThanOrEqualSuccess <: LessThanOrEqualResult

node1 <= node2 is guaranteed under all possible assignments of the holes involved. The strictness of a LessThanOrEqualSuccess is specified by 1 of 2 concrete cases:

• LessThanOrEqualSuccessLessThan: node1 < node2
• LessThanOrEqualSuccessEquality: node1 == node2
• LessThanOrEqualSuccessWithHoles: node1 <= node2. Unable to specific.

struct LessThanOrEqualSuccessEquality <: LessThanOrEqualSuccess end

node1 == node2 is guaranteed under all possible assignments of the holes involved.

struct LessThanOrEqualSuccessEquality <: LessThanOrEqualSuccess end

node1 < node2 is guaranteed under all possible assignments of the holes involved.

struct LessThanOrEqualSuccessWithHoles <: LessThanOrEqualSuccess end

node1 <= node2 is guaranteed under all possible assignments of the holes involved. Because of the holes involved, it is not possible to specify '<' or '=='.

LocalContains

Enforces that a given rule appears at or below the given path at least once.

LocalContains

Enforces that a given tree appears at or below the given path at least once.

!!! warning: This is a stateful constraint can only be propagated by the UniformSolver. The indices and candidates fields should not be set by the user.

LocalContainsSubtree(path::Vector{Int}, tree::AbstractRuleNode)

Enforces that a given tree appears at or below the given path at least once.

LocalForbidden

Forbids the a subtree that matches the tree to be generated at the location provided by the path. Use a Forbidden constraint for enforcing this throughout the entire search space.

LocalForbiddenSequence <: AbstractLocalConstraint

Forbids the given sequence of rule nodes ending at the node at the path. If any of the rules in ignore_if appears in the sequence, the constraint is ignored.

Enforces an order over two or more subtrees that fill the variables specified in order when the pattern is applied at the location given by path. Use an Ordered constraint for enforcing this throughout the entire search space.

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 MakeEqualHardFail <: MakeEqualResult end

node1 != node2 is guaranteed under all possible assignments of the holes involved.

abstract type MakeEqualResult end

A result of the make_equal! function. Can be one of 3 cases:

• MakeEqualSuccess
• MakeEqualHardFail
• MakeEqualSoftFail

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 MakeEqualSuccess <: MakeEqualResult end

node1 == node2 is guaranteed under all possible assignments of the holes involved.

Ordered <: AbstractGrammarConstraint

A AbstractGrammarConstraint that enforces a specific order in MatchVar assignments in the pattern defined by tree. Nodes in the pattern can either be a RuleNode, which contains a rule index corresponding to the rule index in the AbstractGrammar and the appropriate number of children. It can also contain a VarNode, which contains a single identifier symbol. A VarNode can match any subtree. 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 indices. For more information, see Base.isless(rn₁::AbstractRuleNode, rn₂::AbstractRuleNode).

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.

The pattern is not matched and can never be matched by filling in holes

abstract type PatternMatchResult end

A result of the pattern_match function. Can be one of 4 cases:

• PatternMatchSuccess
• PatternMatchSuccessWhenHoleAssignedTo
• PatternMatchHardFail
• PatternMatchSoftFail

The pattern can still be matched in a non-trivial way. Includes two cases:

• multiple holes are involved. this result stores a reference to one of them
• a single hole is involved, but needs to be filled with a node of size >= 2

The pattern is exactly matched and does not involve any holes at all

The pattern can be matched when the hole is filled with any of the given ind(s).

abstract type Solver

Abstract constraint solver. Each solver should have at least the following fields:

• statistics::TimerOutput
• fix_point_running::Bool
• schedule::PriorityQueue{AbstractLocalConstraint, Int}

Each solver should implement at least:

• post!
• get_tree
• get_grammar
• set_infeasible!
• isfeasible
• HerbCore.get_node_at_location
• get_hole_at_location
• notify_tree_manipulation
• deactivate!

mutable struct SolverState

A state to be solved by the GenericSolver. A state contains of:

• tree: A partial AST
• active_constraints: The local constraints that apply to this tree. These constraints are enforced each time the tree is modified.
• isfeasible: Flag to indicate if this state is still feasible. When a propagator spots an inconsistency, this field will be set to false. Tree manipulations and further propagations are not allowed on infeasible states

StateHole <: AbstractUniformHole

StateHoles are uniform holes used by the UniformSolver. Domain manipulations are tracked for backpropagation.

• domain: A StateSparseSet representing the rule nodes this hole can take. If size(domain) == 1, this hole should act like a RuleNode
• children: The children of this hole in the expression tree.

Converts a RuleNode to a StateHole

Converts a UniformHole to a StateHole

Stateful integer that can be saved and restored by the StateManager. Supports the following functions:

• get_value
• set_value!
• increment!
• decrement!

Backup entry for the given StateInt

Manages all changes made to StateInts using StateIntBackups

Converts a BitVector domain representation to a StateSparseSet Example:

set = StateSparseSet(sm, BitVector((1, 1, 0, 0, 1, 0, 0))) #{1, 2, 5}

Create a new StateSparseSet with values [1, 2, ..., n]

Simple stack that can only increase in size. Supports backtracking by decreasing the size to the saved size.

function StateStack{T}(sm::AbstractStateManager) where T

Create an empty StateStack supporting elements of type T

function StateStack{T}(sm::AbstractStateManager, vec::Vector{T}) where T

Create a StateStack for the provided vec

A DFS-based solver that uses StateHoles that support backtracking.

UniformSolver(grammar::AbstractGrammar, fixed_shaped_tree::AbstractRuleNode)

Unique <: AbstractGrammarConstraint

This [AbstractGrammarConstraint] enforces that a given rule appears in the program tree at most once.

struct VarNode <: AbstractRuleNode

Matches any subtree and assigns it to a variable name. The LocalForbidden constraint will not match if identical variable symbols match to different trees. Example usage:

RuleNode(3, [VarNode(:x), VarNode(:x)])

This matches RuleNode(3, [RuleNode(1), RuleNode(1)]), RuleNode(3, [RuleNode(2), RuleNode(2)]), etc. but also larger subtrees such as RuleNode(3, [RuleNode(4, [RuleNode(1)]), RuleNode(4, [RuleNode(1)])])

@csgrammar_annotated Define an annotated grammar and return it as a ContextSensitiveGrammar. Allows for adding optional annotations per rule. As well as that, allows for adding optional labels per rule, which can be referenced in annotations. Syntax is backwards-compatible with @csgrammar. Examples:

g₁ = @csgrammar_annotated begin
    Element = 1
    Element = x
    Element = Element + Element := commutative
    Element = Element * Element := (commutative, transitive)
end

g₁ = @csgrammar_annotated begin
    Element = 1
    Element = x
    Element = Element + Element := forbidden_path([3, 1])
    Element = Element * Element := (commutative, transitive)
end

g₁ = @csgrammar_annotated begin
    one::            Element = 1
    variable::       Element = x
    addition::       Element = Element + Element := (
                                                       commutative,
                                                       transitive,
                                                       forbidden_path([:addition, :one]) || forbidden_path([:one, :variable])
                                                    )
    multiplication:: Element = Element * Element := (commutative, transitive)
end

function Base.collect(stack::StateStack)

Return the internal Vector representation of the stack. !!! warning: The returned vector is read-only.

Returns all elements in the set.

Returns the minimum value in the set. This function name is used instead of min to allow code reuse for domains of type BitVector and StateSparseSet.

Returns the maximum value in the set. This function name is used instead of min to allow code reuse for domains of type BitVector and StateSparseSet.

Checks if value val is in StateSparseSet s. !!! warning: This allows a StateSparseSet to be used as if it were a BitVector representation of a set

Checks if value val is in StateSparseSet s.

function Base.in(stack::StateStack, value)::Bool

Checks whether the value is in the stack.

Returns the number of values in the StateSparseSet.

function Base.push!(stack::StateStack, item)

Place an item on top of the stack.

Pretty print the StateSparseSet.

Returns the number of values in the StateSparseSet.

function Base.size(stack::StateStack)

Get the current size of the stack.

Returns the number of values in the StateSparseSet. !!! warning: This is not actually the sum of the set. It is the length of the set. This allows a StateSparseSet to be used as if it were a BitVector representation of a set

_contains(node::AbstractRuleNode, rule::Int)::Bool

Recursive helper function for the LocalContains constraint Returns one of the following:

• true, if the node does contains the rule
• false, if the node does not contain the rule
• Vector{AbstractHole}, if the node contains the rule if one the holes gets filled with the target rule

function _count_occurrences!(node::AbstractRuleNode, rule::Int, holes::Vector{AbstractHole})::Int

Recursive helper function for the LocalUnique constraint. Returns the number of certain occurrences of the rule in the tree. All holes that potentially can hold the target rule are stored in the holes vector.

!!! warning: Stops counting if the rule occurs more than once. Counting beyond 2 is not needed for LocalUnique.

function _count_occurrences(rule::Int, node::AbstractRuleNode)::Int

Recursively counts the number of occurrences of the rule in the node.

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.

Exchanges the positions in the internal representation of the StateSparseSet.

This function should be called whenever the minimum or maximum value from the set might have been removed. The minimum and maximum value of the set will be updated to the actual bounds of the set.

This function should be called whenever the maximum value from the set might have been removed. The maximum value of the set will be updated to the actual maximum of the set.

This function should be called whenever the minimum value from the set might have been removed. The minimum value of the set will be updated to the actual minimum of the set.

Converts an annotation to a constraint. commutative: creates an Ordered constraint transitive: creates an (incorrect) Forbidden constraint forbidden_path(path::Vector{Union{Symbol, Int}}): creates a ForbiddenSequence` constraint with the original rule included ... || ...: creates a OneOf constraint (also works with ... || ... || ... et cetera, though not very performant)

are_disjoint(domain1::BitVector, domain2::BitVector)::Bool

Returns true if there is no overlap in values between domain1 and domain2

are_disjoint(set1::StateSparseSet, set2::StateSparseSet)

Returns true if there is no overlap in values between set1 and set2

Should be called whenever the state of a StateInt is modified. Creates a StateIntBackup for the given StateInt. Only backup the value if this integer has not been stored during this state before Example usecase:

a = StateInt(sm, 10)
save_state!(sm)
set_value!(a, 9) #backup value 10
set_value!(a, 8) #no need to backup again
set_value!(a, 3) #no need to backup again
restore!(sm) #restores a to value 10

check_tree(c::Contains, tree::AbstractRuleNode)::Bool

Checks if the given AbstractRuleNode tree abides the Contains constraint.

check_tree(c::ContainsSubtree, tree::AbstractRuleNode)::Bool

Checks if the given AbstractRuleNode tree abides the ContainsSubtree constraint.

check_tree(c::Forbidden, tree::AbstractRuleNode)::Bool

Checks if the given AbstractRuleNode tree abides the Forbidden constraint.

check_tree(c::ForbiddenSequence, tree::AbstractRuleNode; sequence_started=false)::Bool

Checks if the given AbstractRuleNode tree abides the ForbiddenSequence constraint.

check_tree(c::Ordered, tree::AbstractRuleNode)::Bool

Checks if the given AbstractRuleNode tree abides the Ordered constraint.

function check_tree(c::Unique, tree::AbstractRuleNode)::Bool

Checks if the given AbstractRuleNode tree abides the Unique constraint.

contains_varnode(rn::AbstractRuleNode, name::Symbol)

Checks if an AbstractRuleNode tree contains a VarNode with the given name.

deactivate!(solver::GenericSolver, constraint::AbstractLocalConstraint)

Function that should be called whenever the constraint is already satisfied and never has to be repropagated.

deactivate!(solver::UniformSolver, constraint::AbstractLocalConstraint)

Function that should be called whenever the constraint is already satisfied and never has to be repropagated.

Decrease the value of the integer by 1

fix_point!(solver::Solver)

Propagate constraints in the current state until no further dedecutions can be made

freeze_state(hole::StateHole)::RuleNode

Converts a [StateHole])(@ref) to a [RuleNode]@(ref). The hole and its children are assumed to be filled.

function get_grammar(solver::GenericSolver)::AbstractGrammar

Get the grammar.

function get_grammar(solver::UniformSolver)::AbstractGrammar

Get the grammar.

get_hole_at_location(solver::GenericSolver, location::Vector{Int})::AbstractHole

Get the node at path location and assert it is a AbstractHole.

get_hole_at_location(solver::UniformSolver, path::Vector{Int})

Get the hole that is located at the provided path.

get_intersection(domain1::BitVector, domain2::BitVector)::Bool

Returns all the values that are in both domain1 and domain2

function get_max_depth(solver::GenericSolver)::SolverState

Get the maximum depth of the tree.

function get_max_depth(solver::GenericSolver)::SolverState

Get the maximum number of AbstractRuleNodes allowed inside the tree.

get_nodes(solver)

Return an iterator over all nodes in the tree

function get_nodes_on_path(root::AbstractRuleNode, path::Vector{Int})::Vector{AbstractRuleNode}

Gets a list of nodes on the path, starting (and including) the root.

function get_priority(::AbstractLocalConstraint)

Used to determine which constraint to propagate first in fix_point!. Constraints with fast propagators and/or strong inference should be propagated first.

function get_starting_symbol(solver::GenericSolver)::Symbol

Get the symbol from the solver.

function get_state(solver::GenericSolver)::SolverState

Get the current [SolverState]@(ref) of the solver.

function get_tree(solver::GenericSolver)::AbstractRuleNode

Returns the number of AbstractRuleNodes in the tree.

function get_tree(solver::UniformSolver)::AbstractRuleNode

Get the root of the tree. This remains the same instance throughout the entire search.

function get_tree_size(solver::GenericSolver)::Int

Returns the number of AbstractRuleNodes in the tree.

Get the value of the stateful integer

Increase the value of the integer by 1

is_subdomain(specific_tree::AbstractRuleNode, general_tree::AbstractRuleNode)

Checks if the specific_tree can be obtained by repeatedly removing values from the general_tree

 is_subdomain(subdomain::BitVector, domain::BitVector)
 is_subdomain(subdomain::StateSparseSet, domain::BitVector)

Checks if subdomain is a subdomain of domain. Example: [0, 0, 1, 0] is a subdomain of [0, 1, 1, 1]

isfeasible(solver::GenericSolver)

Returns true if no inconsistency has been detected. Used in several ways:

• Iterators should check for infeasibility to discard infeasible states
• After any tree manipulation with the possibility of an inconsistency (e.g. remove_below!, remove_above!, remove!)
• fix_point! should check for infeasibility to clear its schedule and return
• Some GenericSolver functions assert a feasible state for debugging purposes @assert isfeasible(solver)
• Some GenericSolver functions have a guard that skip the function on an infeasible state: if !isfeasible(solver) return end

isfeasible(solver::UniformSolver)

Returns true if no inconsistency has been detected.

load_state!(solver::GenericSolver, state::SolverState)

Overwrites the current state with the given state

function make_equal!(solver::Solver, node1::AbstractRuleNode, node2::AbstractRuleNode)::MakeEqualResult

Tree manipulation that enforces node1 == node2 if unambiguous.

function make_less_than_or_equal!(h1::Union{RuleNode, AbstractHole}, h2::Union{RuleNode, AbstractHole}, guards::Vector{Tuple{AbstractHole, Int}})::LessThanOrEqualResult

Helper function that keeps track of the guards

function make_less_than_or_equal!(h1::Union{RuleNode, AbstractHole}, h2::Union{RuleNode, AbstractHole})::LessThanOrEqualResult

Ensures that n1<=n2 by removing impossible values from holes. Returns one of the following results:

• LessThanOrEqualSuccess. When [n1<=n2].
• LessThanOrEqualHardFail. When [n1>n2] or when the solver state is infeasible.
• LessThanOrEqualSoftFail. When no further deductions can be made, but [n1<=n2] and [n1>n2] are still possible.

function make_less_than_or_equal!(solver::Solver, nodes1::Vector{AbstractRuleNode}, nodes2::Vector{AbstractRuleNode}, guards::Vector{Tuple{AbstractHole, Int}})::LessThanOrEqualResult

Helper function that tiebreaks on children.

new_state!(solver::GenericSolver, tree::AbstractRuleNode)

Overwrites the current state and propagates constraints on the tree from the ground up

notify_new_node(solver::GenericSolver, event_path::Vector{Int})

Notify all constraints that a new node has appeared at the event_path by calling their respective on_new_node function.

notify_new_nodes(solver::GenericSolver, node::AbstractRuleNode, path::Vector{Int})

Notify all grammar constraints about the new node and its (grand)children

notify_new_nodes(solver::UniformSolver, node::AbstractRuleNode, path::Vector{Int})

Notify all grammar constraints about the new node and its (grand)children

notify_tree_manipulation(solver::GenericSolver, event_path::Vector{Int})

Notify subscribed constraints that a tree manipulation has occured at the event_path by scheduling them for propagation

notify_tree_manipulation(solver::UniformSolver, event_path::Vector{Int})

Notify subscribed constraints that a tree manipulation has occured at the event_path by scheduling them for propagation

partition(hole::Hole, grammar::ContextSensitiveGrammar)::Vector{BitVector}

Partition a Hole into subdomains grouped by childtypes

Generic fallback function for commutativity. Swaps arguments 1 and 2, then dispatches to a more specific signature. If this gets stuck in an infinite loop, the implementation of an AbstractRuleNode type pair is missing.

pattern_match(rn::AbstractRuleNode, mn::AbstractRuleNode)::PatternMatchResult

Recursively tries to match AbstractRuleNode rn with AbstractRuleNode mn. Returns a PatternMatchResult that describes if the pattern was matched.

pattern_match(node::AbstractRuleNode, domainrulenode::DomainRuleNode, vars::Dict{Symbol, AbstractRuleNode})::PatternMatchResult

Comparing any AbstractRuleNode with a DomainRuleNode

pattern_match(rn::AbstractRuleNode, var::VarNode, vars::Dict{Symbol, AbstractRuleNode})::PatternMatchResult

Comparing any AbstractRuleNode with a named VarNode

pattern_match(h1::Union{RuleNode, AbstractHole}, h2::Union{RuleNode, AbstractHole}, vars::Dict{Symbol, AbstractRuleNode})::PatternMatchResult

Comparing any pair of Rulenode and/or AbstractHole. It is important to note that some AbstractHoles are already filled and should be treated as RuleNode. This is why this function is dispatched on (isfilled(h1), isfilled(h2)). The '(RuleNode, AbstractHole)' case could still include two nodes of type AbstractHole, but one of them should be treated as a rulenode.

pattern_match(rns::Vector{AbstractRuleNode}, mns::Vector{AbstractRuleNode}, vars::Dict{Symbol, AbstractRuleNode})::PatternMatchResult

Pairwise tries to match two ordered lists of AbstractRuleNodes. Typically, this function is used to pattern match the children two AbstractRuleNodes.

post!(solver::GenericSolver, constraint::AbstractLocalConstraint)

Imposes the constraint to the current state. By default, the constraint will be scheduled for its initial propagation. Constraints can overload this method to add themselves to notify lists or triggers.

post!(solver::UniformSolver, constraint::AbstractLocalConstraint)

Post a new local constraint. Converts the constraint to a state constraint and schedules it for propagation.

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!(solver::Solver, c::LocalContains)

Enforce that the rule 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::Solver, c::LocalForbiddenSequence)

function propagate!(solver::Solver, c::LocalForbidden)

Enforce that the forbidden tree does not occur at the path. The forbidden tree is matched against the AbstractRuleNode located at the path. Deductions are based on the type of the PatternMatchResult returned by the pattern_match function.

function propagate!(solver::Solver, c::LocalOrdered)

Enforce that the VarNodes in the tree are in the specified order. First the node located at the path is matched to see if the ordered constraint applies here. The nodes matching the variables are stored in the vars dictionary. Then the order is enforced within the make_less_than_or_equal! tree manipulation.

function propagate!(solver::Solver, c::LocalUnique)

Enforce that the rule 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)

Enforce that the tree appears at or below the path at least once. Nodes that can potentially become the target sub-tree are considered candidates. In case of multiple candidates, a stateful set of indices is used to keep track of active candidates.

remove!(solver::GenericSolver, path::Vector{Int}, rule_index::Int)

Remove rule_index from the domain of the hole located at the path. It is assumed the path points to a hole, otherwise an exception will be thrown.

remove!(solver::GenericSolver, path::Vector{Int}, rules::Vector{Int})

Remove all rules from the domain of the hole located at the path. It is assumed the path points to a hole, otherwise an exception will be thrown.

remove!(set::StateSparseSet, val::Int)

Removes value val from StateSparseSet set. Returns true if val was in set.

remove!(solver::Solver, path::Vector{Int}, rule_index::Int)

Remove rule_index from the domain of the hole located at the path. It is assumed the path points to a hole, otherwise an exception will be thrown.

remove!(solver::UniformSolver, path::Vector{Int}, rules::Vector{Int})

Remove all rules from the domain of the hole located at the path. It is assumed the path points to a hole, otherwise an exception will be thrown.

remove_above!(solver::GenericSolver, path::Vector{Int}, rule_index::Int)

Reduce the domain of the hole located at the path by removing all rules indices above rule_index Example: rule_index = 2. hole with domain [1, 1, 0, 1] gets reduced to [1, 0, 0, 0] and gets simplified to a RuleNode

Remove all the values greater than val from the set

remove_above!(solver::UniformSolver, path::Vector{Int}, rule_index::Int)

Reduce the domain of the hole located at the path by removing all rules indices above rule_index Example: rule_index = 2. hole with domain {1, 2, 4} gets reduced to {1}

remove_all_but!(solver::GenericSolver, path::Vector{Int}, new_domain::BitVector)

Reduce the domain of the hole located at the path, to the new_domain. It is assumed the path points to a hole, otherwise an exception will be thrown. It is assumed new_domain ⊆ domain. For example: [1, 0, 1, 0] ⊆ [1, 0, 1, 1]

remove_all_but!(solver::GenericSolver, path::Vector{Int}, rule_index::Int)

Fill in the hole located at the path with rule rule_index. It is assumed the path points to a hole, otherwise an exception will be thrown. It is assumed rule_index ∈ hole.domain.

!!! warning: If the hole is known to be in the current tree, the hole can be passed directly. The caller has to make sure that the hole instance is actually present at the provided path.

remove_all_but!(solver::GenericSolver, path::Vector{Int}, rules_to_keep::Vector{Int})

Remove all rules from the domain of the hole located at the path except for the rules in rules_to_keep.

remove_all_but!(set::StateSparseSet, val::Int)::Bool

Removes all values from StateSparseSet set, except val

remove_all_but!(set::StateSparseSet, vals::Vector{Int})::Bool

Removes all values from StateSparseSet set, except those in vals

remove_all_but!(solver::UniformSolver, path::Vector{Int}, rule_index::Int)

Fill in the hole located at the path with rule rule_index.

remove_below!(solver::GenericSolver, path::Vector{Int}, rule_index::Int)

Reduce the domain of the hole located at the path by removing all rules indices below rule_index Example: rule_index = 2. hole with domain [1, 1, 0, 1] gets reduced to [0, 1, 0, 1]

Remove all the values less than val from the set

remove_below!(solver::UniformSolver, path::Vector{Int}, rule_index::Int)

Reduce the domain of the hole located at the path by removing all rules indices below rule_index Example: rule_index = 2. hole with domain {1, 2, 4} gets reduced to {2, 4}

function remove_node!(solver::GenericSolver, path::Vector{Int})

Remove the node at the given path by substituting it with a hole of the same symbol.

Restores the StateInt stored in the StateIntBackup to its original value

Reverts all the backups since the last save_state!.

Restore state of the solver until the last save_state!

save_state!(solver::GenericSolver)

Returns a copy of the current state that can be restored by calling load_state!(solver, state)

Make a backup of the current state. Return to this state by calling restore!.

Save the current state of the solver, can restored using restore!

schedule(solver::GenericSolver, constraint::AbstractLocalConstraint)

Schedules the constraint for propagation.

set_infeasible!(solver::GenericSolver)

Function to be called if any inconsistency has been detected

set_infeasible!(solver::Solver)

Function to be called if any inconsistency has been detected

Set the value of the integer to the given val

shouldschedule(solver::Solver, constraint::AbstractLocalConstraint, path::Vector{Int})::Bool

Function that is called when a tree manipulation occured at the path. Returns true if the constraint should be scheduled for propagation.

Default behavior: return true iff the manipulation happened at or below the constraint path.

shouldschedule(::Solver, constraint::LocalForbiddenSequence, path::Vector{Int})::Bool

Return true iff the manipulation happened at or above the constraint path.

simplify_hole!(solver::GenericSolver, path::Vector{Int})

Takes a Hole and tries to simplify it to a UniformHole or RuleNode. If the domain of the hole is empty, the state will be marked as infeasible

substitute!(solver::GenericSolver, path::Vector{Int}, new_node::AbstractRuleNode; is_domain_increasing::Union{Nothing, Bool}=nothing)

Substitute the node at the path, with a new_node.

• is_domain_increasing: indicates if all grammar constraints should be repropagated from the ground up.

Domain increasing substitutions are substitutions that cannot be achieved by repeatedly removing values from domains. Example of an domain increasing event: hole[{3, 4, 5}] -> hole[{1, 2}]. Example of an domain decreasing event: hole[{3, 4, 5}] -> rulenode(4, [hole[{1, 2}], rulenode(1)]).

contains_hole(hole::StateHole)::Bool

Returns true if the hole or any of its (grand)children are not filled.

HerbCore.get_node_at_location(solver::GenericSolver, location::Vector{Int})::AbstractRuleNode

Get the node at path location.

get_node_at_location(solver::UniformSolver, path::Vector{Int})

Get the node that is located at the provided path.

get_path(solver::GenericSolver, node::AbstractRuleNode)

Get the path at which the node is located.

get_path(solver::UniformSolver, node::AbstractRuleNode)

Get the path at which the node is located.

get_rule(hole::StateHole)::Int

Assuming the hole has domain size 1, get the rule it is currently assigned to.

isfilled(hole::StateHole)::Bool

Holes with domain size 1 are fixed to a rule. Returns whether the hole has domain size 1. (holes with an empty domain are not considered to be fixed)

update_rule_indices!(c::Contains, grammar::AbstractGrammar, mapping::AbstractDict{<:Integer,<:Integer})

Updates the Contains constraint to reflect grammar changes by replacing it with a new Contains constraint using the mapped rule index.

Arguments

• c: The Contains constraint to be updated
• grammar: The grammar that changed
• mapping: Dictionary mapping old rule indices to new rule indices

update_rule_indices!(c::Contains, grammar::AbstractGrammar)

Updates the Contains constraint as required when grammar size changes. Errors if the rule index exceeds number of grammar rules.

Arguments

• c: The Contains constraint to be updated
• grammar: The grammar that changed

update_rule_indices!(c::Contains, n_rules::Integer, mapping::AbstractDict{<:Integer,<:Integer}, constraints::Vector{<:AbstractConstraint})

Updates the Contains constraint to reflect grammar changes by replacing it with a new Contains constraint using the mapped rule index.

Arguments

• c: The Contains constraint to be updated
• n_rules: The new number of rules in the grammar
• mapping: Dictionary mapping old rule indices to new rule indices
• constraints: Vector of grammar constraints containing the constraint to update

update_rule_indices!(c::Contains, n_rules::Integer)

Updates a Contains constraint to reflect grammar changes. Errors if rule index exceeds new n_rules.

Arguments

• c: The Contains constraint to be updated
• n_rules: The new number of rules in the grammar

update_rule_indices!(c::ContainsSubtree, grammar::AbstractGrammar, mapping::AbstractDict{<:Integer, <:Integer})

Updates the ContainsSubtree constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The ContainsSubtree to be updated
• grammar: The grammar that changed
• mapping: Dictionary mapping old rule indices to new rule indices

update_rule_indices!(c::ContainsSubtree, grammar::AbstractGrammar)

Updates the ContainsSubtree constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The ContainsSubtree constraint to be updated
• grammar: The grammar that changed

update_rule_indices!(c::ContainsSubtree, n_rules::Integer, mapping::AbstractDict{<:Integer, <:Integer}, ::Vector{<:AbstractConstraint})

Updates the ContainsSubtree constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The ContainsSubtree to be updated
• n_rules: The new number of rules in the grammar
• mapping: Dictionary mapping old rule indices to new rule indices

update_rule_indices!(c::ContainsSubtree, n_rules::Integer)

Updates the ContainsSubtree constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The ContainsSubtree constraint to be updated
• n_rules: The new number of rules in the grammar

update_rule_indices!(node::DomainRuleNode, n_rules::Integer, mapping::AbstractDict{<:Integer, <:Integer})

Updates the DomainRuleNode by resizing the domain vector to n_rules and remapping rule indices based mapping. Errors if the length of the domain vector exceeds new n_rules.

Arguments

• node: The current DomainRuleNode being processed
• n_rules: The new number of rules in the grammar
• mapping: Dictionary mapping old rule indices to new rule indices

update_rule_indices!(node::DomainRuleNode, n_rules::Integer)

Updates the DomainRuleNode by resizing the domain vector to n_rules. Errors if the length of the domain vector exceeds new n_rules.

Arguments

• node: The current DomainRuleNode being processed
• n_rules: The new number of rules in the grammar

update_rule_indices!(c::Forbidden, grammar::AbstractGrammar, mapping::AbstractDict{<:Integer, <:Integer})

Updates the Forbidden constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The Forbidden constraint to be updated
• grammar: The grammar that changed
• mapping: Dictionary mapping old rule indices to new rule indices

update_rule_indices!(c::Forbidden, grammar::AbstractGrammar)

Updates the Forbidden constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The Forbidden constraint to be updated.
• grammar: The new number of rules in the grammar.

update_rule_indices!(c::Forbidden, n_rules::Integer, mapping::AbstractDict{<:Integer, <:Integer}, ::Vector{<:AbstractConstraint})

Updates the Forbidden constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The Forbidden constraint to be updated
• n_rules: The new number of rules in the grammar
• mapping: Dictionary mapping old rule indices to new rule indices

update_rule_indices!(c::Forbidden, n_rules::Integer)

Updates the Forbidden constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The Forbidden constraint to be updated.
• n_rules: The new number of rules in the grammar.

update_rule_indices!(c::ForbiddenSequence, grammar::AbstractGrammar, mapping::AbstractDict{<:Integer, <:Integer})

Updates the rule indices in a ForbiddenSequence constraint by applying the given mapping to both the sequence and ignore_if fields. Errors if rule indices exceeds number of grammar rules.

Arguments

• c: The ForbiddenSequence constraint to be updated
• grammar: The grammar that changed
• mapping: Dictionary mapping old rule indices to new rule indices

update_rule_indices!(c::ForbiddenSequence, grammar::AbstractGrammar)

Updates a ForbiddenSequence constraint to reflect grammar changes. Errors if rule indices exceeds number of grammar rules.

Arguments

• c: The ForbiddenSequence constraint to be updated
• grammar: The grammar that changed

update_rule_indices!(c::ForbiddenSequence, n_rules::Integer, mapping::AbstractDict{<:Integer, <:Integer}, ::Vector{<:AbstractConstraint})

Updates the rule indices in a ForbiddenSequence constraint by applying the given mapping to both the sequence and ignore_if fields. Errors if rule indices exceeds number of grammar rules.

Arguments

• c: The ForbiddenSequence constraint to be updated
• n_rules: The new number of rules in the grammar
• mapping: Dictionary mapping old rule indices to new rule indices

update_rule_indices!(c::ForbiddenSequence, n_rules::Integer)

Updates a ForbiddenSequence constraint to reflect grammar changes. Errors if rule indices exceeds n_rules.

Arguments

• c: The ForbiddenSequence constraint to be updated
• n_rules: The new number of rules in the grammar

update_rule_indices!(c::Ordered, grammar::AbstractGrammar, mapping::AbstractDict{<:Integer, <:Integer})

Updates the Ordered constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The Ordered constraint to be updated
• grammar: The grammar that changed
• mapping: Dictionary mapping old rule indices to new rule indices

update_rule_indices!(c::Ordered, grammar::AbstractGrammar)

Updates the Ordered constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The Ordered constraint to be updated
• grammar: The grammar that changed

update_rule_indices!(c::Ordered, n_rules::Integer, mapping::AbstractDict{<:Integer, <:Integer}, ::Vector{<:AbstractConstraint})

Updates the Ordered constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The Ordered constraint to be updated
• n_rules: The new number of rules in the grammar
• mapping: Dictionary mapping old rule indices to new rule indices

update_rule_indices!(c::Ordered, n_rules::Integer)

Updates the Ordered constraint to reflect grammar changes by calling HerbCore.update_rule_indices! on its tree field.

Arguments

• c: The Ordered constraint to be updated.
• n_rules: The new number of rules in the grammar.

HerbCore.update_rule_indices!(c::Unique,
grammar::AbstractGrammar,
mapping::AbstractDict{<:Integer,<:Integer})

Updates the Unique constraint to reflect grammar changes by replacing it with a new Unique constraint using the mapped rule index.Errors if rule index exceeds number of grammar rules.

Arguments

• c: The Unique constraint to be updated
• grammar: The grammar that changed
• mapping: Dictionary mapping old rule indices to new rule indices

update_rule_indices!(c::Unique, grammar::AbstractGrammar)

Updates a Unique constraint to reflect grammar changes. Errors if rule index exceeds number of grammar rules.

Arguments

• c: The Unique constraint to be updated
• grammar: The grammar that changed

HerbCore.update_rule_indices!(c::Unique,
n_rules::Integer,
mapping::AbstractDict{<:Integer,<:Integer},
constraints::Vector{<:AbstractConstraint})

Updates the Unique constraint to reflect grammar changes by replacing it with a new Unique constraint using the mapped rule index. Errors if rule index exceeds new n_rules.

Arguments

• c: The Unique constraint to be updated
• n_rules: The new number of rules in the grammar
• mapping: Dictionary mapping old rule indices to new rule indices
• constraints: Vector of grammar constraints containing the constraint to update

update_rule_indices!(c::Unique, n_rules::Integer)

Updates a Unique constraint to reflect grammar changes. Errors if rule index exceeds new n_rules.

Arguments

• c: The Unique constraint to be updated.
• n_rules: The new number of rules in the grammar.

HerbCore.update_rule_indices!(c::VarNode, n_rules::Integer, mapping::AbstractDict{<:Integer, <:Integer})

Update the rule indices of a VarNode. As VarNodes contain no indices, this function does nothing.

 HerbCore.update_rule_indices!(c::ContainVarNodesSubtree, n_rules::Integer)

Update the rule indices of a VarNode. As VarNodes contain no indices, this function does nothing.