From 5e61c548d7f06b55376da74f1298a538099a13c3 Mon Sep 17 00:00:00 2001 From: Siddhartha Prasad Date: Fri, 22 May 2026 08:45:18 -0400 Subject: [PATCH 1/3] [design] Counterfactual instances on UNSAT (proposal) Adds Notes/counterfactual-unsat.md sketching a relaxation pass in the Forge/Pardinus layer: on UNSAT, drop minimum core formulas, re-solve, and return a near-instance plus the dropped constraint list over the existing Sterling websocket. Scope is intentionally narrow to the Racket-side work: - new RelaxedSat result type - naive drop-and-retry relaxation loop in forge/solver-specific/pardinus.rkt - new status "counterfactual" + dropped field on the JSON envelope (extending the channel PR #312 already established) - real instance XML via the existing SAT path in modelToXML.rkt Sterling / CopeAndDrag-side rendering (custom themes, per-tuple violation annotations) is explicitly out of scope and treated as a downstream follow-on PR against the CnD repo. Builds on PR #312 (Nelson, Nov 2025), which already plumbed the unsat core onto the Sterling websocket. No code yet. Co-Authored-By: Claude Opus 4.7 --- Notes/counterfactual-unsat.md | 267 ++++++++++++++++++++++++++++++++++ 1 file changed, 267 insertions(+) create mode 100644 Notes/counterfactual-unsat.md diff --git a/Notes/counterfactual-unsat.md b/Notes/counterfactual-unsat.md new file mode 100644 index 00000000..c4b5fa30 --- /dev/null +++ b/Notes/counterfactual-unsat.md @@ -0,0 +1,267 @@ +# Counterfactual Instances on UNSAT (Proposal) + +This document sketches a feature for Forge: when a `run` returns UNSAT, +run a **relaxation pass** in the solver layer — drop minimum core +formulas, re-solve, and return a near-instance plus the list of dropped +constraints. Ship the result over the existing Sterling websocket so the +visualizer has a real instance to render instead of the placeholder +UNSAT sig. + +**Scope of this proposal:** Forge / Pardinus (Racket) only — the +relaxation pass and the minimum wire-format change needed to carry the +near-instance back to Sterling. Sterling / CopeAndDrag-side rendering +work (custom themes, per-tuple violation annotations, dedicated UI) is +a separate follow-on effort and is explicitly out of scope here. + +**Status:** design proposal, no code yet. Branch `counterfactual-unsat`, +based on `edit-update`. + +## Motivation + +UNSAT today produces a placeholder `` in the +visualizer plus a list of core formulas shipped on the side via the +JSON `'core` field (PR #312). The user gets a textual error report but +no instance to point at. We have most of the machinery to do better: + +1. Pardinus already extracts unsat cores mapped back to Forge AST nodes + (`forge/solver-specific/pardinus.rkt` L191–199; + `forge/solver-specific/pardinus-cores.rkt`). +2. PR #312 (Nelson, Nov 2025) already ships the core to Sterling as a + structured JSON field — the bridge from the Racket solver to the + visualizer is in place. +3. SpyTial's spytial-core has been doing the analogous workflow for + *spatial* constraints for a year: MFS (maximal feasible subset) + + IIS (irreducible infeasible subsystem). We're proposing the same + idea one layer up, on the logical spec itself, in the solver. + +Spytial's framing: *the diagram is part of the denotation*. UNSAT with a +placeholder sig is better than UNSAT with nothing — but UNSAT with a +real instance plus the dropped formulas is the actual goal. This +proposal does the half that lives in Forge; the visualizer half can be +landed independently once a real instance is on the wire. + +## What's already in place (PR #312 and surrounding work) + +Before describing what to add, here's what `edit-update` already has, so +the new work is scoped against it accurately: + +| File | What it does today | +|------|--------------------| +| `forge/sigs-structs.rkt` (L50–57) | `Unsat` struct carries `core : (U False (Listof (U node String)))` — node for AST-mapped formulas, string for unmappable ones. | +| `forge/solver-specific/pardinus.rkt` (L48, L191–199) | Configures Pardinus with `:core-gran` and `:core-minimization`. On UNSAT, pretty-prints the core to stderr. | +| `forge/solver-specific/pardinus-cores.rkt` (L18–90) | Maps Pardinus path IDs back to Forge AST nodes and pretty-prints with source locations. | +| `forge/server/modelToXML.rkt` (L151–152, L222–228) | On UNSAT, reads `(Unsat-core soln)` and emits a synthetic `` placeholder in the XML. | +| `forge/server/forgeserver.rkt` (L225–252) | `make-status-value` returns `"unsat"`; `make-core-value` deparses the core list and ships it via the JSON `'core` field on the websocket. | + +So the wire already carries `{ status: "unsat", core: [...], data: }`. The piece that's missing is **a real instance in the `data` field**. + +## Architecture (in scope) + +All proposed work is in Layer 1. The visualizer is treated as an +unchanged downstream consumer that already speaks the JSON envelope: + +``` +┌─────────────────────────────────────────────────────────────────┐ +│ Layer 1 — Forge / Pardinus (Racket) [in scope] │ +│ │ +│ Forge spec ──► Pardinus ──► UNSAT + core [exists today] │ +│ │ │ +│ ▼ │ +│ Relaxation pass [NEW] │ +│ (drop minimum core, │ +│ re-solve until SAT or │ +│ budget exhausted) │ +│ │ │ +│ ▼ │ +│ RelaxedSat (instance + │ +│ dropped constraint set) [NEW] │ +│ │ │ +│ ▼ │ +│ modelToXML.rkt + forgeserver.rkt │ +│ emit real instance XML, ship │ +│ dropped list on JSON envelope [NEW branch] │ +└──────────────────────────────────┬──────────────────────────────┘ + │ websocket JSON (existing + │ envelope from PR #312) + ▼ + Sterling / CopeAndDrag [unchanged, downstream] + renders the real instance via its existing SAT + path; the dropped formulas land on the existing + 'core channel (or new 'dropped — see wire format). + Richer visualizer-side rendering is a separate PR + against the CopeAndDrag repo. +``` + +The seam to defend in review: nothing in this proposal requires +Sterling / CnD to change to deliver value. The existing SAT-instance +renderer already knows how to draw the XML body, and the existing +core-rendering path (PR #312) already knows how to show the dropped +formulas. The win from this proposal is that the XML body becomes a +real instance instead of a placeholder. + +## Landing Zones + +### Solver pipeline (Racket) + +| File | Today | Change | +|------|-------|--------| +| `forge/sigs-structs.rkt` (L44–57) | `Sat` and `Unsat` are disjoint result types. | Either add a `RelaxedSat` variant carrying `(instance, dropped-constraints, original-core)`, or add `relaxed?: Boolean` plus a `dropped` field to `Sat`. The latter is fewer touch-points but couples relaxation data to the SAT path; the former keeps types honest. Recommend `RelaxedSat`. | +| `forge/solver-specific/pardinus.rkt` (L170–203) | `get-next-kodkod-model` returns `Sat` or `Unsat`. Already detects UNSAT, has the core, prints to stderr. | When a new `counterfactual` option is set and the result is `Unsat` with a core, enter a relaxation loop: pop a core formula, re-issue the solve with that formula's assertion suppressed, repeat until SAT (or a budget is exhausted). Wrap the resulting `Sat` as `RelaxedSat`. | +| `forge/solver-specific/pardinus-cores.rkt` (L18–90) | Maps Pardinus path IDs back to Forge AST nodes; pretty-prints. | Reusable as-is. The relaxation loop needs the AST-mapped core to know what to drop and what to report. | +| `forge/send-to-solver.rkt` (L46–48) | Defines the result contract `(U Sat Unsat Unknown)`. | Widen to include `RelaxedSat`. | + +**The hard part is the relaxation strategy.** Three options, in order of +ambition: + +1. **Naive drop-and-retry.** Each iteration, pick the smallest formula in + the minimized core, suppress it, re-solve. Stop when SAT. Cheap to + implement, no MaxSAT primitive needed. Result is *some* MFS, not + necessarily the largest. +2. **MUS/MCS enumeration (MARCO-style).** Enumerate minimal correction + sets over the core. Surface the smallest MCS as the "constraints to + drop"; solve once more with those removed. Better explanations, more + solver calls. +3. **Native partial-MaxSAT in Pardinus.** Would require the upstream + Kodkod fork to expose MaxSAT, which I don't believe it does today. + Mentioned for completeness; out of scope for v1. + +Recommend (1) for the first cut. The user-visible quality bar is "an +instance with *some* constraints noted as dropped"; (1) clears that bar. + +### Wire format (minimum needed to ship the instance) + +The JSON envelope (`make-sterling-data` in `forge/server/forgeserver.rkt` +L239–) already has `status`, `data`, and `core` fields. The smallest +viable change to deliver a near-instance to Sterling: + +| Field | Today | Proposed | +|-------|-------|----------| +| `status` | `"sat" \| "unsat" \| "unknown" \| "error"` | Add `"counterfactual"`. Older Sterling clients that don't recognize it fall back to the `"sat"` rendering path, which is the correct behavior — there *is* an instance in `data`. | +| `data` (XML) | Placeholder `` on UNSAT. | Real instance XML, generated by reusing the existing SAT path in `modelToXML.rkt` with the relaxed model. **This is the main user-visible win.** | +| `core` | List of deparsed core formulas (from PR #312). | Unchanged on true `"unsat"`. On `"counterfactual"`, leave empty (or omit). | +| `dropped` (new) | — | List of `{ id, location, formula }` records for each formula suppressed during relaxation. Same deparse format as `core` — reuse `make-core-value` machinery. | + +`modelToXML.rkt` already has a special-case branch for `Unsat` kind +`'unsat` (L222–228) and separate branches for `'no-more-instances` and +`'no-counterexample`. Add a fourth branch for `RelaxedSat` that falls +through to the existing SAT-instance generator with the same atom / +relation walker, then attaches the dropped list at the envelope level +in `forgeserver.rkt`. + +**Not in this proposal:** per-tuple `violates` annotations in the XML. +That's the bridge between solver-side relaxation and richer +visualizer-side rendering, and it can be added later without breaking +the wire format defined here. + +## User-facing surface + +Two new Forge options on `run`: + +```forge +run {} for 5 Node, counterfactual on, counterfactual_budget 3 +``` + +- `counterfactual on/off` — enables the relaxation pipeline on UNSAT. +- `counterfactual_budget N` — max formulas to drop before giving up. + +Without these options, UNSAT behavior is unchanged: students who haven't +opted in see exactly what PR #312 already delivers, and there is no +solver overhead on the SAT path. + +## Phased delivery + +This branch is intentionally small and stops at "real instance on the +wire." Suggested PR sequence inside Forge: + +1. **This doc.** Land the design first so the interface is reviewed + before the implementation, in the spirit of `Notes/Bounds.md`. +2. **Result-type widening + naive relaxation.** Add `RelaxedSat`, plumb + through `send-to-solver.rkt`, implement strategy (1) above. Gate on + the new `counterfactual` option. Unit tests using existing + `forge/tests/forge/e2e/` harness. +3. **Wire extension.** Add `status: "counterfactual"` and `dropped` + field to the JSON envelope; new `modelToXML.rkt` branch that emits + a real instance for `RelaxedSat`. After this PR the feature is + end-to-end visible in Sterling (rendered through the existing SAT + path). + +**Out of this proposal**, but natural follow-ons: + +- **CopeAndDrag theme + parser.** Separate PR against the CopeAndDrag + repo. Recognize `status: "counterfactual"`, render the `dropped` + list as a side panel, optionally consume `violates="…"` annotations + if/when added. +- **Witness annotations.** Add `violates="cN"` per-tuple attributes in + the XML for the easy quantifier-shape cases (see open questions). +- **MCS enumeration** for higher-quality dropped sets. + +## Open questions + +- **Witness attribution.** Given a dropped formula `all n: Node | n.next != n`, + which tuples in the relaxed instance "witness" the violation? For + quantifier-free or universally-quantified facts this is mechanical + (evaluate the negation against the instance, collect the binders). + For nested quantifiers / Skolemized formulas it's the same provenance + problem Amalgam tackled. Worth scoping v1 to the easy case and falling + back to "no witness, just listed in side panel" otherwise. +- **Determinism.** Spytial's IIS is "quasi-deterministic" — same failure, + same diagnostic. Naive drop-and-retry depends on core ordering, which + Pardinus does not guarantee stable. We should sort the core by AST + source location before picking, so the same spec always produces the + same counterfactual. +- **Interaction with temporal mode.** Does the relaxation play with + `min/max-trace-length`? Probably yes — a dropped constraint just yields + a trace satisfying everything else — but worth a test in + `forge/tests/temporal/`. +- **Bounds vs. facts.** Should we ever drop bounds (e.g., `exactly 3 Node`) + or only logical constraints? Recommend: facts/preds/run blocks only. + Bounds are usually intentional scope; dropping them silently would be + surprising. (Also avoids interacting with the bounds reconciliation + work in `Notes/Bounds.md`.) +- **Relationship to `'no-counterexample` and `'no-more-instances` kinds.** + Both already get special XML branches in `modelToXML.rkt`. + Counterfactual mode should be a no-op for those — they're not "unsat + because of contradicting facts," so relaxation has no semantic meaning. +- **Performance.** Worst case is O(|core|) solve calls. For pedagogical + models this is fine; for research-scale specs the budget option needs + to be a hard wall. + +## Relationship to prior Alloy work + +This isn't a new idea in the Alloy lineage — it's the natural fusion of +several existing strands that have not been integrated: + +- **Aluminum** (Nelson, Saghafi, Dougherty et al.) — minimal / + locally-minimal instance generation. Different problem (find the + *smallest* SAT instance) but same "don't just return SAT/UNSAT, return + something more interesting" instinct. +- **Amalgam** (Nelson et al.) — provenance / why / why-not over + instances. Directly applicable to the witness-attribution open + question above. +- **PR #312** (Nelson, Nov 2025) — already moved the unsat core onto the + Sterling wire. This proposal is the next step on the same trajectory: + instead of just shipping the core, ship a counterfactual instance + derived from it. +- **Sterling / CopeAndDrag** — already the extension point for richer + post-solve UX, and CnD inherits that surface. + +What's new here is *packaging*: making "UNSAT → counterfactual diagram" +the default debugging experience for a Forge student, not a research +artifact that requires opting in to a separate tool. + +## Out of scope (v1) + +- **Visualizer-side rendering work** in Sterling / CopeAndDrag. The + proposal stops at "real instance + dropped list on the wire" and + leans on the existing SAT renderer + PR #312 core display. Richer + rendering (themes, per-tuple violation badges, dedicated UI) is a + separate PR against the CnD repo. +- MaxSAT in the Pardinus/Kodkod backend. +- Suggesting *fixes* to the spec ("did you mean…"). The output is + "here's an instance, here's what we dropped." Inferring intent is a + separate research problem. +- Multi-instance counterfactual exploration ("show me three different + near-misses"). Worth doing, not v1. +- Relaxation over bounds. +- Per-tuple witness annotations (`violates="cN"` in the XML). Wire + format is forward-compatible with adding these later. From 5db29013a64b403fc3d44b897c772159f659243c Mon Sep 17 00:00:00 2001 From: Siddhartha Prasad Date: Fri, 22 May 2026 11:51:15 -0400 Subject: [PATCH 2/3] Counterfactual instances on UNSAT (initial implementation) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Implements the solver-side relaxation pass described in Notes/counterfactual-unsat.md. When a Forge run returns UNSAT and the new `counterfactual` option is `on`, the Pardinus backend now drops one core formula at a time, re-solves under a fresh run-name, and on success returns a RelaxedSat carrying both the satisfying instance and the list of dropped formulas. Files touched: * forge/sigs-structs.rkt - RelaxedSat substruct of Sat (so all existing consumers — modelToXML, lazy tree, is-sat? — treat it as a normal SAT instance and render through the existing SAT path). - New options: `counterfactual` ('on/'off, default 'off) and `counterfactual_budget` (non-negative integer, default 5). * forge/solver-specific/pardinus.rkt - send-to-kodkod refactored: the problem-emission logic moved into a local `emit-problem` helper that takes a dropped-ID set; the initial problem is emitted with no drops. - A `relax-context` closure (built only when the option is on) re-uses `emit-problem` to re-issue the whole problem under fresh run-names with the chosen assertions replaced by `true`. Returns 3 values now: (all-rels core-map relax-context). - get-next-kodkod-model takes relax-context as an extra argument and, on a fresh UNSAT with core, runs `run-relaxation-loop` — naive drop-and-retry, smallest top-level assertion first, deterministic. The loop bails out after `counterfactual_budget` iterations or when the core only references already-dropped assertions. - Once we've entered relaxation, subsequent "next instance" requests are routed to the relaxed run-name (kept in a box inside relax-context), so clicking "next" on a counterfactual doesn't silently drop the user back to UNSAT. * forge/send-to-solver.rkt - Typed contract widened: send-to-kodkod returns (Values Any Any Any); get-next-kodkod-model takes an extra Any. cvc5 backend unchanged. * forge/server/forgeserver.rkt - make-status-value: RelaxedSat? checked before Sat? so relaxed results report status "counterfactual" rather than "sat". - New `make-dropped-value` helper deparses the dropped-formulas list using the same machinery as `make-core-value` (shared `deparse-formula-entry`). - JSON envelope gains a `dropped` field alongside `core`. Older Sterling clients ignore unknown fields and fall back to the SAT rendering path (since `status` is unknown to them and the XML body *is* a real instance), which is the correct degradation. modelToXML.rkt needed no changes: because RelaxedSat is a Sat substruct, the existing cond chain in solution-to-XML-string already routes it through the SAT-instance generator. Smoke-tested four cases against MiniSatProver: - single-drop counterfactual (drops `no edges`, returns SAT instance) - multi-drop counterfactual (drops two assertions over two iterations) - normal SAT with counterfactual on (no relaxation triggered) - normal UNSAT with counterfactual off (regression: unchanged path) CnD / Sterling-side rendering of the new status and dropped field is out of scope for this commit and tracked as a follow-on against the CopeAndDrag repo. Co-Authored-By: Claude Opus 4.7 --- forge/send-to-solver.rkt | 21 +- forge/server/forgeserver.rkt | 43 ++- forge/sigs-structs.rkt | 33 ++- forge/solver-specific/pardinus.rkt | 414 +++++++++++++++++++++-------- 4 files changed, 389 insertions(+), 122 deletions(-) diff --git a/forge/send-to-solver.rkt b/forge/send-to-solver.rkt index 7c769c8e..50a3062f 100644 --- a/forge/send-to-solver.rkt +++ b/forge/send-to-solver.rkt @@ -36,14 +36,19 @@ [(start-server pardinus:start-server ) (-> Symbol Symbol (U False Path-String) (Values Output-Port Input-Port Input-Port (-> Void) (-> Boolean)))]) -; (send-to-kodkod run-name run-spec bitwidth all-atoms solverspec total-bounds bound-lower +; (send-to-kodkod run-name run-spec bitwidth all-atoms solverspec total-bounds bound-lower ; bound-upper run-constraints stdin stdout stderr)) -; Separate solver-specific translation for each solver backend +; Separate solver-specific translation for each solver backend. +; +; send-to-kodkod now returns (Values all-rels core-map relax-context). The +; relax-context is #f when the counterfactual option is off, and otherwise +; an opaque hash used by get-next-kodkod-model to re-issue the problem with +; assertions dropped. get-next-kodkod-model takes it as an extra argument. (require/typed forge/solver-specific/pardinus - [send-to-kodkod (-> Symbol Run-spec Integer (Listof FAtom) Any Any Any Any - (Listof node/formula) Output-Port Input-Port Input-Port - (Values Any Any))] - [get-next-kodkod-model (->* ((-> Boolean) Symbol Any (Listof FAtom) Any + [send-to-kodkod (-> Symbol Run-spec Integer (Listof FAtom) Any Any Any Any + (Listof node/formula) Output-Port Input-Port Input-Port + (Values Any Any Any))] + [get-next-kodkod-model (->* ((-> Boolean) Symbol Any (Listof FAtom) Any Any Output-Port Input-Port Input-Port) (String) (U Sat Unsat Unknown))]) @@ -328,9 +333,9 @@ #:run-command run-command)))] [(equal? backend 'pardinus) (begin - (define-values (all-rels core-map) + (define-values (all-rels core-map relax-context) (send-to-kodkod run-name run-spec bitwidth all-atoms solverspec total-bounds bound-lower bound-upper run-constraints stdin stdout stderr)) - (lambda ([mode : String]) (get-next-kodkod-model is-running? run-name all-rels all-atoms core-map stdin stdout stderr mode)))] + (lambda ([mode : String]) (get-next-kodkod-model is-running? run-name all-rels all-atoms core-map relax-context stdin stdout stderr mode)))] [else (raise-forge-error #:msg (format "Invalid backend: ~a" backend) #:context run-command)])) diff --git a/forge/server/forgeserver.rkt b/forge/server/forgeserver.rkt index 01c1e1c8..dbd3a185 100644 --- a/forge/server/forgeserver.rkt +++ b/forge/server/forgeserver.rkt @@ -222,20 +222,43 @@ (serve-sterling-static #:provider-port port #:static-port (get-option state-for-run 'sterling_static_port))]))) ; closes outer unless -(define (make-status-value inst) - (cond [(Sat? inst) "sat"] +(define (make-status-value inst) + ; Note: RelaxedSat is a substruct of Sat, so the RelaxedSat? check must + ; come *before* the Sat? check — otherwise relaxed results would be + ; reported as plain "sat" and the visualizer would have no signal that + ; we dropped constraints to produce them. + (cond [(RelaxedSat? inst) "counterfactual"] + [(Sat? inst) "sat"] [(Unsat? inst) "unsat"] [(Unknown? inst) "unknown"] [else "error"])) + +; Deparse a core/dropped entry — same shape for both fields. An entry is +; either an AST node (which we deparse to source) or a string Pardinus +; couldn't map back to user syntax (pass through verbatim). +(define (deparse-formula-entry cr) + (cond [(node? cr) (deparse cr)] + [(string? cr) cr] + [else (raise-forge-error + #:msg (format "Unexpected formula entry sending to Sterling: ~a" cr) + #:context #f)])) + (define (make-core-value inst) (if (and (Unsat? inst) (Unsat-core inst)) - (map (lambda (cr) (cond [(node? cr) (deparse cr)] - [(string? cr) cr] - [else (raise-forge-error #:msg (format "Unexpected core value sending to Sterling: ~a" cr) - #:context #f)])) - (Unsat-core inst)) + (map deparse-formula-entry (Unsat-core inst)) #f)) +; The list of formulas that were dropped from the unsat core during +; counterfactual relaxation. Only populated for RelaxedSat results; #f +; for plain Sat (no relaxation happened) and Unsat (relaxation didn't +; reach SAT, or wasn't enabled). Same wire shape as `core`, so the +; Sterling-side renderer can reuse whatever formatting it uses for the +; existing core display. +(define (make-dropped-value inst) + (cond [(RelaxedSat? inst) + (map deparse-formula-entry (RelaxedSat-dropped inst))] + [else #f])) + (define (make-sterling-data xml id run-name temporal? inst [old-id #f]) (define not-done? (Sat? inst)) (jsexpr->string @@ -250,6 +273,12 @@ 'data xml 'status (make-status-value inst) 'core (make-core-value inst) + ; New: list of formulas dropped by the + ; counterfactual relaxation, or #f when the + ; result wasn't a counterfactual. Older + ; Sterling clients that don't know about the + ; field will just ignore it. + 'dropped (make-dropped-value inst) 'buttons (cond [(not not-done?) (list)] [temporal? (list (hash 'text "Next Trace" diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt index 079547d4..e2344fc1 100644 --- a/forge/sigs-structs.rkt +++ b/forge/sigs-structs.rkt @@ -47,6 +47,24 @@ [metadata : Any] ; association list ) #:transparent) +; A counterfactual result: the *original* run was UNSAT, but after dropping +; one or more constraints from the unsat core we got a satisfying instance. +; Substruct of Sat so that all existing consumers (modelToXML, lazy tree, +; is-sat?, etc.) treat it as a normal SAT instance and render it through +; the existing SAT path. Only solver/visualizer code that wants to *report* +; the relaxation (status="counterfactual", dropped-formulas side panel) +; needs to dispatch on RelaxedSat? before Sat?. +(struct RelaxedSat Sat ( + ; The constraints that were suppressed to make the problem satisfiable. + ; Same shape as Unsat-core: each element is either a node (AST node, when + ; we mapped back to the user's formula) or a String (when we couldn't). + [dropped : (Listof (U node String))] + ; The original unsat core that triggered relaxation. Useful for the + ; visualizer to explain "this was the conflict; we resolved it by dropping + ; the formulas in 'dropped'". + [original-core : (Listof (U node String))] + ) #:transparent) + (struct Unsat ( ; If there's a core, there are two cases per component: ; (1) a node: a known formula @@ -270,7 +288,12 @@ 'engine_verbosity 1 'test_keep 'first 'no_overflow 'false - 'java_exe_location #f)) + 'java_exe_location #f + ; Counterfactual: when the run is UNSAT, drop core formulas and + ; re-solve, returning a near-instance instead of just UNSAT. + 'counterfactual 'off + ; Max number of formulas to drop before giving up and reporting UNSAT. + 'counterfactual_budget 5)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;; Constants ;;;;;;; @@ -320,7 +343,9 @@ 'engine_verbosity exact-nonnegative-integer? 'test_keep (oneof-pred '(first last)) 'no_overflow (oneof-pred '(false true)) - 'java_exe_location (lambda (x) (or (equal? x #f) (string? x))))) + 'java_exe_location (lambda (x) (or (equal? x #f) (string? x))) + 'counterfactual (oneof-pred '(on off)) + 'counterfactual_budget exact-nonnegative-integer?)) (define option-types-names (hash 'eval-language "symbol" @@ -342,7 +367,9 @@ 'engine_verbosity "non-negative integer" 'test_keep "one of: first or last" 'no_overflow "one of: false or true" - 'java_exe_location "string")) + 'java_exe_location "string" + 'counterfactual "one of: on or off" + 'counterfactual_budget "non-negative integer")) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/forge/solver-specific/pardinus.rkt b/forge/solver-specific/pardinus.rkt index 8e476b8b..7106d56c 100644 --- a/forge/solver-specific/pardinus.rkt +++ b/forge/solver-specific/pardinus.rkt @@ -13,9 +13,9 @@ print formula / assert formula (f0 ... fk) print solve |# - + ; (define-syntax-rule (kk-print lines ...) -; (kodkod:cmd +; (kodkod:cmd ; [stdin] ; lines ...)) @@ -30,7 +30,8 @@ (require (prefix-in @ (only-in racket/base >= not - = and or max > < +)) (only-in racket match first rest empty empty? set->list list->set set-intersect set-union curry range index-of pretty-print filter-map string-prefix? string-split thunk* - remove-duplicates subset? cartesian-product match-define cons? set-subtract) + remove-duplicates subset? cartesian-product match-define cons? set-subtract + findf third sort) racket/hash) (require forge/solver-specific/pardinus-cores) @@ -38,36 +39,10 @@ (provide send-to-kodkod get-next-kodkod-model) (define (send-to-kodkod run-name run-spec bitwidth all-atoms solverspec total-bounds bound-lower bound-upper run-constraints stdin stdout stderr) - + ; Print targets (define-syntax-rule (pardinus-print lines ...) - (pardinus:cmd [stdin] lines ...)) - - (pardinus-print (pardinus:print-cmd (format "(with ~a" run-name))) - (pardinus-print - (pardinus:configure (format ":bitwidth ~a :solver ~a :max-solutions 1 :verbosity ~a :skolem-depth ~a :sb ~a :core-gran ~a :core-minimization ~a :log-trans ~a :no-overflow ~a ~a ~a" - bitwidth - solverspec - (get-option run-spec 'engine_verbosity) ; see the Wiki for levels - (get-option run-spec 'skolem_depth) - (get-option run-spec 'sb) - (get-option run-spec 'coregranularity) - (get-option run-spec 'core_minimization) - (get-option run-spec 'logtranslation) - (get-option run-spec 'no_overflow) - (if (equal? 'temporal (get-option run-spec 'problem_type)) - (format ":min-trace-length ~a" (get-option run-spec 'min_tracelength)) - "") - (if (equal? 'temporal (get-option run-spec 'problem_type)) - (format ":max-trace-length ~a" (get-option run-spec 'max_tracelength)) - ""))) - (pardinus:declare-univ (length all-atoms))) - - ; Declare ints - (define num-ints (expt 2 bitwidth)) - (pardinus-print - (pardinus:declare-ints (range (@- (/ num-ints 2)) (/ num-ints 2)) ; ints - (range num-ints))) ; indexes + (pardinus:cmd [stdin] lines ...)) ; to-tupleset :: List>, int -> tupleset (define (to-tupleset arity eles) @@ -78,7 +53,7 @@ (pardinus:tupleset #:tuples eles))) (define (get-atoms rel atom-names) - (define atoms + (define atoms (for/list ([tup atom-names]) (for/list ([atom tup]) (unless (member atom all-atoms) @@ -90,67 +65,153 @@ (define ret (to-tupleset (relation-arity rel) atoms)) ret) - (for ([rel (get-all-rels run-spec)] - [bound total-bounds]) - (pardinus-print - (pardinus:declare-rel - (if (node/expr/relation-is-variable rel) - (pardinus:x (relation-name rel)) - (pardinus:r (relation-name rel))) - (get-atoms rel (bound-lower bound)) - (get-atoms rel (bound-upper bound))))) - - ; Declare assertions (define all-rels (get-all-rels run-spec)) - + ; Keep track of which formula corresponds to which CLI assert - ; for highlighting unsat cores. TODO: map back from CLI output - ; constraints later + ; for highlighting unsat cores and for counterfactual relaxation. + ; The mapping is the same across the original run and any relaxation + ; re-issues, since we keep assertion numbering stable. (define core-map (make-hash)) - (for ([p run-constraints] [assertion-number (in-naturals)]) - (hash-set! core-map assertion-number p) + (hash-set! core-map assertion-number p)) + + ; Emit a full (with ...) problem to the solver. If dropped-ids + ; contains an assertion-number, that assertion's body is replaced with + ; `true` (so Pardinus keeps the f:N identifier in scope but the formula + ; doesn't constrain anything). Used both for the initial problem and for + ; counterfactual relaxation re-issues, which need to drop a subset of + ; the original assertions and re-solve under a fresh run-name. + (define (emit-problem effective-run-name dropped-ids include-target?) + (pardinus-print (pardinus:print-cmd (format "(with ~a" effective-run-name))) (pardinus-print - (pardinus:print-cmd-cont "(~a " (pardinus:f assertion-number)) - (translate-to-kodkod-cli run-spec p all-rels all-atoms '()) - (pardinus:print-cmd ")") - (pardinus:assert (pardinus:f assertion-number)))) - - ; target-oriented model finding may not impose an initial target, but might - ; be used just to implement custom "next" strategies - (when (equal? 'target (get-option run-spec 'problem_type)) - (define target (Run-spec-target run-spec)) - (when target - (for ([(rel-name atoms) (Target-target target)]) - (define relation (hash-ref (get-relation-map run-spec) (symbol->string rel-name))) - (define sig-or-rel - (if (@= (relation-arity relation) 1) - (get-sig run-spec relation) - (get-relation run-spec relation))) - - (pardinus-print - (pardinus:declare-target - (pardinus:r (relation-name relation)) - (get-atoms relation atoms))))) - - ; Always say what mode; admittedly this won't always make sense if untargeted - ; Conflate "target distance" declared with a concrete target and global mode. - ; Note well: the space of possible options should mirror the contract on this field. + (pardinus:configure (format ":bitwidth ~a :solver ~a :max-solutions 1 :verbosity ~a :skolem-depth ~a :sb ~a :core-gran ~a :core-minimization ~a :log-trans ~a :no-overflow ~a ~a ~a" + bitwidth + solverspec + (get-option run-spec 'engine_verbosity) ; see the Wiki for levels + (get-option run-spec 'skolem_depth) + (get-option run-spec 'sb) + (get-option run-spec 'coregranularity) + (get-option run-spec 'core_minimization) + (get-option run-spec 'logtranslation) + (get-option run-spec 'no_overflow) + (if (equal? 'temporal (get-option run-spec 'problem_type)) + (format ":min-trace-length ~a" (get-option run-spec 'min_tracelength)) + "") + (if (equal? 'temporal (get-option run-spec 'problem_type)) + (format ":max-trace-length ~a" (get-option run-spec 'max_tracelength)) + ""))) + (pardinus:declare-univ (length all-atoms))) + + ; Declare ints + (define num-ints (expt 2 bitwidth)) (pardinus-print - (pardinus:print-cmd "(target-option target-mode ~a)" - (if target - (Target-distance target) - (get-option run-spec 'target_mode))))) + (pardinus:declare-ints (range (@- (/ num-ints 2)) (/ num-ints 2)) ; ints + (range num-ints))) ; indexes + + (for ([rel all-rels] + [bound total-bounds]) + (pardinus-print + (pardinus:declare-rel + (if (node/expr/relation-is-variable rel) + (pardinus:x (relation-name rel)) + (pardinus:r (relation-name rel))) + (get-atoms rel (bound-lower bound)) + (get-atoms rel (bound-upper bound))))) + + ; Emit assertion definitions and assertions. Drop a formula by emitting + ; `(f:N true)` in place of the real formula, keeping the identifier in + ; scope so any other references stay valid. + (for ([p run-constraints] + [assertion-number (in-naturals)]) + (cond + [(memv assertion-number dropped-ids) + (pardinus-print + (pardinus:print-cmd "(~a true)" (pardinus:f assertion-number)) + (pardinus:assert (pardinus:f assertion-number)))] + [else + (pardinus-print + (pardinus:print-cmd-cont "(~a " (pardinus:f assertion-number)) + (translate-to-kodkod-cli run-spec p all-rels all-atoms '()) + (pardinus:print-cmd ")") + (pardinus:assert (pardinus:f assertion-number)))])) + + ; target-oriented model finding: only attach the target to the *original* + ; run, not to relaxation re-issues. The relaxed problem inherits the + ; user's bounds and constraints (minus dropped) but is otherwise a + ; vanilla satisfiability problem. + (when (and include-target? + (equal? 'target (get-option run-spec 'problem_type))) + (define target (Run-spec-target run-spec)) + (when target + (for ([(rel-name atoms) (Target-target target)]) + (define relation (hash-ref (get-relation-map run-spec) (symbol->string rel-name))) + (define sig-or-rel + (if (@= (relation-arity relation) 1) + (get-sig run-spec relation) + (get-relation run-spec relation))) + + (pardinus-print + (pardinus:declare-target + (pardinus:r (relation-name relation)) + (get-atoms relation atoms))))) + + ; Always say what mode; admittedly this won't always make sense if untargeted + ; Conflate "target distance" declared with a concrete target and global mode. + ; Note well: the space of possible options should mirror the contract on this field. + (pardinus-print + (pardinus:print-cmd "(target-option target-mode ~a)" + (if target + (Target-distance target) + (get-option run-spec 'target_mode))))) + + ; Close the "with" scope. + (pardinus-print (pardinus:print-cmd ")")) + (pardinus-print (pardinus:print-eoi)) + ; Wait for the acknowledgement before sending more messages. + (pardinus:read-ack stdout stderr)) + + ; Emit the initial problem under the user's run-name. Dropped-ids is a + ; list (treated as a set, with at most `budget` entries); we use list ops + ; to avoid colliding with `set` already exported by forge/lang/ast. + (emit-problem run-name '() #t) - ; Close the "with" scope. - (pardinus-print (pardinus:print-cmd ")")) - (pardinus-print (pardinus:print-eoi)) - ; Wait for the acknowledgement before sending more messages. - (pardinus:read-ack stdout stderr) + ; Build the relaxation context. If counterfactual mode is off, this is + ; #f and `get-next-kodkod-model` short-circuits any UNSAT into the + ; normal UNSAT response. If on, it's a hash carrying: + ; 'reissue - a closure (set-of-int -> symbol) that re-emits the + ; whole problem with the given assertion-IDs replaced + ; by `true`, under a freshly-generated run-name, and + ; returns that new run-name. + ; 'budget - max relaxation iterations. + ; 'current-name - a box holding the most recently issued relax-name + ; (or #f if we haven't entered relaxation yet). Used + ; by `get-next-kodkod-model` to keep "next-instance" + ; requests pointed at the relaxed run after the first + ; counterfactual is produced. + (define relax-context + (cond + [(equal? 'on (get-option run-spec 'counterfactual)) + (define relax-counter (box 0)) + (define current-name-box (box #f)) + (define budget-opt (get-option run-spec 'counterfactual_budget)) + (define budget + (if (exact-nonnegative-integer? budget-opt) budget-opt 5)) + (define (reissue dropped-ids) + (set-box! relax-counter (add1 (unbox relax-counter))) + (define relax-name + (string->symbol (format "~a__cf~a" run-name (unbox relax-counter)))) + (emit-problem relax-name dropped-ids #f) + (set-box! current-name-box relax-name) + relax-name) + (hash 'reissue reissue + 'budget budget + 'current-name current-name-box)] + [else #f])) - ; Done with the problem spec. Return any needed shared data specific to this backend. - (values all-rels core-map)) + ; Done with the problem spec. Return shared data plus the relax context + ; (which is #f when counterfactual mode is off; callers must tolerate that). + (values all-rels core-map relax-context)) @@ -165,39 +226,184 @@ [tcstr (if tcx (format " Core min (ms): ~a" tcx) "")]) (format "#vars: ~a; #primary: ~a; #clauses: ~a~nTransl (ms): ~a; Solving (ms): ~a~a" vars prim clauses tt ts tcstr))) - + +; Pull the top-level assertion ID out of a raw Pardinus core entry. +; Pardinus emits entries shaped like "f:3" or "f:3,1,2" — where "3" is the +; top-level assertion (matches a key in core-map) and the comma-separated +; suffix descends into sub-formulas. For relaxation we need the top-level +; piece so we can drop the corresponding (assert f:N) in the next re-issue. +; Returns #f if the entry doesn't have the expected shape (which can +; happen for opaque cores Pardinus couldn't trace back; those entries +; just get skipped by the relaxation picker). +(define (top-level-assertion-id raw-core-entry) + (cond + [(string? raw-core-entry) + (cond + [(string-prefix? raw-core-entry "f:") + (define rest-str (substring raw-core-entry 2)) + (define head (first (string-split rest-str ","))) + (string->number head)] + [else #f])] + [else #f])) + +; Counterfactual relaxation loop. +; +; Preconditions: `initial-unsat` is an Unsat? value with kind 'unsat and a +; non-#f core; `relax-context` is a non-#f hash from send-to-kodkod. +; +; Strategy (naive drop-and-retry): each iteration, look at the *raw* core +; path-IDs Pardinus gave us, extract their top-level assertion IDs, pick +; the smallest one we haven't already dropped, add it to the dropped set, +; and ask `relax-context` to re-issue the problem under a fresh run-name +; with the dropped assertions replaced by `true`. Solve the new run; if +; SAT, wrap as RelaxedSat; if still UNSAT with a fresh core, loop. Bail +; out after `budget` iterations or when there are no new IDs to drop. +; +; Sorting top-level IDs ascending makes the relaxation deterministic — the +; same UNSAT spec always produces the same counterfactual (assuming the +; underlying Pardinus core itself is deterministic, which with +; `:core-minimization fast` it generally is). +(define (run-relaxation-loop initial-unsat initial-raw relax-context core-map all-rels all-atoms + stdin stdout stderr) + (define-syntax-rule (pardinus-print lines ...) + (pardinus:cmd [stdin] lines ...)) + + (define reissue (hash-ref relax-context 'reissue)) + (define budget (hash-ref relax-context 'budget)) + (define original-core (Unsat-core initial-unsat)) + + (let loop ([current-raw initial-raw] + [dropped-ids '()] + [dropped-formulas '()] + [iters 0]) + (cond + [(@>= iters budget) + ; Budget exhausted — return the original UNSAT untouched so the + ; user still sees the conflict report, just without a counterfactual. + (when (@>= (get-verbosity) VERBOSITY_LOW) + (printf "Counterfactual relaxation hit budget (~a) without reaching SAT.~n" budget)) + initial-unsat] + [else + ; current-raw is the raw read-solution result for the most recent + ; UNSAT. Shape: (list 'unsat run-name (list path-id ...) stats) + (define raw-core (third current-raw)) + (cond + [(or (not raw-core) (null? raw-core)) + ; No actionable core — nothing left to drop. + initial-unsat] + [else + ; Pick the smallest top-level ID we haven't already dropped. + (define candidate-ids + (sort (filter exact-nonnegative-integer? + (remove-duplicates (map top-level-assertion-id raw-core))) + @<)) + (define next-id + (findf (lambda (id) (@not (memv id dropped-ids))) candidate-ids)) + (cond + [(@not next-id) + ; Core only references assertions we've already dropped or + ; opaque entries we can't map back. Give up. + (when (@>= (get-verbosity) VERBOSITY_LOW) + (printf "Counterfactual relaxation could not pick a new constraint to drop; giving up after ~a iter(s).~n" iters)) + initial-unsat] + [else + (define new-dropped-ids (cons next-id dropped-ids)) + (define dropped-formula (hash-ref core-map next-id)) + (define new-dropped-formulas (cons dropped-formula dropped-formulas)) + (when (@>= (get-verbosity) VERBOSITY_LOW) + (printf "Counterfactual: dropping assertion ~a to relax (iter ~a/~a).~n" + next-id (add1 iters) budget)) + (define relax-name (reissue new-dropped-ids)) + (pardinus-print (pardinus:solve relax-name "")) + (define new-raw (pardinus:read-solution stdout stderr)) + (define new-result (translate-from-kodkod-cli + 'run new-raw all-rels all-atoms core-map)) + (cond + [(Sat? new-result) + ; Success — wrap as RelaxedSat. Reverse the list so callers + ; see drops in the order we made them. + (RelaxedSat (Sat-instances new-result) + (Sat-stats new-result) + (Sat-metadata new-result) + (reverse new-dropped-formulas) + original-core)] + [(and (Unsat? new-result) + (Unsat-core new-result) + (equal? (Unsat-kind new-result) 'unsat)) + ; Still UNSAT — keep relaxing using the *new* core, which + ; may surface assertions outside the original core. + (loop new-raw new-dropped-ids new-dropped-formulas (add1 iters))] + [else + ; UNSAT without a usable core, or some other state — bail. + initial-unsat])])])]))) + ; Print solve -(define (get-next-kodkod-model is-running? run-name all-rels all-atoms core-map stdin stdout stderr [mode ""]) +(define (get-next-kodkod-model is-running? run-name all-rels all-atoms core-map relax-context stdin stdout stderr [mode ""]) ; Print targets (define-syntax-rule (pardinus-print lines ...) - (pardinus:cmd [stdin] lines ...)) - + (pardinus:cmd [stdin] lines ...)) + ; If the solver process isn't running at all, error: (unless (is-running?) (raise-user-error "KodKod server is not running.")) ; If the solver is running, but this specific run ID is closed, user error (when (is-run-closed? run-name) (raise-user-error (format "Run ~a has been closed." run-name))) - - (pardinus-print (pardinus:solve run-name mode)) + + ; If we've already done one round of counterfactual relaxation in this + ; session, subsequent "next instance" requests should query the *relaxed* + ; run, not the original UNSAT one. Otherwise the user clicks "next" on + ; the counterfactual diagram and is silently dropped back to UNSAT. + (define already-relaxed-name + (and relax-context (unbox (hash-ref relax-context 'current-name)))) + (define effective-run-name (or already-relaxed-name run-name)) + + (pardinus-print (pardinus:solve effective-run-name mode)) + (define raw-solution (pardinus:read-solution stdout stderr)) (define result (translate-from-kodkod-cli - 'run - (pardinus:read-solution stdout stderr) - all-rels + 'run + raw-solution + all-rels all-atoms core-map)) - - (when (and (Unsat? result) (Unsat-core result)) ; if we have a core + + ; Counterfactual relaxation: only enter on a fresh UNSAT (not when the + ; relaxed run itself returns UNSAT — that just means "no more instances + ; of the counterfactual"). The 'unsat kind check excludes 'no-counterexample + ; and 'no-more-instances, which are not "the problem contradicts itself" + ; conditions and have no useful relaxation semantics. + (define final-result + (cond + [(and relax-context + (@not already-relaxed-name) + (Unsat? result) + (Unsat-core result) + (equal? (Unsat-kind result) 'unsat)) + (run-relaxation-loop result raw-solution relax-context core-map all-rels all-atoms + stdin stdout stderr)] + [else result])) + + (when (and (Unsat? final-result) (Unsat-core final-result)) ; if we have a core (when (@>= (get-verbosity) VERBOSITY_DEBUG) (printf "core-map: ~a~n" core-map) - (printf "core: ~a~n" (Unsat-core result))) - (when (@>= (get-verbosity) VERBOSITY_LOW) - (printf "Unsat core available (~a formulas):~n" (length (Unsat-core result)))) - (for ([id (Unsat-core result)] - [idx (range (length (Unsat-core result)))]) - (pretty-print-core-formula idx (length (Unsat-core result)) id core-map))) - + (printf "core: ~a~n" (Unsat-core final-result))) + (when (@>= (get-verbosity) VERBOSITY_LOW) + (printf "Unsat core available (~a formulas):~n" (length (Unsat-core final-result)))) + (for ([id (Unsat-core final-result)] + [idx (range (length (Unsat-core final-result)))]) + (pretty-print-core-formula idx (length (Unsat-core final-result)) id core-map))) + + ; Briefly summarize a counterfactual result so it's visible in the + ; console alongside the existing core display for plain UNSAT. + (when (and (RelaxedSat? final-result) (@>= (get-verbosity) VERBOSITY_LOW)) + (define dropped (RelaxedSat-dropped final-result)) + (printf "Counterfactual instance found by dropping ~a constraint(s):~n" + (length dropped)) + (for ([fmla dropped] + [idx (range (length dropped))]) + (pretty-print-core-formula idx (length dropped) fmla core-map))) + (when (@>= (get-verbosity) VERBOSITY_LOW) - (displayln (format-statistics (if (Sat? result) (Sat-stats result) (Unsat-stats result))))) - result) \ No newline at end of file + (displayln (format-statistics (if (Sat? final-result) (Sat-stats final-result) (Unsat-stats final-result))))) + final-result) From 915db5f2777103e42a391360d8e9114a66e5f181 Mon Sep 17 00:00:00 2001 From: Siddhartha Prasad Date: Fri, 22 May 2026 12:27:30 -0400 Subject: [PATCH 3/3] Relation-level witness flagging for dropped counterfactual formulas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit For each formula dropped during counterfactual relaxation, walk its AST to collect the sigs and fields it references, then annotate every tuple of those relations in the relaxed instance with `violates_cN`="true" (where N indexes the dropped formula). The annotations ride on the existing tuple-annotations channel in modelToXML, so they surface in the per-tuple XML attributes the visualizer already consumes. This is the Amalgam-flavored half of the proposal — coarse, not full per-tuple provenance. We say "look here: these relations are involved in the dropped constraint," not "this specific tuple is the unsatisfying witness." Full witness extraction would need an evaluator pass per dropped formula (probably another commit cycle); this gives the visualizer enough signal to direct user attention without that plumbing. New module forge/server/counterfactual-witness.rkt provides: - collect-referenced-relations: AST walker pulling every node/expr/relation reachable from a formula or expression. Handles every node type Forge currently constructs (op-on-exprs, comprehensions, quantified formulas, multiplicity, ite, pred/fun spacers, int expressions, ...). Opaque entries (string fallbacks from Pardinus, sealed formulas) contribute no relations. - build-witness-tuple-annotations: turns (dropped-formulas, instance) into the nested hash shape modelToXML's tuple-annotations expects. Tuples in multiple dropped formulas' relations accumulate multiple violates_cN annotations. forge/server/forgeserver.rkt: both get-xml definitions (display-model and start-sterling-menu) now populate tuple-annotations from RelaxedSat results before handing them to solution-to-XML-string. Non-RelaxedSat results get the empty hash, same as before. Unit-tested with a direct test (a hand-built `no edges` formula against a fake instance) — walker finds `edges`, both edges tuples get violates_c0=true. End-to-end smoke tests still pass. Co-Authored-By: Claude Opus 4.7 --- forge/server/counterfactual-witness.rkt | 143 ++++++++++++++++++++++++ forge/server/forgeserver.rkt | 29 ++++- 2 files changed, 167 insertions(+), 5 deletions(-) create mode 100644 forge/server/counterfactual-witness.rkt diff --git a/forge/server/counterfactual-witness.rkt b/forge/server/counterfactual-witness.rkt new file mode 100644 index 00000000..9c2a9506 --- /dev/null +++ b/forge/server/counterfactual-witness.rkt @@ -0,0 +1,143 @@ +#lang racket/base + +; Witness attribution for counterfactual UNSAT relaxation. +; +; When the solver returns a RelaxedSat (a SAT instance produced by dropping +; one or more core formulas), the dropped formulas are by definition false +; in the resulting instance. To help the visualizer point at *what made +; them false*, we walk each dropped formula's AST, collect the sigs/fields +; it references, and tag every tuple of those relations in the instance +; with a `violates_cN`="true" XML attribute. The N indexes into the +; RelaxedSat-dropped list, so the visualizer can correlate a flagged tuple +; with the specific dropped constraint. +; +; This is intentionally coarse: it doesn't say "this specific tuple is the +; one that violates phi" (that would be full Amalgam-style provenance, +; which needs an evaluator pass per dropped formula). It says "these +; relations are involved in the violation; look here." For most pedagogical +; specs this is enough signal to direct attention. +; +; Anything Pardinus couldn't map back to an AST node (entries that come +; through as strings in Unsat-core / RelaxedSat-dropped) gets no flagging +; — we have no AST to walk. + +(require forge/lang/ast + (only-in racket/list second remove-duplicates)) + +(provide collect-referenced-relations + build-witness-tuple-annotations) + +; Walk the AST rooted at `root`, gathering every node/expr/relation that +; appears anywhere in the formula or its sub-expressions. Quantifier +; variables, atoms, and constants are leaves with no relations. Decl +; domains are visited (so `all n: Node | ...` correctly attributes `Node`). +(define (collect-referenced-relations root) + (define result '()) + (define (push! r) (set! result (cons r result))) + + (define (visit-decl-domain decl) + ; A decl is `(var domain)` or `(var . domain)` depending on shape; + ; mirror the same robustness as sigs-structs.rkt's `second/safe`. + (cond [(list? decl) (when (>= (length decl) 2) (visit (second decl)))] + [(pair? decl) (visit (cdr decl))])) + + (define (visit n) + (cond + ; Hit: a relation (sig or field). + [(node/expr/relation? n) (push! n)] + + ; Expressions with explicit child lists. + [(node/expr/op-on-exprs? n) + (for-each visit (node/expr/op-on-exprs-children n))] + [(node/expr/op-on-ints? n) + (for-each visit (node/expr/op-on-ints-children n))] + + ; If-then-else expression. + [(node/expr/ite? n) + (visit (node/expr/ite-condition n)) + (visit (node/expr/ite-thene n)) + (visit (node/expr/ite-elsee n))] + + ; Comprehension `{ x: D | phi }`. + [(node/expr/comprehension? n) + (for-each visit-decl-domain (node/expr/comprehension-decls n)) + (visit (node/expr/comprehension-formula n))] + + ; Function call expanded form. + [(node/expr/fun-spacer? n) + (visit (node/expr/fun-spacer-expanded n))] + + ; Integer expressions with children. + [(node/int/op-on-ints? n) + (for-each visit (node/int/op-on-ints-children n))] + [(node/int/op-on-exprs? n) + (for-each visit (node/int/op-on-exprs-children n))] + [(node/int/sum-quant? n) + (for-each visit-decl-domain (node/int/sum-quant-decls n)) + (visit (node/int/sum-quant-int-expr n))] + + ; Formula operators. + [(node/formula/op-on-formulas? n) + (for-each visit (node/formula/op-on-formulas-children n))] + [(node/formula/op-on-exprs? n) + (for-each visit (node/formula/op-on-exprs-children n))] + [(node/formula/op-on-ints? n) + (for-each visit (node/formula/op-on-ints-children n))] + + ; Quantified formulas `all x: D | phi`, `some x: D | phi`, etc. + [(node/formula/quantified? n) + (for-each visit-decl-domain (node/formula/quantified-decls n)) + (visit (node/formula/quantified-formula n))] + + ; Multiplicity formulas (`some e`, `no e`, `lone e`, ...). + [(node/formula/multiplicity? n) + (visit (node/formula/multiplicity-expr n))] + + ; Predicate call expanded form. + [(node/fmla/pred-spacer? n) + (visit (node/fmla/pred-spacer-expanded n))] + + ; Everything else (quantifier vars, atoms, constants, sealed + ; formulas we can't introspect) contributes no relations. + [else (void)])) + + (visit root) + (remove-duplicates result)) + +; Build a tuple-annotations hash suitable for modelToXML's +; `#:tuple-annotations` keyword arg. +; +; dropped-formulas: List<(U node String)> — typically (RelaxedSat-dropped soln) +; instance-by-symbol: HashTable> — typically +; (first (Sat-instances soln)), keyed by the engine's symbol names +; (e.g., 'edges, 'Node). +; +; Returns: HashTable>> +; where each tuple of a relation referenced by dropped-formula i gets +; the annotation `violates_cI` = `true`. +; +; A tuple in a relation that appears in multiple dropped formulas gets +; multiple violates_cN annotations — they accumulate via cons. +(define (build-witness-tuple-annotations dropped-formulas instance-by-symbol) + (define result (make-hash)) + + (for ([dropped (in-list dropped-formulas)] + [idx (in-naturals)]) + (define annotation-pair + (cons (string->symbol (format "violates_c~a" idx)) 'true)) + (define relations + (cond [(node? dropped) (collect-referenced-relations dropped)] + [else '()])) ; opaque string entries: skip + + (for ([rel (in-list relations)]) + (define rel-sym (string->symbol (relation-name rel))) + (when (hash-has-key? instance-by-symbol rel-sym) + (define rel-tuples (hash-ref instance-by-symbol rel-sym)) + (unless (hash-has-key? result rel) + (hash-set! result rel (make-hash))) + (define per-tuple (hash-ref result rel)) + (for ([tup (in-list rel-tuples)]) + (define existing (hash-ref per-tuple tup '())) + (hash-set! per-tuple tup (cons annotation-pair existing)))))) + + result) diff --git a/forge/server/forgeserver.rkt b/forge/server/forgeserver.rkt index dbd3a185..7931d9ce 100644 --- a/forge/server/forgeserver.rkt +++ b/forge/server/forgeserver.rkt @@ -16,6 +16,7 @@ (require (only-in forge/lang/ast relation-name raise-forge-error deparse node?) forge/server/modelToXML + forge/server/counterfactual-witness forge/evaluator xml net/sendurl "../racket-rfc6455/net/rfc6455.rkt" net/url web-server/http/request-structs racket/runtime-path @@ -123,12 +124,22 @@ (define command-string (format "~a" (syntax->datum command))) - (define (get-xml soln) + (define (get-xml soln) ;(define tuple-annotations (if (and (Sat? model) (equal? 'on (get-option the-run 'local_necessity))) ; (build-tuple-annotations-for-ln model) ; (hash))) ; TODO: disable LN for winter '21 dev - (define tuple-annotations (hash)) + ; For counterfactual results, flag every tuple of any relation + ; referenced by a dropped formula with `violates_cN`="true". This + ; gives CnD/Sterling enough signal to highlight "look here" without + ; needing per-tuple provenance. + (define tuple-annotations + (cond + [(and (RelaxedSat? soln) (not (empty? (Sat-instances soln)))) + (build-witness-tuple-annotations + (RelaxedSat-dropped soln) + (first (Sat-instances soln)))] + [else (hash)])) (when (@>= (get-verbosity) VERBOSITY_STERLING) (printf "tuple annotations were: ~a~n" tuple-annotations)) (solution-to-XML-string soln relation-map name command-string filepath @@ -450,9 +461,17 @@ ; The bitwidth for this run. (define bitwidth (get-bitwidth (Run-run-spec the-run))) - ; Helper to convert a solution to Alloy-format instance XML - (define (get-xml soln) - (define tuple-annotations (hash)) ; no annotations at the moment + ; Helper to convert a solution to Alloy-format instance XML. + ; Same counterfactual witness flagging as the display-model path: + ; tag tuples of relations referenced by each dropped formula. + (define (get-xml soln) + (define tuple-annotations + (cond + [(and (RelaxedSat? soln) (not (empty? (Sat-instances soln)))) + (build-witness-tuple-annotations + (RelaxedSat-dropped soln) + (first (Sat-instances soln)))] + [else (hash)])) (solution-to-XML-string soln (get-relation-map the-run) name command-string filepath bitwidth forge-version #:tuple-annotations tuple-annotations