Pure ASPIF text emitter. No vaelii deps, no I/O.
ASPIF is the Potassco Answer Set Programming Intermediate Format, the ground-program protocol between gringo and clasp. We emit the full set of ground statement types: facts, normal rules, single- and multi-head choice atoms/rules, disjunctive heads, integrity constraints, weight/cardinality bodies, minimize (weak constraints), show output, projection (type 3), externals (type 5), assumptions (type 6), heuristics (type 7), and acyclicity edges (type 8).
Wire format (line-oriented, space-separated):
Line 1: asp 1 0 0
Rule: 1 <head_type> <head_size> <head...> <body_type> <body_size> <lits...>
head_type = 0 disjunctive | 1 choice
head_size may exceed 1 (disjunction a|b, choice {a;b;c})
body_type = 0 normal (list of signed literals)
= 1 weight body — see below
body literal: +atom for positive, -atom for default-negated
Weight rule:
1 <head_type> <head_size> <head...> 1 <lower_bound> <body_size>
<lit_1> <w_1> ... <lit_n> <w_n>
head fires when the sum of weights of satisfied body
literals is at least <lower_bound>. Cardinality is
the all-weights-equal-1 special case.
Minimize: 2 <priority> <n> <lit_1> <w_1> ... <lit_n> <w_n>
Project: 3 <n> <atoms...>
Output: 4 <str_len> <str> <n_conditions> <atoms...>
External: 5 <atom> <init> init = 0 free | 1 true | 2 false | 3 release
Assume: 6 <n> <signed_lits...> (static assumption block)
Heuristic:7 <modifier> <atom> <value> <priority> <body_size> <lits...>
modifier = 0 level | 1 sign | 2 factor | 3 init | 4 true | 5 false
Edge: 8 <u> <v> <body_size> <lits...> (acyclicity edge u→v)
End: 0
ASPIF has no native bound on a choice head (lb {…} ub); a bound is
expressed by putting weight-rule + integrity-constraint cardinality
enforcement beside a multi-head choice, the same way gringo does.
Atom ids are positive integers; 0 is the terminator and must not appear as an atom. String lengths in show statements count bytes (equal to character count for ASCII); non-ASCII names need UTF-8 byte counting which we do not currently handle.
The public API has two halves:
(1) Statement constructors (fact, choice, rule, choice-rule,
constraint, minimize, show) that return plain data maps.
Data form is inspectable, easy to assemble programmatically,
and trivial to unit-test.
(2) render turns a sequence of statements into the full ASPIF
text with header and terminator.
Pure ASPIF text emitter. No vaelii deps, no I/O.
ASPIF is the Potassco Answer Set Programming Intermediate Format, the
ground-program protocol between gringo and clasp. We emit the full set
of ground statement types: facts, normal rules, single- and multi-head
choice atoms/rules, disjunctive heads, integrity constraints,
weight/cardinality bodies, minimize (weak constraints), show output,
projection (type 3), externals (type 5), assumptions (type 6),
heuristics (type 7), and acyclicity edges (type 8).
Wire format (line-oriented, space-separated):
Line 1: `asp 1 0 0`
Rule: 1 <head_type> <head_size> <head...> <body_type> <body_size> <lits...>
head_type = 0 disjunctive | 1 choice
head_size may exceed 1 (disjunction `a|b`, choice `{a;b;c}`)
body_type = 0 normal (list of signed literals)
= 1 weight body — see below
body literal: +atom for positive, -atom for default-negated
Weight rule:
1 <head_type> <head_size> <head...> 1 <lower_bound> <body_size>
<lit_1> <w_1> ... <lit_n> <w_n>
head fires when the sum of weights of satisfied body
literals is at least <lower_bound>. Cardinality is
the all-weights-equal-1 special case.
Minimize: 2 <priority> <n> <lit_1> <w_1> ... <lit_n> <w_n>
Project: 3 <n> <atoms...>
Output: 4 <str_len> <str> <n_conditions> <atoms...>
External: 5 <atom> <init> init = 0 free | 1 true | 2 false | 3 release
Assume: 6 <n> <signed_lits...> (static assumption block)
Heuristic:7 <modifier> <atom> <value> <priority> <body_size> <lits...>
modifier = 0 level | 1 sign | 2 factor | 3 init | 4 true | 5 false
Edge: 8 <u> <v> <body_size> <lits...> (acyclicity edge u→v)
End: 0
ASPIF has no native *bound* on a choice head (`lb {…} ub`); a bound is
expressed by putting weight-rule + integrity-constraint cardinality
enforcement beside a multi-head choice, the same way gringo does.
Atom ids are positive integers; 0 is the terminator and must not
appear as an atom. String lengths in show statements count bytes
(equal to character count for ASCII); non-ASCII names need UTF-8
byte counting which we do not currently handle.
The public API has two halves:
(1) Statement constructors (`fact`, `choice`, `rule`, `choice-rule`,
`constraint`, `minimize`, `show`) that return plain data maps.
Data form is inspectable, easy to assemble programmatically,
and trivial to unit-test.
(2) `render` turns a sequence of statements into the full ASPIF
text with header and terminator.Bidirectional atom id table for ASPIF translation.
ASPIF atoms are positive integers; every entity referenced in the emitted program — sentex or contradiction marker — needs a unique id. Atom 0 is reserved as the ASPIF terminator and is never allocated.
The table maps three kinds of source values to atom ids, sharing a single counter so ids are unique across kinds:
(1) sentex ids — the :id field of a vaelii sentex record. These become the atoms the ASP solver reasons about.
(2) contradiction descriptors — nested sentence-shaped Clojure
values of the form
(contradiction <head> :involved [[:sentex H1] [:sentex H2] …])
where <head> is a sentence-shaped tag (e.g. (negation S),
(disjointTypes ent t-a t-b), or a user-named head emitted by
a grounding rule like (wrongBulbCount 3 4)) and :involved
lists the sentex handles that participated. Atoms backed by
contradiction descriptors get weight in the minimize statement;
the solver avoids models in which they are true.
(3) aux descriptors — auxiliary atoms used by translators (e.g. the
count ≥ N heads of cardinality weight rules). They are
distinct from contradictions: the minimize statement does not
weight them, and clasp witnesses ignore them when reconstructing
contradictions for callers.
Labels are short string identifiers that appear in clasp's witness output; we read them back during result parsing to recover the originating sentex or contradiction. Format:
s<sentex-id> — sentex-backed atoms c<atom-id> — contradiction-backed atoms a<atom-id> — aux-backed atoms
Using s/c prefixes keeps the two namespaces distinct even if a
sentex id happens to numerically match a contradiction atom id.
The table is a clojure.core/atom wrapping a plain map. Intern operations use swap! for atomicity; lookups are pure derefs. All intern operations are idempotent.
Bidirectional atom id table for ASPIF translation.
ASPIF atoms are positive integers; every entity referenced in the
emitted program — sentex or contradiction marker — needs a unique id.
Atom 0 is reserved as the ASPIF terminator and is never allocated.
The table maps three kinds of source values to atom ids, sharing a
single counter so ids are unique across kinds:
(1) sentex ids — the :id field of a vaelii sentex record. These
become the atoms the ASP solver reasons about.
(2) contradiction descriptors — nested sentence-shaped Clojure
values of the form
(contradiction <head> :involved [[:sentex H1] [:sentex H2] …])
where `<head>` is a sentence-shaped tag (e.g. `(negation S)`,
`(disjointTypes ent t-a t-b)`, or a user-named head emitted by
a grounding rule like `(wrongBulbCount 3 4)`) and `:involved`
lists the sentex handles that participated. Atoms backed by
contradiction descriptors get weight in the minimize statement;
the solver avoids models in which they are true.
(3) aux descriptors — auxiliary atoms used by translators (e.g. the
`count ≥ N` heads of cardinality weight rules). They are
distinct from contradictions: the minimize statement does not
weight them, and clasp witnesses ignore them when reconstructing
contradictions for callers.
Labels are short string identifiers that appear in clasp's witness
output; we read them back during result parsing to recover the
originating sentex or contradiction. Format:
s<sentex-id> — sentex-backed atoms
c<atom-id> — contradiction-backed atoms
a<atom-id> — aux-backed atoms
Using `s`/`c` prefixes keeps the two namespaces distinct even if a
sentex id happens to numerically match a contradiction atom id.
The table is a clojure.core/atom wrapping a plain map. Intern
operations use swap! for atomicity; lookups are pure derefs. All
intern operations are idempotent.Subprocess wrapper around the clasp ASP solver.
Consumes ASPIF text on stdin, returns parsed results as Clojure maps.
clasp exit codes encode the solve outcome (10=sat, 20=unsat, 30=optimum,
bitmask combinations) and are NOT error codes — we rely on the JSON
Result field from --outf=2 and only throw when clasp itself fails
to run or produces no parseable output.
The four modes match the user-facing reason API in vaelii.impl.asp.reason: :label, :all-optima, :classify-true, :classify-supportable.
Subprocess wrapper around the clasp ASP solver. Consumes ASPIF text on stdin, returns parsed results as Clojure maps. clasp exit codes encode the solve outcome (10=sat, 20=unsat, 30=optimum, bitmask combinations) and are NOT error codes — we rely on the JSON `Result` field from `--outf=2` and only throw when clasp itself fails to run or produces no parseable output. The four modes match the user-facing reason API in vaelii.impl.asp.reason: :label, :all-optima, :classify-true, :classify-supportable.
In-process ASP solver: a JNA binding to the native clingo C API (which
embeds clasp). Drop-in for vaelii.impl.asp.clasp/solve — same
(solve aspif-text mode) contract and return shape — but without the
subprocess + JSON round-trip.
Why in-process: it drops the per-solve fork and JSON round-trip the
subprocess pays, which is the whole win on the small programs
vaelii.impl.asp.solver routes here.
The four modes map to clingo configuration passed as command-line arguments to clingo_control_new (clingo accepts clasp's flags): --opt-mode=optN so brave/cautious enumerate over optimal models only, --enum-mode=brave|cautious, --models=0|1. Shown atoms come back as the s/c/a label strings vaelii emits via ASPIF type-4 show statements; the lexicographic cost vector comes from clingo_model_cost.
Native lib: a system libclingo (brew install clingo) reachable via jna.library.path, or an absolute path in -Dvaelii.clingo.lib. Crash isolation is lost vs the subprocess — every native return is checked and every Control is freed in a finally; a malformed program throws rather than segfaults.
In-process ASP solver: a JNA binding to the native clingo C API (which embeds clasp). Drop-in for `vaelii.impl.asp.clasp/solve` — same `(solve aspif-text mode)` contract and return shape — but without the subprocess + JSON round-trip. Why in-process: it drops the per-solve fork and JSON round-trip the subprocess pays, which is the whole win on the small programs `vaelii.impl.asp.solver` routes here. The four modes map to clingo configuration passed as command-line arguments to clingo_control_new (clingo accepts clasp's flags): --opt-mode=optN so brave/cautious enumerate over optimal models only, --enum-mode=brave|cautious, --models=0|1. Shown atoms come back as the s/c/a label strings vaelii emits via ASPIF type-4 show statements; the lexicographic cost vector comes from clingo_model_cost. Native lib: a system libclingo (brew install clingo) reachable via jna.library.path, or an absolute path in -Dvaelii.clingo.lib. Crash isolation is lost vs the subprocess — every native return is checked and every Control is freed in a finally; a malformed program throws rather than segfaults.
The real ASP backend behind vaelii.impl.solve/Solver — the edge solver.
solve.clj describes what an edge solve is: most of the KB is monotonic or
default-true with no conflict, so only the contested defeasible nodes are sent,
known-true content is fixed background, and contradictions are soft and
prioritized so a solve never fails. This namespace renders that Program to
ASPIF and reads an answer set back.
Each contested assumption is a choice atom: true means believed, false means
defeated. Known-true (:fixed) members of a contradiction are not atoms —
they hold by assumption, which is exactly what makes them background.
A contradiction #{h1 h2 ...} becomes a violation atom derived from its
contested members:
v :- a_h1, a_h2, ...
and a weak constraint minimizing v. Weak rather than hard is the whole
point: an unsatisfiable contradiction costs, it does not make the program UNSAT,
so it comes back in :violated instead of throwing.
A nogood carrying :hard true (a set/hardConstraint rule ground by
solve-context) is instead a hard integrity constraint
:- a_h1, a_h2, ...
with no violation atom and no minimize term: a model satisfying its whole body is excluded outright. That is what makes graph 3-coloring plain satisfaction rather than optimality-proving over soft violations — an adjacency clash is never tradeable. Soft nogoods (the default) keep the minimize path above.
In practice :violated comes back empty, and that is correct rather than a gap.
An irreducible known-true clash never reaches a solver: core/settle's
decide-nogood classifies it as hard and reports it directly, and
solve/program drops any nogood with no contested member. What does arrive
always has a contested member, and defeating that member always satisfies it.
The :doomed path below is therefore defensive — it costs nothing and stays
correct if nogoods ever grow beyond today's S vs (not S) pairs.
Higher ASPIF minimize priorities dominate lower ones, so the levels are:
| level | minimizes | why |
|---|---|---|
2 + rank(p) | violation atoms | satisfy contradictions, caller priority first |
1 | defeated assumptions | give up as little belief as possible |
0 | a content-keyed weight | break remaining ties stably |
Caller priorities are mapped through their ascending rank rather than used as levels directly, so any integers work and none can collide with the two levels below.
A tie between equally-good answer sets has no principled winner, but it must not
depend on assertion order — the engine-wide invariant in docs/nmtms.md. Atom ids
are allocated in solve/content-key order, and level 0 weights defeating the
greatest content-key most cheaply, mirroring the stub's choice. Same knowledge
in any order, same answer set.
edge-solver degrades rather than fails: with no clingo and no clasp reachable
it delegates to solve/local-solver, so installing it is always safe.
The real ASP backend behind `vaelii.impl.solve/Solver` — the edge solver.
`solve.clj` describes *what* an edge solve is: most of the KB is monotonic or
default-true with no conflict, so only the contested defeasible nodes are sent,
known-true content is fixed background, and contradictions are soft and
prioritized so a solve never fails. This namespace renders that `Program` to
ASPIF and reads an answer set back.
## The encoding
Each contested assumption is a **choice atom**: true means believed, false means
defeated. Known-true (`:fixed`) members of a contradiction are *not* atoms —
they hold by assumption, which is exactly what makes them background.
A contradiction `#{h1 h2 ...}` becomes a violation atom derived from its
contested members:
v :- a_h1, a_h2, ...
and a **weak** constraint minimizing `v`. Weak rather than hard is the whole
point: an unsatisfiable contradiction costs, it does not make the program UNSAT,
so it comes back in `:violated` instead of throwing.
A nogood carrying `:hard true` (a `set/hardConstraint` rule ground by
`solve-context`) is instead a **hard integrity constraint**
:- a_h1, a_h2, ...
with no violation atom and no minimize term: a model satisfying its whole body is
excluded outright. That is what makes graph 3-coloring plain satisfaction rather
than optimality-proving over soft violations — an adjacency clash is never
tradeable. Soft nogoods (the default) keep the minimize path above.
In practice `:violated` comes back empty, and that is correct rather than a gap.
An irreducible known-true clash never reaches a solver: `core/settle`'s
`decide-nogood` classifies it as *hard* and reports it directly, and
`solve/program` drops any nogood with no contested member. What does arrive
always has a contested member, and defeating that member always satisfies it.
The `:doomed` path below is therefore defensive — it costs nothing and stays
correct if nogoods ever grow beyond today's `S` vs `(not S)` pairs.
## The objective, most significant first
Higher ASPIF minimize priorities dominate lower ones, so the levels are:
| level | minimizes | why |
|---|---|---|
| `2 + rank(p)` | violation atoms | satisfy contradictions, caller priority first |
| `1` | defeated assumptions | give up as little belief as possible |
| `0` | a content-keyed weight | break remaining ties *stably* |
Caller priorities are mapped through their ascending rank rather than used as
levels directly, so any integers work and none can collide with the two levels
below.
## Determinism
A tie between equally-good answer sets has no principled winner, but it must not
depend on assertion order — the engine-wide invariant in docs/nmtms.md. Atom ids
are allocated in `solve/content-key` order, and level 0 weights defeating the
greatest content-key most cheaply, mirroring the stub's choice. Same knowledge
in any order, same answer set.
## Availability
`edge-solver` degrades rather than fails: with no clingo and no clasp reachable
it delegates to `solve/local-solver`, so installing it is always safe.Brave/cautious classification of a settled tie, and materializing one labeling as a specialization context.
in?The TMS answers what do I believe. After settle arbitrates a default/default
tie, one side is IN and the other OUT — but that answer flattens two very different
situations. A belief can be IN because every consistent way of resolving the
contradictions keeps it, or because the solver had two equally good options and
picked one. in? cannot tell them apart; both read as "believed".
Brave/cautious classification separates them by asking the solver for all optimal answer sets rather than one:
| class | in every optimum | in some optimum | meaning |
|---|---|---|---|
:true | yes | yes | forced — no consistent labeling gives it up |
:supportable | no | yes | arbitrary — the current belief is one of several |
:false | no | no | excluded — no consistent labeling holds it |
:supportable is the interesting one, and it is invisible from the TMS alone. In a
Nixon diamond both sides are :supportable: whichever the TMS committed to, the
other was equally available.
Two rules keep these from drifting apart from belief.
Classification reads the recorded program, never a recomputed one. Resolving a
tie erases its own evidence — the defeated side stops matching, so the nogood is no
longer derivable from the KB. core/last-program holds what the solver was
actually asked (see the KB record).
Labeling reads the TMS, not a fresh solve. label-context materializes the
labeling the engine committed to, taken from jtms/in?, rather than re-solving
and hoping for the same answer set back. A re-solve would usually agree, and
"usually" is not a property worth building on.
So the invariants hold by construction, and asp_label_test pins them:
:true ⊆ believed (cautious holds in the committed model)
:false ∩ believed = ∅ (excluded holds in no model, including that one)
:supportable — either way, by definition
Classification needs a real ASP backend; local-solver produces one labeling and
cannot enumerate optima. With no backend reachable, classify reports every
contested assumption as :supportable — honest (each is one of several options)
and never overclaims :true.
Brave/cautious classification of a settled tie, and materializing one labeling as
a specialization context.
## What this adds over `in?`
The TMS answers *what do I believe*. After `settle` arbitrates a default/default
tie, one side is IN and the other OUT — but that answer flattens two very different
situations. A belief can be IN because every consistent way of resolving the
contradictions keeps it, or because the solver had two equally good options and
picked one. `in?` cannot tell them apart; both read as "believed".
Brave/cautious classification separates them by asking the solver for *all* optimal
answer sets rather than one:
| class | in every optimum | in some optimum | meaning |
|---|---|---|---|
| `:true` | yes | yes | forced — no consistent labeling gives it up |
| `:supportable` | no | yes | arbitrary — the current belief is one of several |
| `:false` | no | no | excluded — no consistent labeling holds it |
`:supportable` is the interesting one, and it is invisible from the TMS alone. In a
Nixon diamond both sides are `:supportable`: whichever the TMS committed to, the
other was equally available.
## Concert with the TMS
Two rules keep these from drifting apart from belief.
**Classification reads the recorded program, never a recomputed one.** Resolving a
tie erases its own evidence — the defeated side stops matching, so the nogood is no
longer derivable from the KB. `core/last-program` holds what the solver was
actually asked (see the KB record).
**Labeling reads the TMS, not a fresh solve.** `label-context` materializes the
labeling the engine *committed to*, taken from `jtms/in?`, rather than re-solving
and hoping for the same answer set back. A re-solve would usually agree, and
"usually" is not a property worth building on.
So the invariants hold by construction, and `asp_label_test` pins them:
:true ⊆ believed (cautious holds in the committed model)
:false ∩ believed = ∅ (excluded holds in no model, including that one)
:supportable — either way, by definition
## Requirements
Classification needs a real ASP backend; `local-solver` produces one labeling and
cannot enumerate optima. With no backend reachable, `classify` reports every
contested assumption as `:supportable` — honest (each *is* one of several options)
and never overclaims `:true`.Solving as a persistent, inert artifact: assumptionRules define choices, a
solve grounds them (scoped to a base context), enumerates the optimal answer sets,
and materializes each one as its own labeling context — a genlContext child of
the base holding the chosen truth values as inert sentexes. classify then gathers
brave/cautious over those labelings.
The two imperatives (do/label Base Into) and (do/classify Into) route here.
Belief in this KB is global (one JTMS, not an ATMS): a believed (not head) in a
context that sees the base would defeat the base's head everywhere — so only one
labeling could ever exist (the do/labeling global-commit). Materializing the truth
values inert (core/assert-inert — stored and indexed but not a JTMS premise)
sidesteps that entirely: an inert sentex is never IN, so it is invisible to the
belief-filtered nogood scan, forms no contradiction, and moves no belief. Every
answer set therefore coexists as its own context, the base KB is untouched, and the
result persists in the records for inspection.
The answer persists: the labeling contexts and the classification, as inert
sentexes in the records. The grounding — the menu of candidate choice heads —
never does. A grounding is derived solver working state, recomputable from the
assumptionRules and the base's believed facts; an inert copy would carry no
justification linking it back to what produced it, so it would rot silently the
moment the base moved. The Program keys on program-local ids (see build), and
label returns the menu as :choices for a caller who wants to see it.
And what persists is replaced on re-run, never accreted: label clears a
previous run's artifacts under the same Into before writing (see clear-run!),
and classify clears its own previous classification. Truth values from two
different groundings unioned into one context assert nothing at all.
Constraints are the engine's own contradictions among the direct ground choice
heads — a (not X)/X pair, a functional predicate given two values, or a
disjoint type clash. Choices do not propagate through ordinary rules yet
(that is provenance-propagation / full clingo grounding, the named follow-ups).
Solving as a **persistent, inert** artifact: `assumptionRules` define choices, a solve grounds them (scoped to a base context), enumerates the optimal answer sets, and materializes **each one as its own labeling context** — a `genlContext` child of the base holding the chosen truth values as inert sentexes. `classify` then gathers brave/cautious over those labelings. The two imperatives `(do/label Base Into)` and `(do/classify Into)` route here. ## Why inert, and why per-answer-set Belief in this KB is global (one JTMS, not an ATMS): a *believed* `(not head)` in a context that sees the base would defeat the base's `head` everywhere — so only one labeling could ever exist (the `do/labeling` global-commit). Materializing the truth values **inert** (`core/assert-inert` — stored and indexed but not a JTMS premise) sidesteps that entirely: an inert sentex is never IN, so it is invisible to the belief-filtered nogood scan, forms no contradiction, and moves no belief. Every answer set therefore coexists as its own context, the base KB is untouched, and the result **persists in the records** for inspection. ## What persists, and what does not The **answer** persists: the labeling contexts and the classification, as inert sentexes in the records. The **grounding** — the menu of candidate choice heads — never does. A grounding is derived solver working state, recomputable from the assumptionRules and the base's believed facts; an inert copy would carry no justification linking it back to what produced it, so it would rot silently the moment the base moved. The Program keys on program-local ids (see `build`), and `label` returns the menu as `:choices` for a caller who wants to see it. And what persists is **replaced on re-run**, never accreted: `label` clears a previous run's artifacts under the same `Into` before writing (see `clear-run!`), and `classify` clears its own previous classification. Truth values from two different groundings unioned into one context assert nothing at all. ## MVP scope (docs/solving.md) Constraints are the engine's own contradictions among the **direct** ground choice heads — a `(not X)`/`X` pair, a `functional` predicate given two values, or a `disjoint` type clash. Choices do **not** propagate through ordinary rules yet (that is provenance-propagation / full clingo grounding, the named follow-ups).
Backend selector for vaelii's ASP solver. Callers (reason.clj) use
solver/solve/solver/available? so the engine can run the in-process
clingo backend (default, when libclingo + JNA are present) or fall back to
the clasp subprocess — without any caller change.
The clingo backend is loaded LAZILY via requiring-resolve so JNA/libclingo
stay optional: a plain build (without the :with-clingo profile) has no JNA
on the classpath, the resolve fails cleanly, and the facade falls back to
clasp. clasp is also the deliberate fallback for long-running daemons, since
an in-process native crash takes down the whole JVM.
Select explicitly with -Dvaelii.asp.solver or VAELII_ASP_SOLVER = clingo|clasp. Default is auto: prefer in-process clingo when it loads, else clasp.
Backend selector for vaelii's ASP solver. Callers (reason.clj) use `solver/solve`/`solver/available?` so the engine can run the in-process clingo backend (default, when libclingo + JNA are present) or fall back to the clasp subprocess — without any caller change. The clingo backend is loaded LAZILY via requiring-resolve so JNA/libclingo stay optional: a plain build (without the `:with-clingo` profile) has no JNA on the classpath, the resolve fails cleanly, and the facade falls back to clasp. clasp is also the deliberate fallback for long-running daemons, since an in-process native crash takes down the whole JVM. Select explicitly with -Dvaelii.asp.solver or VAELII_ASP_SOLVER = clingo|clasp. Default is auto: prefer in-process clingo when it loads, else clasp.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |