JavaTypeUnifyASP

Step ② of the pipeline: typing constraints → a type assignment. Takes the .cons file JavaConstraintGenerator produces, turns it into ASP facts, solves them with clingo, and turns the answer set back into JSON.

See ../README.md for the whole flow and src/main/asp/unifyFinal.lp for the encoding, whose comments map every rule to its counterpart in the dissertation.

CLI

java -jar target/JavaTXcompiler-0.1-jar-with-dependencies.jar <subcommand> [args]

Subcommand	Purpose
gen-facts <in.cons> <out.lp>	constraints → ASP facts
cycle-check-facts <in.cons> <out.lp>	facts for the cycle pre-check (below)
gen-facts-pruned <in.cons> <brave-atoms.txt> <out.lp>	as gen-facts, minus the alternatives the pre-check ruled out
parse-solution <atoms.txt> <out.json>	answer set → placeholder-name → type JSON

The cycle pre-check

A constraint set can force a type placeholder to equal a type that properly contains it — for example _r <. C<_p> together with _p <. _res <. _r, which makes _p =. C<_p>. No finite type satisfies that.

The encoding already says so: the Anti Cycle Conditions (Build / Connect / Fail-Cycle) exist for exactly this case. But they are integrity constraints, and clingo evaluates those only once grounding has finished — while on a cyclic set grounding is precisely what does not terminate. Each Subst-Param firing nests a type one level deeper, and maxdepth(5) bounds the depth but not the branching, so the ground program grows out of reach. The symptom is a hang with Rules: 0, never an UNSAT. See ../ASP_BUGS.md, Bug 5.

So the check runs before the solve, in src/main/asp/cycleCheck.lp. It builds no type terms at all — only a graph over placeholder identities — and therefore grounds in milliseconds however deep the types in the constraint set are.

Two kinds of edge, and the distinction is the whole point:

Edge	From	Meaning
containsEdge	_r <. C<_p>, _r =. C<_p>, C<_p> =. _r	solving _r means solving _p inside it
flowEdge	_p <. _res, _p =. _res	_p's type flows into _res's

A selection of or-constraint alternatives is cyclic iff its graph has a cycle through at least one containsEdge. A cycle of flow edges alone (_a <. _b <. _a) is harmless — it just means the two are the same type.

Because a cycle usually needs a particular combination of alternatives from different or-constraints, the question is combinatorial, so clingo answers it — in one call:

clingo --enum-mode=brave cycle_facts.lp src/main/asp/cycleCheck.lp

• UNSATISFIABLE → no acyclic selection exists → the constraint set has no finite solution. Report it and stop, instead of hanging.
• otherwise → the brave consequences (the last answer clingo prints, not the first) are exactly the alternatives occurring in at least one acyclic selection. Anything absent belongs to no solution, and gen-facts-pruned drops it.

Dropping is sound because every satisfiable selection is acyclic. Measured on a set with four cyclic alternatives and one acyclic one:

	outcome	ground rules	time
unpruned	never finishes grounding	0	> 65 s
pruned	SATISFIABLE	265	4 ms

../pipeline.sh runs this automatically as part of step 2.

Caveat. Sound only because F-bounded definitions (class X extends C<X>) are out of scope — the dissertation excludes them where it argues that restricting substitution to placeholder-free types preserves completeness. With an F-bounded class in the table, a type containing itself can be legitimate and this check would reject a satisfiable set.

Limitation. Pruning removes an alternative only when it is cyclic in every selection. Where cyclic and acyclic selections coexist and both remain reachable, grounding still explores the cyclic ones. The corrected connect rule in unifyFinal.lp is the in-solver backstop for what the pre-check cannot see.