CHRis: Constraint Handling Rules with Indexes Specified

CHRis is an implementation of the programming language Constraint Handling Rules (CHR) embedded in Nim. As its name suggests, it extends the normal CHR language by allowing the programmer to specify the execution of CHR programs in more detail. This makes it easier to reason about efficiency and optimize programs.

CHRis was tested with versions 1.4.2, 2.0.2 and 2.2.2 of Nim and works with the C, C++ and JavaScript backends (Objective C was not tested). Unfortunately, it doesn't work at compile time.

Our running example (saved in its entirety in `tests/testdocexample.nim`) is one use case where CHR shines: an inequality solver. We have (in)equalities encoded as Constraints, containing the left and the right variable as strings:

type
    ConstraintKind = enum Equal, LessOrEqual
    Constraint = tuple
        kind: ConstraintKind
        left,right: string

func `$`(c: Constraint): string =
    ## Pretty printing
    c.left & (case c.kind
            of Equal: "="
            of LessOrEqual: "<="
        ) & c.right

const myConstraints = [
    (LessOrEqual, "A", "B"),  # A <= B
    (LessOrEqual, "B", "C"),  # etc.
    (LessOrEqual, "C", "A"),
    (LessOrEqual, "X", "Y"),
    (LessOrEqual, "Y", "X"),
    (LessOrEqual, "C", "X")
]

Now we will use CHR to derive further (in)equalities that are implied by the ones we have, for example A <= C.

Usage

Define the constraint store

First, we define the interface of our constraint store. A constraint store is a mutable multi-set of the constraints we work with.

Here, we define a type of store called InequalityStore that stores elements of type Constraint and is accessible via four indexes (an index is a data structure to efficiently retrieve specified subsets of the stored constraints):

import chris

chrStore InequalityStore(c: Constraint):
    
    # This will enable us to give a value `v` of type ConstraintKind (so either Equal or
    # LessOrEqual) and retrieve all constraints `c` where `c.kind == v`
    index[ConstraintKind] ofKind: c.kind
    
    # Retrieve all constraints that have a given left variable
    index[string] withLeft: c.left
    
    # Retrieve all duplicates of a given constraint
    index[Constraint] theConstraint: c
    
    # Give () and retrieve all constraints
    index[tuple[]] anyConstraint: ()
    
    # These kinds of indexes are known as expression (= function based) indexes.

The procs == and hash must be defined for the elements of the store. In this example, this is already the case because Constraint is a tuple.

Define the rules

Now, we write our program's main part: the constraint handling rules, which describe how constraints will be added (put) and removed from the constraint store. The rules together with a constraint store (here, the InequalityStore defined above) form a solver, which we name inequalitySolver:

chrSolver[InequalityStore] inequalitySolver:
    
    rule removeDuplicates:
        remove c ~ anyConstraint ()
        have dup ~* theConstraint c
    
    # Remove A<=B if we have A=B
    rule eqImpliesLeq:
        remove le ~ ofKind LessOrEqual
        have eq ~ theConstraint (Equal, le.left, le.right)
    
    # Remove the tautologies A=A and A<=A
    rule reflexive:
        remove c ~ anyConstraint ()
        check c.left == c.right
    
    # From A<=B and B<=C follows A<=C (similarly for =)
    rule transitive:
        have c1 ~ anyConstraint ()
        have c2 ~ withLeft c1.right
        put (kind: if c1.kind==Equal: c2.kind  else: LessOrEqual,
            left:c1.left, right:c2.right)
    
    # From A<=B and B<=A follows A=B (and B=A)
    rule antisymmetricLeq:
        have c ~ ofKind LessOrEqual
        have antiC ~* theConstraint (LessOrEqual, c.right, c.left)
        put (Equal, c.left, c.right)
        put (Equal, c.right, c.left)

Syntax

The syntax seen above is described here; for its semantics, read the following section.

A rule consists of its name and at least one clause. A clause is one of the following:

