Build each class's state machine once per checker (#414)

Stacked on #413.

## Description
Building a state machine takes about 25 SMT checks for a small class,
and each check creates its own Z3 context. The machine only depends on
specifications, which are all registered in the first pass, so
`TypeChecker` now builds it on the first state error and reuses it for
every later error in the same checker. Finding the receiver's current
states still runs at each error.

Other options considered:
- **Eagerly, after the first pass, for every class with `@StateSet`:**
correct programs would pay the SMT cost too. Only worth it once
something needs machines without an error, e.g. the fsm diagram.
- **Once per run, cached in `Context`:** `Context` would depend on
`state_machine`, which depends on `context` (a package cycle). The other
way is a static cache that tracks when specifications change. Neither
seemed worth it for the extra hits across classes.

## Cost
Extra time of `TestExamples` on the 269 cases that exist on `main`
(summed per case, one run each; `main` takes 80.3 s):
- #413, without the cache: +29.5 s
- with this PR: +10.6 s, spread over the 54 files with state errors

## Type of change
- [x] Code refactoring

## Checklist
- [x] `mvn test` passes locally

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -2,6 +2,7 @@
 
 import java.lang.annotation.Annotation;
 import java.util.Collections;
+import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
 import java.util.Optional;
@@ -17,6 +18,9 @@
 import liquidjava.processor.context.RefinedVariable;
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.processor.facade.GhostDTO;
+import liquidjava.processor.state_machine.StateMachine;
+import liquidjava.processor.state_machine.StateMachineBuilder;
+import liquidjava.processor.state_machine.StateSolver;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.smt.SMTEvaluator;
@@ -49,6 +53,7 @@ public abstract class TypeChecker extends CtScanner {
     protected final Factory factory;
     protected final VCChecker vcChecker;
     private final Diagnostics diagnostics = Diagnostics.getInstance();
+    private final Map<String, Optional<StateMachine>> stateMachines = new HashMap<>();
 
     public TypeChecker(Context context, Factory factory) {
         this.context = context;
@@ -64,6 +69,18 @@ public Factory getFactory() {
         return factory;
     }
 
+    /**
+     * The state machine of {@code className}, built once per checker: the specifications it is built from are all known
+     * before a checker starts
+     */
+    public Optional<StateMachine> getStateMachine(String className, CtElement element) throws LJError {
+        if (!stateMachines.containsKey(className)) {
+            StateSolver solver = new StateSolver(this, element.getPosition());
+            stateMachines.put(className, StateMachineBuilder.build(this, solver, className, element));
+        }
+        return stateMachines.get(className);
+    }
+
     @Override
     public void scan(CtElement element) {
         try {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -659,12 +659,11 @@ private static List<Hint> stateHints(TypeChecker tc, RefinedFunction function, S
         if (receiver.isEmpty() || !StateMachineBuilder.canModel(function))
             return List.of();
         try {
-            StateSolver solver = new StateSolver(tc, invocation.getPosition());
-            Optional<StateMachine> machine = StateMachineBuilder.build(tc, solver, function.getTargetClass(),
-                    invocation);
+            Optional<StateMachine> machine = tc.getStateMachine(function.getTargetClass(), invocation);
             if (machine.isEmpty())
                 return List.of();
-            Set<State> current = solver.possibleStates(machine.get().states(), state, instanceName);
+            Set<State> current = new StateSolver(tc, invocation.getPosition()).possibleStates(machine.get().states(),
+                    state, instanceName);
             return StateHints.forCall(machine.get(), function, current, receiver.get());
         } catch (RuntimeException e) {
             // a failure to compute hints must not replace the error being reported