Feature support matrix
An honest table of what Logic Studio does, what it partially does, and what it does not do.
Last reviewed: 2026-05-25. Reflects shipped state of logic.solves.ca at that date. Roadmap items (✨) are documented under docs/ but not yet shipping.
This matrix is built from the source code, not from aspirations. Status legends:
- ✅ Full — implemented and tested
- ⚠️ Partial — works with caveats; see Notes
- ❌ Not supported — not implemented
- ✨ Roadmap — documented under
docs/; not yet shipping
Expression language
| Feature | Status | Notes |
|---|
| Boolean variables | ✅ Full | Case-sensitive identifiers |
| Boolean literals (true/false/0/1) | ✅ Full | |
| NOT, AND, OR, XOR | ✅ Full | Symbol and keyword forms (!, &, |, ^) |
| Implication (→) | ✅ Full | -> syntax |
| Biconditional (↔) | ✅ Full | <-> syntax |
| Named bindings | ✅ Full | Semicolon-terminated; forward references not supported |
| Don't-cares | ✅ Full | B? suffix or via Inputs panel |
| Predicate comparisons (<, <=, >, >=, ==, !=) | ✅ Full | Numeric scalars on the right-hand side only |
| Set membership (in, not-in) | ✅ Full | Literal value sets: in {CA, US} |
| Cross-variable arithmetic (a + b > c) | ❌ Not supported | Each predicate must involve exactly one typed variable |
| String predicates | ⚠️ Partial | Parsed; no runtime evaluation beyond equality/set membership |
| Comments | ✅ Full | Line comments // and #, plus block comments /* … */. Block comments do not nest; unterminated blocks raise a lex error. |
Analysis panels
| Feature | Status | Notes |
|---|
| Syntax-highlighted editor | ✅ Full | Variable colour cycling, operator colouring, error underlines |
| Live parse errors | ✅ Full | Red border + error message below editor |
| Flow graph (single binding) | ✅ Full | React Flow DAG, Dagre layout |
| Flow graph (Show-all DAG) | ✅ Full | All bindings in one graph; shared sub-expressions shared |
| Truth table | ✅ Full | Up to 2n rows; truncates for large n |
| Decision table | ✅ Full | Compact rules view; supports collapse of identical rows |
| Simplification (QM + Petrick) | ✅ Full | Minimum two-level SOP |
| Simplification Why? trace | ✅ Full | Step-by-step QM reasoning in prose form |
| Rewrite transforms (CNF, DNF, NNF, De Morgan, Factor) | ✅ Full | One-click; before/after preview |
| Pseudocode rendering | ✅ Full | Always-on if/else pseudocode block in Rewrite panel |
| Coverage — Branch | ✅ Full | |
| Coverage — MC/DC | ✅ Full | Each condition independently affects the decision |
| Coverage — Pairwise | ✅ Full | |
| Coverage — Prime Implicant | ✅ Full | Based on QM prime implicants |
| Karnaugh map renderer | ✅ Full | Gray-coded grid for 2–6 variables (2×2, 2×4, 4×4, 4×8, 8×8). Cells show 0/1/don't-care; tooltips show the full per-cell assignment. Outside 2–6 variables the panel directs users to the truth table / Simplify. |
| Equivalence diff | ✅ Full | Checks two expressions for logical equivalence; returns counterexample on mismatch |
| Notebook (save/load expressions) | ✅ Full | IndexedDB; browser-local only; not synced |
| Variable impact chart | ✅ Full | Shows fraction of assignments where each variable is decisive |
| Notebook empty state | ✅ Full | Oriented first-time card explains what saved entries are, how to import, and that storage is browser-local |
| Coverage strategy disclosures | ✅ Full | Each coverage mode (branch, MC/DC, pairwise, prime-implicant, full truth-table) carries an (i) disclosure with the underlying concept; gated by the teaching toggle (default ON) |
| Equivalence Diff default render | ✅ Full | Side A pre-seeds with the working expression, Side B pre-seeds with the simplified form; the panel opens in the populated/compared state when both exist |
| Equivalence Diff backend routing | ✅ Full | Auto-picks QM enumeration (≤14 bool vars), SAT (>14 bool vars), or SMT/Z3 (predicate atoms). Shown in the result's “Why this backend?” note. |
| Equivalence Diff truth-table diff | ⚠️ Partial | Full row-by-row diff only on the QM enumeration path. SAT/SMT paths return verdict + a single counterexample (the truth-table is too large or not pure-boolean). |
Predicates
| Feature | Status | Notes |
|---|
| Numeric buckets (truth table rows per range) | ✅ Full | Splits real line at boundary values from predicates |
| Enum buckets | ✅ Full | One bucket per declared enum value |
| Contradiction detection | ✅ Full | Within a single variable; e.g. age < 18 AND age >= 18 |
| Subsumption detection | ✅ Full | Within a single variable |
| Cross-variable predicate reasoning | ⚠️ Partial | Only via Z3 SMT; the QM simplifier treats all predicates as opaque atoms |
| Type editor UI (set type / range / enum values) | ✅ Full | Click + next to a predicate variable. Type metadata persists to localStorage and rides shared URLs (v2 schema). |
Solver
| Feature | Status | Notes |
|---|
| SAT solving (pure boolean) | ✅ Full | logic-solver backend; fast, no download |
| SMT solving (Z3 WASM) | ✅ Full | Loads lazily; requires SharedArrayBuffer (COOP/COEP headers) |
| Tautology / contradiction detection | ✅ Full | Both backends |
| Multi-solution enumeration | ✅ Full | Bounded by both count (1–1024, default 16) and wall-clock time budget (100–30000 ms, default 2000). Returns the reason it stopped: exhausted, limit, timeout, or free. Available in the Solver panel when the active backend is SAT or SMT. |
| Optimisation (MaxSAT / MaxSMT) | ✨ Roadmap | Not shipping. Plan and open syntax questions in docs/OPTIMISATION-ROADMAP.md. Z3 Optimize is available in the WASM build; phase-1 will wrap it with soft-clause sugar after the ?-vs-don't-care token collision is decided. |
| Quantifier reasoning (∀, ∃) | ✨ Roadmap | Not shipping. Plan in docs/QUANTIFIERS-ROADMAP.md. Phase-1 expands quantifiers over finite enums and small integer ranges into and/or at parse time; phase-2 builds Z3 ForAll/Exists directly. Today the existing tautology / contradiction / satisfiability checks already answer the propositional ∀/∃ questions. |
| Custom Z3 theories | ❌ Not supported | Only the theories exposed by the predicate UI are used |
Export / import
| Feature | Status | Notes |
|---|
| Export to JavaScript | ✅ Full | |
| Export to Python | ✅ Full | |
| Export to C | ✅ Full | |
| Export to SQL (WHERE clause) | ✅ Full | |
| Export to GitHub Actions condition | ✅ Full | |
| Export to Lisp S-expression | ✅ Full | |
| Import from JavaScript / Python | ⚠️ Partial | Best-effort; complex expressions may not parse |
| Import from SQL / GHA | ⚠️ Partial | Best-effort |
| PNG graph export | ✅ Full | html-to-image; screen resolution |
| SVG graph export | ✅ Full | Vector; embeds theme colours |
| Coverage test vectors (JS/Python/C/SQL) | ✅ Full | |
Persistence & sharing
| Feature | Status | Notes |
|---|
| URL-encoded sharing | ✅ Full | Expression source encoded in URL hash; self-contained |
| Server-side persistence | ❌ Not supported | Everything is client-local. No accounts, no server storage. |
| Notebook (IndexedDB) | ✅ Full | Survives page reload; lost when browser data is cleared |
| Variable type annotations in share URL | ✅ Full | Share schema v2 carries {src, names?, types?} where each typed variable round-trips its type, display name, domain (min/max), and enum values. v1 URLs continue to decode. |
| Display name customisations in share URL | ✅ Full | Carried via the names field of the share schema (both v1 and v2). |
UI & UX
| Feature | Status | Notes |
|---|
| Dark theme | ✅ Full | Default; "Schematic Slate" palette |
| Light theme | ✅ Full | "Schematic Paper" palette |
| System theme (prefers-color-scheme) | ✅ Full | Respects OS preference unless overridden |
Teaching mode ((i) disclosures) | ✅ Full | Header toggle (default ON). When on, info chips next to each surface vocabulary term reveal a short concept page. Persists to localStorage. |
| Basic / Advanced UI mode | ✅ Full | Header toggle. Basic (default) hides specialised vocabulary (CNF/DNF labels, prime implicant phrasing, quantifier symbols) in favour of plain-English alternatives. Components opt in via .ls-jargon and .ls-plain spans. Persists to localStorage. |
| ⌘K command palette | ✅ Full | Filterable command search + shortcut help |
| Keyboard shortcuts | ✅ Full | See Editor → Shortcuts |
| Mobile / narrow layout | ✅ Full | Hybrid layout shell: shared Zustand store with separate DesktopLayout / MobileLayout components. Breakpoints <720 mobile, 720–1024 tablet, >1024 desktop. Graph interaction is still pan/zoom-only on touch. |
| Z3 lazy-load progress UI | ✅ Full | Solver status pill with subtle progress bar; does not push page layout. Prefetch gated behind explicit need (Phase 2.2). |
| Accessibility (WCAG AA contrast) | ⚠️ Partial | Both themes target AA contrast; not fully audited for all interactive components |
| Screen reader support | ⚠️ Partial | ARIA roles and labels on major regions; graph nodes are not accessible to screen readers |
| Offline use | ⚠️ Partial | Service worker is registered (Workbox + vite-plugin-pwa); app shell, static assets, and the editor work offline after first load. Z3 WASM (~33 MB) is only fetched when SMT solving is invoked and is not prefetched. Cloudflare CDN helps with repeat visits. |
| Install as PWA | ✅ Full | Manifest + service worker; InstallAppButton surfaces a prompt where the browser supports it (Chromium, Edge, Android Chrome). Safari requires Add-to-Home-Screen from share sheet. |
Known gaps summary
- No server-side sharing or collaboration — everything is URL-encoded or browser-local
- QM simplifier treats predicate atoms as opaque booleans — it can't use numeric/set semantics directly; use Z3/SMT routing for that
- Import is best-effort; complex or idiomatic code in the source language may not parse
- Graph nodes are not screen-reader accessible (they're React Flow canvas elements)
- Equivalence Diff truth-table view requires ≤14 pure-boolean variables (SAT/SMT paths show verdict + counterexample only)
- Z3 WASM (~33 MB) is not bundled into the service-worker pre-cache, so SMT is unavailable on a cold network drop
- Cross-variable predicate arithmetic (
a + b > c) is not parsed; each predicate must involve one typed variable
- Real-device iOS/Android polish pass is pending hardware; Safari WebKit Playwright on Linux is blocked on
libgtk-4
- Roadmap items not yet shipping: Optimisation / MaxSAT (
docs/OPTIMISATION-ROADMAP.md), Quantifiers ∀/∃ (docs/QUANTIFIERS-ROADMAP.md)