• have or remove, followed by an identifier, followed by ~ (or ~*; see passive clauses), followed by an index expression.

  The identifier becomes bound here to a value of the same type as the elements of the constraint store (in the example, Constraint). It is visible in the subsequent clauses of the same rule.

  An index expression is either indexName indexValue or, equivalently, indexName(indexValue). The index name is the name of an index defined in the constraint store of this solver. The index value is an expression of the same type as the index (which is given at the index's definition).

• put, followed by an expression of the same type as the elements of the constraint store (in the example, Constraint).
• check, followed by an expression of type bool.

Use the solver

The chrSolver template shown above creates a constructor function with which we can create instances of the solver. To submit constraints and fire the rules, call the putAndSolve proc:

var mySolver: ChrSolver[Constraint, InequalityStore] = inequalitySolver()  # Type annotation just for illustration
mySolver.putAndSolve myConstraints

The result of the computation can be observed through the `$`, `distinctLen` and `count` procs, as well as the `items` and `pairs` iterators:

echo mySolver  #~> {B=A: *1, C<=Y: *1, A=B: *1, B=C: *1, A<=X: *1, A=C: *1, C<=X: *1, C=A: *1, X=Y: *1, B<=X: *1, Y=X: *1, C=B: *1, B<=Y: *1, A<=Y: *1}
# Order may differ. *1 means one copy of a constraint.

assert mySolver.distinctLen == 14
assert mySolver.count((Equal, "C", "B")) == 1

var s: seq[Constraint]
for constraint in mySolver:
    if constraint.left == "X": s.add constraint
assert $s == "@[X=Y]"

for constraint,count in mySolver: assert count == 1

You can also access the `constraints` pseudo-attribute to make queries using the indexes you defined:

let equalities = mySolver.constraints.ofKind Equal
assert $equalities == "@[A=C: *1, C=A: *1, A=B: *1, C=B: *1, B=A: *1, B=C: *1, X=Y: *1, Y=X: *1]"
assert equalities.distinctLen == 8
var c = 0
for constraint,count in mySolver.constraints.withLeft "C": c += count
assert c == 4

You can continue to use the solver instance by further calls to putAndSolve, which will mutate the store together with the submitted constraints according to the rules.

You can instantiate the solver multiple times (by calling the constructor function multiple times) and use the instances independently. Each will use the same rules to process constraints, but will have its own constraint store.

You can use the same type of constraint store (defined with chrStore) for multiple solvers (defined with chrSolver), and – of course – you can define multiple types of constraint store.

Semantics

For better presentation, the semantics of CHR programs written with CHRis are explained in two subsections: The first subsection covers the abstract semantics, which are an accurate but imprecise specification intended to convey the main idea of how CHR programs are executed. The second subsection covers the concrete semantics, which fill in all the remaining details.

Abstract semantics

Standard put ordering

For the abstract semantics, we assume that in each rule, all put clauses appear right next to each other and at the very end of the rule. This restriction is enforced in usual CHR implementations. Thus, breaking it gives rise to nonstandard CHR programs (though they adhere to the concrete semantics), and CHRis warns about it.

Identity versus equality

Let's explain how this documentation uses the word identical, in contrast to equal. Besides the concept of equality between constraints (which is defined by the == operator), CHRis has the separate concept of identity: Every constraint created is non-identical with all others – even if it is equal to some of them. You can imagine that each constraint has a unique identifier that determines its identity.

As the rest of this section should make clear, CHRis only considers the identities of constraints when firing rules, by default. Equality is only considered if users invoke it – either by explicit comparisons in rules or implicitly via indexes (see Matching; for the example's theConstraint index, == is applied to constraints). Equality between constraints is also used by the constraint store's accessor routines, which group equal constraints together.

Firing rules

A call to putAndSolve adds the given constraints to the store of the solver instance and repeatedly fires rules.

A rule can fire if each have and remove clause it contains matches a constraint (all non-identical) from the store and all check clauses evaluate to true. (See below how matching works.)

If a rule fires, the constraints that matched the remove clauses are removed from the store. Also, for each put clause in the rule, the given constraint is created and added to the store.

This might enable further rules to fire. The call to putAndSolve fires rules and returns only when no rule can fire anymore.

Matching

Assume there is a have clause (the same holds for remove clauses) have a ~ indexName indexValue (or equivalently have a ~ indexName(indexValue)), and indexName is defined like

chrStore MyStore(c: Constraint):
    index[T] indexName: f(c)

Then, a constraint x can match the clause iff f(x) == indexValue. (Therefore, the indexes in CHRis are an example of so-called expression, or function based, indexes.) In case of a match, the identifier a is bound to the value x.

Single-chance test for firing

Once a rule has been tested for firing by matching each have and remove clause with a constraint, the same combination of matches (that is, matching each clause with the identical constraint again) won't be tested again. This holds regardless of whether or not the rule has fired and across all calls to putAndSolve on the same solver instance.

The purpose of this behavior is to prevent trivial non-determination after firing a rule without remove clauses, because the same rule could then – without this behavior – be fired infinitely often. The behavior is also necessary because the expression in a check clause is a black box that could change its value at any point in the future, but you don't want to re-evaluate it until eternity.

So you must be careful with a check clause that depends on something other than the constraints matched in the rule, because its result is effectively cached for each combination of matches and not re-evaluated. But such a check would be unidiomatic CHR anyway, so this shouldn't be a great restriction.

Concrete semantics

The abstract semantics have explained under which conditions a rule can fire and what happens if it does. The concrete semantics now explain how, among the rules that can fire, the rule to actually fire is selected. This determines not only the order, but also the total set of rules fired, because some of them may be mutually exclusive.

The constraint store is divided into two parts: the main store and the new-stack. Both are empty when the solver is instantiated.

A call to putAndSolve first pushes the submitted constraints onto the new-stack (in the reverse order; see its documentation).

Main loop

After that, putAndSolve performs the following steps in a loop:

1. The top constraint from the new-stack is popped. This constraint is now called active constraint.
2. Rules are fired. (For the order, see below.) In each firing, the active constraint is among the matched constraints, and all others come from the main store (so the new-stack is ignored). Every constraint created by put clauses is pushed onto the new-stack in the same order as the creation. This step either ends when all combinations of matches have been tried or when the active constraint is removed by a remove clause.
3. If the active constraint was not removed, it is added to the main store.

This loop terminates before step 1 when the new-stack is empty.

Handling each active constraint

Finally, the last part to explain is how rules are fired for each active constraint.

All rules are tested sequentially in the order they are defined. For each rule, the active constraint is sequentially reserved for each have or remove clause in the order they appear in the rule.

For each reservation, a backtracking search is run over the clauses of the containing rule. To get the main idea of the control flow in this search, please compare the following exemplary rule definition to a representation of its execution in pseudo-code (which is very close to the actual implementation).

The example is this rule:

rule myRule:
    have a ~ index1 expr1
    have b ~ index2 expr2
    check boolExpr
    remove c ~ index3 expr3
    put constraintExpr1
    remove d ~ index4 expr4
    put constraintExpr2
    put constraintExpr3

This is translated essentially to the following: (The shown snippet would be executed once per reservation, which makes 4 times per active constraint, because there are 4 have or remove clauses.)

for a in index1(expr1):
    for b in index2(expr2):
        if boolExpr:
            for c in index3(expr3):
                block fireLabel:
                    newStack.push constraintExpr1
                    for d in index4(expr4):
                        newStack.push constraintExpr2
                        newStack.push constraintExpr3
                        fireRule()
                        break fireLabel

There are still some details missing from the above snippet; they are given now.

A `have` or `remove` clause – if the active constraint is not currently reserved for the clause – loops over all constraints from the main store that can match the clause. The order of the iteration is unspecified. The current iteration's constraint is temporarily removed from the main store so that it cannot match subsequent have or remove clauses while it already matches the current clause. If the active constraint is currently reserved for it, the clause becomes a trivial loop over just the active constraint (if it matches) or (if not) over nothing.

`put` clauses push the given constraints onto the new-stack immediately when the backtracking search runs over them. In the standard `put` ordering, the put clauses all appear at the end of the rule and are therefore executed exactly when the rule fires. But this is not enforced, so you can write a put clause earlier in the rule (like the first put in the example), which will then be executed at different points in time.

`check` clauses are translated to if statements, causing the search to backtrack if they fail.

If the search reaches the end of the rule, the rule fires (represented by the fireRule function in the pseudo-code). This causes constraints from the main store that matched a remove clause to be permanently removed from the main store. If the active constraint is removed, the program execution now continues with step 1 of the main loop. Else, the search now needs to backtrack quite a bit, because all loops of remove clauses just had their current constraint removed and would need to continue with the next iteration, so the search continues with the next iteration of the outermost of all remove loops (i.e. the first remove in the rule).

Passive clauses

If you use ~* instead of ~ in a have or remove clause, the active constraint will not be reserved for this clause. We say that the clause becomes passive. This means that certain combinations of matches are not tested when firing rules. The intended use is to skip useless searches over combinations of matches that cannot lead to the rule firing – making the program run faster without changing its results. However, nobody can stop you from using passive clauses to change the program's results, producing nonstandard CHR.

Logging

Compile with -d:chrLog to enable logging.

The kinds of events that can be logged are enumerated and documented in the `LoggableEvents` enum. You can change which of them are logged by changing the variable `LOGGED_EVENTS` at runtime.

The logs are submitted to the Logger stored in the variable `LOGGER`. Its default value is a ConsoleLogger, but it can also be freely changed.

For example, you can enable logging of all events with

for e in LoggableEvents: LOGGED_EVENTS.incl e

By default, not all are enabled for less verbosity. If you do this before calling putAndSolve on the inequality solver in our earlier running example, the first 8 lines of the log are as follows:

DEBUG CHR: New-stack = @[A<=B, B<=C, C<=A, X<=Y, Y<=X, C<=X]
DEBUG CHR: Activated A<=B
DEBUG CHR: Stored A<=B
DEBUG CHR: Main store = {A<=B: *1}
DEBUG CHR: New-stack = @[B<=C, C<=A, X<=Y, Y<=X, C<=X]
DEBUG CHR: Activated B<=C
DEBUG CHR: Created A<=C
DEBUG CHR: Fired transitive`reservation1 (c1=A<=B, c2=B<=C)

Comparison with traditional CHR

Semantics

Unlike most CHR implementations, CHRis does not implement the so-called refined operation semantics of CHR exactly, in which, when a constraint is created, the handling of the active constraint is interrupted for the handling of the new one – which itself may be recursively interrupted. Instead, CHRis handles the active constraint completely and only then handles the newly created ones. In that, it is similar to Ivanović's CHR implementation in Java. The rationale is efficiency: CHRis can be implemented without robust iterators, propagation histories and continuations of interrupted constraints, and we also get the late-storage and tail call optimizations for free. (These and other implementation techniques are explained by Peter Van Weert: CHR for Imperative Host Languages.)

CHRis is probably the first CHR with indexes specified, which allow you to access constraints via the pre-image of arbitrary functions (not only via subsets of their attributes, as commonly used for joins). The other extension of the normal CHR semantics is not enforcing the standard `put` ordering.

User-specified optimization

In other CHR implementations, users write their program minimalistically and rely on the CHR compiler to optimize it. CHRis has another philosophy: It does no program-specific optimization. Instead, its users specify the execution of their program in more detail. So for a slight increase in verbosity, we gain transparency: We are always sure which parts of the program are optimized and which aren't.

The optimizations that are often inferred by a sufficiently smart compiler, but user-specified in CHRis are:

• The order of have, remove and check clauses. In classic CHR, they are always ordered remove – have – check, and then may be reordered by the compiler while preserving semantics (keywords: join ordering & loop-invariant code motion).
• The definition and usage of indexes (which, besides optimization, also are often actually the simplest expression of the program's semantics in CHRis).

Syntax

Constraint handling rules are traditionally classified into three categories (which are also syntactically distinguished): propagation, simplification and simpagation. In CHRis, this distinction is only implicit: Propagation rules are those with only have and no remove clauses, simplification rules those with only remove and no have clauses, and simpagation rules those which contain both types of clauses.

Often, CHR programs have multiple kinds of constraints, each storing different types of data. Unlike other CHR implementations, CHRis has no special support for constraint kinds – all constraints must be of the same Nim type –, but users can easily simulate them on their own using object variants, indexes and/or check clauses.

A feature that is present in many CHR implementations (inspired by the distinguished Prolog implementation) and absent in CHRis is pattern matching. (Though it should be possible to support tuple unpacking …)