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. 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/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 01c1e1c8..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 @@ -222,20 +233,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 +284,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" @@ -421,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 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)