Choices and Aggregates

Facts, rules, and constraints are deterministic — given them, the answer set is fixed. This page is where you hand the solver a real decision, and then count, sum, and bound what it decides.

Two constructs do the work, and they pair up. A choice rule is the generate step: it offers the solver a set of candidate atoms and lets it pick a subset. Aggregates are the test step: they count, sum, and take extremes over atoms — usually the ones a choice just generated — so you can insist the result stays within bounds. Generate a space of possibilities, then prune it: that’s the shape of most ASP programs, and the shape of this page.

We’ll build one running example — assigning a workshop’s tasks to its workers.

Choice rules

A choice rule hands the solver a decision: from a set of candidate atoms, make some subset true. Choice(element, condition=...) builds one. The element is the atom being chosen, and the condition says where the candidates come from — it’s a conditional literal, so you get one candidate per way the condition can be satisfied. Cap the decision with a cardinality guard, spelled with Python’s comparison operators — the same spelling every guard in this library uses — and attach it to a rule with when(...).derive(...):

from aspalchemy import ASPProgram, Choice, Field, Predicate, Variable

class Task(Predicate, show=False):
    name: Field[str]

class Worker(Predicate, show=False):
    name: Field[str]

class Assigned(Predicate):
    task: Field[str]
    worker: Field[str]

T, W = Variable("T"), Variable("W")

program = ASPProgram()
program.fact(*(Task(name=t) for t in ["wiring", "plumbing", "painting"]))
program.fact(*(Worker(name=w) for w in ["ada", "grace"]))

# Every task goes to exactly one worker
program.when(Task(name=T)).derive(
    Choice(Assigned(task=T, worker=W), condition=Worker(name=W)) == 1
)

>>> print(program.render())
% Generated by aspalchemy ...
task("wiring").
task("plumbing").
task("painting").
worker("ada").
worker("grace").
{ assigned(T, W) : worker(W) } = 1 :- task(T).

#show.
#show assigned/2.

Read that last line as: for each task T, pick exactly one assigned atom, drawing the worker W from the workers we know about. Every comparison operator is a guard, each rendering the way clingo spells it — and a band (between two sizes) is Python’s chained comparison, exactly as it is for aggregates below. With no guard at all the subset is free:

class OnCall(Predicate):
    worker: Field[str]

>>> offers = Choice(Assigned(task=T, worker=W), condition=Worker(name=W))
>>> (offers >= 2).render()
'2 { assigned(T, W) : worker(W) }'
>>> (offers != 3).render()
'{ assigned(T, W) : worker(W) } != 3'
>>> banded = 2 <= offers <= 4
>>> banded.render()
'2 { assigned(T, W) : worker(W) } 4'

A choice that needs no conditions attaches directly with choose(), and holds unconditionally:

# A bare choice rule: hold at least one worker on call, unconditionally
coverage = Choice(OnCall(worker=W), condition=Worker(name=W))
standby = coverage >= 1
program.choose(standby)

>>> standby.render()  # in the program, a rule of its own: '1 { on_call(W) : worker(W) }.'
'1 { on_call(W) : worker(W) }'

A single choice can offer more than one kind of atom: add(element, condition=...) appends another, and the guards then bound the whole set. Guards are checked as you build — a negative size, or an impossible band like 3 <= decision <= 2, is refused right at the Python line rather than quietly becoming an unsatisfiable program:

class Approve(Predicate):
    task: Field[str]

class Defer(Predicate):
    task: Field[str]

>>> decision = Choice(Approve(task=T))
>>> decision.add(Defer(task=T))          # add() mutates, and returns nothing
>>> decision.render()
'{ approve(T); defer(T) }'

# Solve and check the choices were honored
model = program.solve().first()
for t in ["wiring", "plumbing", "painting"]:
    assert sum(1 for a in model.atoms(Assigned) if a.task == t) == 1
assert len(model.atoms(OnCall)) >= 1

And the bounds needn’t be literal integers: a Variable or Expression bound in the rule’s conditions works too, so your data can decide how many atoms to choose.

A choice is a value

A Choice is an ordinary Python value you can name, reuse, and share between rules — but its two halves, the guards and the elements, behave differently, and the difference is worth a minute.

Guards ride a separate node. A comparison operator doesn’t touch the choice — it builds a ChoiceBand, a guarded head holding this very choice (no copy: the band and the choice share elements, exactly as an aggregate comparison shares its aggregate). That’s what lets one menu be guarded two ways:

>>> menu = Choice(OnCall(worker=W), condition=Worker(name=W))
>>> weekday, weekend = menu == 1, menu == 2
>>> weekday.render()
'{ on_call(W) : worker(W) } = 1'
>>> weekend.render()
'{ on_call(W) : worker(W) } = 2'
>>> menu.render()   # the choice itself is untouched, and still reusable
'{ on_call(W) : worker(W) }'

Shared means shared: elements added to the menu before a rule captures it show up in every band over it.

>>> menu.add(OnCall(worker="hot_spare"))
>>> weekday.render()   # both bands see the new element
'{ on_call(W) : worker(W); on_call("hot_spare") } = 1'

Elements are added by mutation. add() appends to this choice and returns nothing — the same contract as list.append, so it can’t be mistaken for a value. That raises a hazard: once a rule has captured a choice — directly, or through a band guarding it — mutating it afterward would silently rewrite the rule already on record. So a captured choice freezes, and add() refuses — naming the file and line of the rule that captured it:

>>> coverage.add(OnCall(worker=W))  # coverage was captured, through standby, by program.choose() above
Traceback (most recent call last):
  ...
RuntimeError: This Choice was captured by the rule at ... and is frozen; mutating it would silently rewrite the recorded rule. Call .copy() for a fresh, mutable Choice with the same elements, or build a new Choice.

The error names the way out. copy() returns an independent, mutable choice with the same elements; since no rule holds the copy, building on it can’t rewrite anything already recorded. The copy is a bare choice — guards belong to the bands that carry them:

>>> extended = coverage.copy()   # a fresh, mutable Choice
>>> extended.add(OnCall(worker="hot_spare"))
>>> extended.render()
'{ on_call(W) : worker(W); on_call("hot_spare") }'
>>> standby.render()            # the captured band is untouched
'1 { on_call(W) : worker(W) }'

Guarding a frozen choice is fine for the same reason — a band rewrites nothing it holds. And freezing fences only mutation: a frozen choice is still a value, so more rules may capture and share it (bands included), rendering identically in each. That file:line in the error is part of the library’s habit that every error teaches.

class Weekend(Predicate, show=False):
    pass

rota = ASPProgram()
rota.fact(Worker(name="ada"), Weekend())
cover = Choice(OnCall(worker=W), condition=Worker(name=W)) == 1
rota.choose(cover)               # captured (and frozen) here...
rota.when(Weekend()).derive(cover)  # ...and shared here, legally

>>> print(rota.render())
% Generated by aspalchemy ...
worker("ada").
weekend.
{ on_call(W) : worker(W) } = 1.
{ on_call(W) : worker(W) } = 1 :- weekend.

#show.
#show on_call/1.

Aggregates

That’s the generate step; aggregates are the test. An aggregate reduces a set of atoms to a single value you can then bound. There are five — Count, Sum, SumPlus, Min, and Max — and they all share the grammar of a choice element: an element (or tuple of terms) with an optional condition, plus add() for further elements. The pair is spelled the same way everywhere ASP writes element : condition — the element first, then condition= — for a Choice, an aggregate, and a ConditionalLiteral alike. (The keyword is simply the parameter’s name, which is the same in all three; these docs always write it.)

from aspalchemy import Field, Predicate, PredicateArg

class Person(Predicate):
    name: Field[PredicateArg]
    age: Field[PredicateArg]

john = Person(name="john", age=30)
mary = Person(name="mary", age=25)

from aspalchemy import ANY, Count, Variable

X = Variable("X")
count = Count(X, condition=Person(name=X, age=ANY)) > 5

Count counts distinct matching tuples. The other four reduce the first term of each tuple: Sum adds it up (SumPlus is the same, except negative weights count as zero), and Min and Max take the extremes. So a tuple’s leading term is its weight, and any trailing terms are there only to keep tuples distinct — Sum((A, X), condition=Person(name=X, age=A)) sums one age per person, even when two people happen to share an age:

>>> from aspalchemy import Max, Sum
>>> A = Variable("A")
>>> total_age = Sum((A, X), condition=Person(name=X, age=A))
>>> total_age.render()
'#sum{ A, X : person(X, A) }'
>>> oldest = Max(A, condition=Person(name=ANY, age=A))
>>> oldest.render()
'#max{ A : person(_, A) }'

An aggregate never stands on its own. It becomes usable only inside a comparison — the guard — and that comparison then drops in wherever comparisons go: when() conditions, forbid(), require(). The count built above is already a full guard; Count(...) > 5 is just a comparison that happens to hold an aggregate. Handing a bare aggregate to a rule as though it were an atom is refused at construction — and so is asking one for a truth value, which Python’s default rules would otherwise answer with a silent True:

>>> if Count(X, condition=Person(name=X, age=ANY)):
...     pass
Traceback (most recent call last):
  ...
TypeError: An aggregate (#count{ X : person(X, _) }) has no boolean value: it aggregates inside a comparison ...

census = ASPProgram()
census.fact(john, mary, Person(name="alan", age=41))
census.require(Count(X, condition=Person(name=X, age=ANY)) >= 3)  # holds: 3 people
census.solve().first()  # would raise UnsatisfiableError if the guard failed

Guards done right

A one-sided guard is a single comparison. A band — the count has to land between two bounds — is Python’s chained comparison, written the way you would say it:

# One-sided: no worker carries more than two tasks
load = Count(T, condition=Assigned(task=T, worker=W))
program.forbid(Worker(name=W), load > 2)

# A band: total assignments between 3 and 6 — one chained comparison
class Balanced(Predicate):
    pass

workload = Count((T, W), condition=Assigned(task=T, worker=W))
program.when(3 <= workload <= 6).derive(Balanced())

The chain builds one construct — a banded aggregate — and it renders as clingo’s own doubly guarded literal, exactly as you would have written it by hand:

>>> print(program.render())
% Generated by aspalchemy ...
task("wiring").
task("plumbing").
task("painting").
worker("ada").
worker("grace").
{ assigned(T, W) : worker(W) } = 1 :- task(T).
1 { on_call(W) : worker(W) }.
:- worker(W), #count{ T : assigned(T, W) } > 2.
balanced :- 3 <= #count{ T, W : assigned(T, W) } <= 6.

#show.
#show assigned/2.
#show balanced/0.
#show on_call/1.
>>> model = program.solve().first()
>>> bool(model.atoms(Balanced))  # 3 tasks, one worker each: the band holds
True

Any pair of bounds works (3 <= workload < 7, 9 > workload > 1 — either direction), the bounds may be variables given values elsewhere in the rule, and every other boolean use of a comparison — if workload > 6:, (workload >= 3) and (workload <= 6) — still refuses with a teaching error, because those really have no truth value. A band that admits no value at all is refused at the Python line, the same check a choice’s impossible cardinality gets — an empty band renders fine but makes its rule dead:

>>> 3 <= workload <= 2
Traceback (most recent call last):
  ...
ValueError: This aggregate band is empty: no value satisfies 3 <= #count{ T, W : assigned(T, W) } <= 2, so ...

Chains are recognized over aggregates and choices only: 1 < X < 9 on plain terms is refused toward the two conditions it means, when(1 < X, X < 9). And a chain may not suspend between its bounds — a yield or await computing the upper bound would park the chain mid-flight, where its pending half cannot survive being resumed on another thread or task. The fix is one line: compute the bound first, then chain.

>>> def lazily_bounded(count):
...     return 3 <= count <= (yield)
>>> hazard = lazily_bounded(workload)
>>> next(hazard)
Traceback (most recent call last):
  ...
RuntimeError: A chained comparison may not suspend between its links: ...

(If you are curious how a Python library can see a chained comparison at all — Python gives no hook for it — chaining.py opens with the whole story and the CPython receipts that pin it.)

Writing the band as two comparisons over the same aggregate — when(workload >= 3, workload <= 6) — remains legal, renders as the two guards it says, and grounds to byte-identical solver input: gringo (clingo’s grounder — the half that instantiates your rules over the data) recognizes the shared aggregate and grounds it once. The test suite pins all three spellings — the chain, the two comparisons, and the hand-written clingo — to one aspif at the ground level. What you do want to avoid is bind-then-compare: binding the count to a variable — N == Count(...) — and then testing N against the bounds. It reads like one aggregate, but it forces gringo to ground a fresh aggregate for every feasible value of N, with the band’s width as the multiplier. Keep the variable out of it: compare the aggregate, don’t name its value.

Cardinality tests are not choices

One last place the choice syntax can trip you. In clingo, braces in what a rule derives mean choose — but the very same braces among a rule’s conditions, 2 { p(X) } 4 :- q., mean something completely different: a cardinality test, counting how many p(X) are true. Nothing is chosen. (That’s the head-versus-body split from Statements and Terms; the error below names it in clingo’s own terms.) So ASPAlchemy refuses a Choice used as a condition, and the message points at the right spelling:

>>> program.forbid(Choice(OnCall(worker=W), condition=Worker(name=W)) >= 3)
Traceback (most recent call last):
  ...
ValueError: A guarded choice belongs in a rule head, where braces CHOOSE. In a body, clingo's braces mean a cardinality TEST — a different construct aspalchemy spells as a Count comparison: Count(X, condition=...) >= n.

A cardinality test is a Count guard — which is exactly what it means — and it grounds identically to the brace form:

# "At most two workers on call" — a cardinality test, spelled as one
program.require(Count(W, condition=OnCall(worker=W)) <= 2)
model = program.solve().first()
assert len(model.atoms(OnCall)) <= 2

A two-sided test (2 { p(X) } 4 among conditions) is just the band from above: 2 <= Count(X, condition=...) <= 4. Keeping the condition-brace syntax out is a deliberate strictness — one syntax should mean one thing, and here braces mean choose, which is why they belong only in what a rule derives.

Fine print: how a chained comparison reaches the library

Nothing above needed you to know how 3 <= workload <= 6 becomes one banded literal, and that’s the point. But the mechanism deserves a few sentences here at the bottom, because there are a few consequences.

Python evaluates a chained comparison as two comparisons joined by and — (3 <= workload) and (workload <= 6), the middle operand evaluated once. The library builds the first link, answers Python’s truth-test on it by noting where in the compiled code that test happens, builds the second link, and — only when both links belong to the same chain in the same expression — merges them into one banded literal (the aggregate band above, or the doubly guarded choice head from Choice rules). A chain that never completes (a one-sided guard bound to a name, an if on an aggregate comparison, a plain and) raises a teaching error instead of keeping half a band: nothing in this machinery can lose a guard quietly.

That “where in the compiled code” is the honest caveat: the recognition reads bytecode, and it is tuned against CPython — the interpreter facts it stands on are pinned by the test suite, on every Python version the library supports. An interpreter that compiles a chain differently is not silently misread: recognition fails closed, so a chain the machinery cannot vouch for gets the same teaching error as any other incomplete chain — possibly a refusal you didn’t deserve on an exotic interpreter, but never a program missing a bound.

One shape never reaches the library at all: a chain whose middle operand is plain Python. With the aggregate at the end, the midpoint truth-test lands on an ordinary Python comparison, and Python’s own short-circuit rules apply before any aggregate is consulted. The results are logically faithful — a falsy first link makes the whole chain False, and a truthy one vanishes as vacuously true, leaving the one-sided guard — but the False is a plain bool, which any rule position then refuses loudly:

>>> tally = Count(X, condition=Person(name=X, age=ANY))
>>> 5 <= 3 <= tally                # falsy first link: Python short-circuits
False
>>> (3 <= 5 <= tally).render()     # type: ignore[attr-defined]  # truthy first link: vacuously true, one-sided guard
'#count{ X : person(X, _) } >= 5'
>>> census.require(5 <= 3 <= tally)
Traceback (most recent call last):
  ...
TypeError: require() takes a Comparison or a Predicate, got bool. require(p) makes p hold; forbid(p) makes it not hold.

One particularly visible consequence: pytest rewrites assert expressions in test files to explain failures, and its rewriter decomposes a chained comparison into the two-comparison and form — which, at the level the library sees, is no longer a chain. So a chain written inside an assert (even nested inside a call argument there) raises the teaching error rather than building the band. The rule of thumb in tests is one you’d probably follow anyway — build the guard on its own line, then assert about it:

banded = 3 <= Count(X, condition=Person(name=X, age=ANY)) <= 6  # the chain, on its own line
# assert on `banded` (or on what a program containing it solves to) from here

Everywhere else — modules, scripts, doctests, notebooks — a chain is just a chain. And whichever way it goes wrong, it goes wrong loudly: the failure mode is an error that names the problem, never a program missing a bound. In a test module you don’t even have to remember this section: the library notices a pytest-rewritten module when it raises and appends exactly this advice to the error.