/* ============================================================
   BTOR2 Visualizer — design system
   Dark "deep ink" theme · glass panels · cyan→violet accent
   ============================================================ */

*, *::before, *::after { box-sizing: border-box; margin: 0; padding: 0; }

:root {
    /* surfaces */
    --bg-primary: #0b0d14;
    --bg-secondary: #10131d;
    --bg-panel: #131724;
    --bg-card: #171c2c;
    --bg-hover: #1f2538;
    --bg-input: #0d101a;

    /* strokes */
    --border: #232940;
    --border-strong: #2f3754;
    --border-glow: rgba(96, 165, 250, 0.35);

    /* text */
    --text: #dde3f0;
    --text-soft: #aab3c8;
    --text-muted: #6b7490;

    /* accent system: cyan -> violet */
    --accent: #60a5fa;
    --accent-2: #8b7cf6;
    --accent-dim: #3b6fd4;
    --accent-grad: linear-gradient(135deg, #38bdf8 0%, #60a5fa 45%, #8b7cf6 100%);
    --accent-soft: rgba(96, 165, 250, 0.12);

    /* category colors */
    --bad-color: #f87171;
    --state-color: #4ade80;
    --constraint-color: #facc15;
    --memory-color: #fbbf24;
    --input-color: #7dd3fc;
    --constant-color: #93c5fd;
    --logic-color: #94a3b8;
    --clump-color: #c4b5fd;

    /* type */
    --font-mono: 'JetBrains Mono', 'Cascadia Code', 'Consolas', monospace;
    --font-sans: 'Inter', system-ui, -apple-system, 'Segoe UI', sans-serif;

    /* geometry */
    --radius: 10px;
    --radius-sm: 7px;
    --radius-xs: 5px;

    /* elevation */
    --shadow-1: 0 1px 2px rgba(0,0,0,.4), 0 2px 8px rgba(0,0,0,.25);
    --shadow-2: 0 4px 14px rgba(0,0,0,.45), 0 1px 3px rgba(0,0,0,.3);
    --shadow-glow: 0 0 0 1px var(--border-glow), 0 4px 18px rgba(56,189,248,.12);
}

html, body {
    height: 100%;
    font-family: var(--font-sans);
    font-size: 13px;
    color: var(--text);
    background:
        radial-gradient(1200px 700px at 75% -10%, rgba(139,124,246,.07), transparent 60%),
        radial-gradient(900px 600px at -10% 110%, rgba(56,189,248,.06), transparent 55%),
        var(--bg-primary);
    overflow: hidden;
    -webkit-font-smoothing: antialiased;
}

::selection { background: rgba(96,165,250,.35); }

/* thin elegant scrollbars */
::-webkit-scrollbar { width: 8px; height: 8px; }
::-webkit-scrollbar-track { background: transparent; }
::-webkit-scrollbar-thumb {
    background: var(--border-strong);
    border-radius: 8px;
    border: 2px solid transparent;
    background-clip: content-box;
}
::-webkit-scrollbar-thumb:hover { background: #3d4666; background-clip: content-box; }

/* ============ Layout ============ */
.app {
    display: grid;
    grid-template-columns: 272px 1fr 312px;
    grid-template-rows: auto 1fr auto;
    height: 100vh;
}

/* ============ Header ============ */
.header {
    grid-column: 1 / -1;
    display: flex;
    align-items: center;
    justify-content: space-between;
    padding: 10px 18px;
    background: linear-gradient(180deg, rgba(23,28,44,.9), rgba(16,19,29,.95));
    border-bottom: 1px solid var(--border);
    backdrop-filter: blur(8px);
}

.header h1 {
    font-size: 15px;
    font-weight: 800;
    letter-spacing: -0.2px;
    font-family: var(--font-mono);
    background: var(--accent-grad);
    -webkit-background-clip: text;
    background-clip: text;
    color: transparent;
    display: inline-flex;
    align-items: center;
    gap: 9px;
}

.logo-mark {
    width: 22px; height: 22px;
    border-radius: 7px;
    background: var(--accent-grad);
    box-shadow: 0 0 14px rgba(96,165,250,.5);
    display: inline-block;
    flex-shrink: 0;
}

.subtitle {
    font-size: 11.5px;
    color: var(--text-muted);
    margin-left: 12px;
    letter-spacing: .1px;
}

.header-actions { display: flex; gap: 8px; align-items: center; }
.header-link {
    font-size: 11.5px;
    color: var(--text-muted);
    text-decoration: none;
    padding: 5px 10px;
    border-radius: var(--radius-sm);
    transition: all .15s;
}
.header-link:hover { color: var(--accent); background: var(--accent-soft); }

/* ============ Panels ============ */
.left-panel, .right-panel {
    background: var(--bg-secondary);
    overflow-y: auto;
    display: flex;
    flex-direction: column;
    min-height: 0;
}
.left-panel  { border-right: 1px solid var(--border); }
.right-panel { border-left: 1px solid var(--border); }

.panel-section {
    padding: 14px 14px 12px;
    border-bottom: 1px solid var(--border);
}

.panel-section h3, .trace-panel h3 {
    font-size: 10.5px;
    text-transform: uppercase;
    letter-spacing: 1.2px;
    color: var(--text-muted);
    margin-bottom: 10px;
    display: flex;
    align-items: center;
    gap: 7px;
}

.panel-section h3::before, .trace-panel h3::before {
    content: "";
    width: 3px; height: 11px;
    border-radius: 2px;
    background: var(--accent-grad);
    display: inline-block;
}

/* ============ Buttons ============ */
.btn {
    font-family: var(--font-sans);
    font-size: 12px;
    font-weight: 600;
    color: var(--text-soft);
    background: var(--bg-card);
    border: 1px solid var(--border-strong);
    border-radius: var(--radius-sm);
    padding: 6px 11px;
    cursor: pointer;
    transition: all .16s cubic-bezier(.4,0,.2,1);
    user-select: none;
}

.btn:hover {
    color: var(--text);
    background: var(--bg-hover);
    border-color: var(--accent-dim);
    transform: translateY(-1px);
    box-shadow: var(--shadow-1);
}
.btn:active { transform: translateY(0); box-shadow: none; }
.btn:focus-visible { outline: 2px solid var(--accent); outline-offset: 1px; }

.btn-primary {
    background: var(--accent-grad);
    color: #0b1020;
    border: none;
    box-shadow: 0 2px 10px rgba(96,165,250,.35);
}
.btn-primary:hover {
    filter: brightness(1.1);
    color: #0b1020;
    box-shadow: 0 4px 16px rgba(96,165,250,.5);
}

.btn-small { font-size: 11px; padding: 4px 9px; }

.btn-group { display: flex; gap: 6px; flex-wrap: wrap; }

input[type="file"] { display: none; }

/* ============ Inputs ============ */
input[type="text"], textarea, select {
    font-family: var(--font-mono);
    font-size: 12px;
    color: var(--text);
    background: var(--bg-input);
    border: 1px solid var(--border-strong);
    border-radius: var(--radius-sm);
    padding: 7px 10px;
    width: 100%;
    transition: border-color .15s, box-shadow .15s;
}
input[type="text"]:focus, textarea:focus, select:focus {
    outline: none;
    border-color: var(--accent-dim);
    box-shadow: 0 0 0 3px var(--accent-soft);
}
input[type="text"]::placeholder, textarea::placeholder { color: var(--text-muted); }

select { appearance: none; cursor: pointer;
    background-image: linear-gradient(45deg, transparent 50%, var(--text-muted) 50%),
                      linear-gradient(135deg, var(--text-muted) 50%, transparent 50%);
    background-position: calc(100% - 16px) 55%, calc(100% - 11px) 55%;
    background-size: 5px 5px;
    background-repeat: no-repeat;
    padding-right: 28px;
}

/* range sliders */
input[type="range"] {
    -webkit-appearance: none;
    appearance: none;
    width: 100%;
    height: 4px;
    border-radius: 4px;
    background: var(--border-strong);
    cursor: pointer;
    border: none;
    padding: 0;
}
input[type="range"]::-webkit-slider-thumb {
    -webkit-appearance: none;
    width: 14px; height: 14px;
    border-radius: 50%;
    background: var(--accent);
    border: 2px solid #0b1020;
    box-shadow: 0 0 8px rgba(96,165,250,.5);
    transition: transform .12s;
}
input[type="range"]::-webkit-slider-thumb:hover { transform: scale(1.2); }
input[type="range"]::-moz-range-thumb {
    width: 12px; height: 12px;
    border-radius: 50%;
    background: var(--accent);
    border: 2px solid #0b1020;
    box-shadow: 0 0 8px rgba(96,165,250,.5);
}

/* checkboxes / radios */
input[type="checkbox"], input[type="radio"] {
    accent-color: var(--accent);
    width: 14px; height: 14px;
    cursor: pointer;
}

.filter-row {
    display: flex;
    align-items: center;
    gap: 8px;
    padding: 4px 0;
    font-size: 12px;
    color: var(--text-soft);
}
.filter-row label { cursor: pointer; flex: 1; }
.filter-row:hover { color: var(--text); }
.filter-row input[type="range"] { flex: 1; width: auto; }

.layout-toggle {
    display: flex;
    background: var(--bg-input);
    border: 1px solid var(--border-strong);
    border-radius: var(--radius-sm);
    padding: 3px;
    margin-bottom: 9px;
    gap: 3px;
}
.layout-option {
    flex: 1;
    display: flex;
    align-items: center;
    justify-content: center;
    gap: 6px;
    font-size: 11.5px;
    font-weight: 600;
    color: var(--text-muted);
    padding: 5px 0;
    border-radius: var(--radius-xs);
    cursor: pointer;
    transition: all .15s;
}
.layout-option:has(input:checked) {
    background: var(--accent-soft);
    color: var(--accent);
    box-shadow: inset 0 0 0 1px var(--border-glow);
}
.layout-option input { display: none; }

.collapsible-header {
    font-size: 12px;
    color: var(--text-soft);
    cursor: pointer;
    padding: 6px 0 2px;
    user-select: none;
    display: flex;
    align-items: center;
    gap: 6px;
    transition: color .15s;
}
.collapsible-header:hover { color: var(--accent); }
.clump-options { padding-left: 6px; }

.search-row { display: flex; gap: 6px; }
.search-row input { flex: 1; }
.search-row .btn { flex-shrink: 0; }

.example-picker select { font-size: 11.5px; font-family: var(--font-sans); }
.text-muted { color: var(--text-muted); }

/* ============ Witness Controls ============ */
.witness-controls {
    margin-top: 10px;
    background: var(--bg-card);
    border: 1px solid var(--border-strong);
    border-radius: var(--radius);
    padding: 12px;
    box-shadow: var(--shadow-1);
}

.witness-step-display {
    text-align: center;
    font-family: var(--font-mono);
    font-size: 13px;
    font-weight: 700;
    color: var(--accent);
    margin-bottom: 8px;
    letter-spacing: .4px;
}

.witness-scrubber-row { margin: 2px 0 10px; }

.witness-playback {
    display: flex;
    justify-content: center;
    gap: 6px;
    margin-bottom: 10px;
}

.witness-btn {
    width: 34px; height: 30px;
    display: inline-flex;
    align-items: center;
    justify-content: center;
    padding: 0;
    font-size: 13px;
    border-radius: 8px;
}

.witness-btn-play {
    background: var(--accent-grad);
    border: none;
    color: #0b1020;
    width: 40px;
    box-shadow: 0 2px 10px rgba(96,165,250,.4);
}
.witness-btn-play:hover { filter: brightness(1.12); color: #0b1020; }

.witness-speed-row {
    display: flex;
    align-items: center;
    gap: 8px;
    font-size: 11px;
    color: var(--text-muted);
    margin-bottom: 8px;
}
.witness-speed-row input { flex: 1; width: auto; }
#witness-speed-label { font-family: var(--font-mono); min-width: 32px; text-align: right; }

.witness-btn-close {
    width: 100%;
    font-size: 11px;
    color: var(--text-muted);
    background: transparent;
    border: 1px dashed var(--border-strong);
}
.witness-btn-close:hover { color: var(--bad-color); border-color: var(--bad-color); transform: none; box-shadow: none; background: transparent; }

/* ============ Graph Canvas ============ */
.graph-area {
    position: relative;
    background:
        radial-gradient(circle at 1px 1px, rgba(170,180,210,.07) 1px, transparent 0) 0 0 / 26px 26px,
        var(--bg-primary);
    overflow: hidden;
}

#cy { width: 100%; height: 100%; }

/* floating toolbar — glass pill */
.toolbar {
    position: absolute;
    bottom: 18px;
    left: 50%;
    transform: translateX(-50%);
    display: flex;
    gap: 4px;
    background: rgba(19,23,36,.82);
    border: 1px solid var(--border-strong);
    border-radius: 14px;
    padding: 6px;
    backdrop-filter: blur(10px);
    box-shadow: var(--shadow-2);
    z-index: 10;
}
.toolbar .btn { border: none; background: transparent; min-width: 38px; }
.toolbar .btn:hover { background: var(--bg-hover); transform: none; box-shadow: none; }

/* legend — floating glass card */
.legend {
    position: absolute;
    top: 16px;
    right: 16px;
    background: rgba(19,23,36,.85);
    border: 1px solid var(--border-strong);
    border-radius: var(--radius);
    padding: 10px 13px;
    backdrop-filter: blur(10px);
    box-shadow: var(--shadow-1);
    font-size: 11px;
    line-height: 1.9;
    color: var(--text-soft);
    z-index: 10;
}
.legend-title {
    font-size: 9.5px;
    text-transform: uppercase;
    letter-spacing: 1.2px;
    color: var(--text-muted);
    margin-bottom: 4px;
}
.legend-item { display: flex; align-items: center; gap: 8px; }
.legend-swatch {
    width: 11px; height: 11px;
    border-radius: 3.5px;
    border: 1.5px solid;
    display: inline-block;
    flex-shrink: 0;
}

/* ============ Empty-state hero ============ */
.hero {
    position: absolute;
    inset: 0;
    display: flex;
    align-items: center;
    justify-content: center;
    z-index: 5;
    pointer-events: none;
}
.hero.hidden { display: none !important; }

.hero-card {
    pointer-events: auto;
    text-align: center;
    background: rgba(19,23,36,.88);
    border: 1px solid var(--border-strong);
    border-radius: 18px;
    padding: 42px 56px;
    backdrop-filter: blur(12px);
    box-shadow: var(--shadow-2);
    max-width: 500px;
    animation: hero-in .5s cubic-bezier(.2,.8,.2,1);
}
@keyframes hero-in {
    from { opacity: 0; transform: translateY(14px) scale(.98); }
    to   { opacity: 1; transform: none; }
}

.hero-mark {
    width: 56px; height: 56px;
    margin: 0 auto 18px;
    border-radius: 16px;
    background: var(--accent-grad);
    box-shadow: 0 6px 28px rgba(96,165,250,.45);
}

.hero-card h2 {
    font-size: 19px;
    font-weight: 800;
    letter-spacing: -.3px;
    margin-bottom: 6px;
}
.hero-card p {
    color: var(--text-muted);
    font-size: 12.5px;
    margin-bottom: 20px;
    line-height: 1.55;
}
.hero-actions { display: flex; gap: 10px; justify-content: center; margin-bottom: 16px; flex-wrap: wrap; }
.hero-actions .btn { padding: 9px 18px; font-size: 13px; }
.hero-hint {
    font-size: 11px;
    color: var(--text-muted);
    border-top: 1px dashed var(--border-strong);
    padding-top: 12px;
    line-height: 2;
}
.hero-hint kbd, .status-bar kbd {
    font-family: var(--font-mono);
    font-size: 10px;
    background: var(--bg-input);
    border: 1px solid var(--border-strong);
    border-bottom-width: 2px;
    border-radius: 4px;
    padding: 1px 5px;
}

/* drag-over glow */
.graph-area.dragover::after {
    content: "Drop a .btor2 model or .wit witness";
    position: absolute; inset: 12px;
    border: 2px dashed var(--accent);
    border-radius: 16px;
    display: flex;
    align-items: center;
    justify-content: center;
    font-size: 15px;
    font-weight: 700;
    color: var(--accent);
    background: rgba(56,189,248,.07);
    z-index: 50;
    pointer-events: none;
}

/* ============ Node list ============ */
.node-list-container {
    flex: 1;
    overflow-y: auto;
    padding: 6px 10px 14px;
    min-height: 120px;
}

.node-group-label {
    font-size: 10px;
    text-transform: uppercase;
    letter-spacing: 1px;
    color: var(--text-muted);
    padding: 9px 4px 3px;
}

.node-item {
    display: flex;
    align-items: center;
    gap: 8px;
    font-family: var(--font-mono);
    font-size: 11.5px;
    padding: 4px 8px;
    border-radius: var(--radius-xs);
    cursor: pointer;
    color: var(--text-soft);
    transition: background .12s, color .12s;
}
.node-item:hover { background: var(--bg-hover); color: var(--text); }
.node-item .nid { color: var(--text-muted); min-width: 34px; }

.placeholder {
    color: var(--text-muted);
    font-size: 12px;
    padding: 10px 6px;
    font-style: italic;
}

/* ============ Right panel: details / trace / stats ============ */
.detail-panel {
    flex: 1;
    overflow-y: auto;
    padding: 10px 14px;
    min-height: 100px;
}

.detail-header {
    display: flex;
    align-items: center;
    gap: 8px;
    margin-bottom: 10px;
}
.detail-nid {
    font-family: var(--font-mono);
    font-weight: 700;
    font-size: 14px;
    color: var(--text);
}
.detail-op {
    font-family: var(--font-mono);
    font-size: 10px;
    font-weight: 600;
    text-transform: uppercase;
    letter-spacing: .6px;
    border-radius: 99px;
    padding: 2px 9px;
    background: var(--accent-soft);
    color: var(--accent);
    border: 1px solid var(--border-glow);
}
.detail-op.state { background: rgba(74,222,128,.1); color: var(--state-color); border-color: rgba(74,222,128,.3); }
.detail-op.bad   { background: rgba(248,113,113,.1); color: var(--bad-color); border-color: rgba(248,113,113,.3); }

.detail-row {
    font-size: 12px;
    padding: 3px 0;
    color: var(--text-soft);
    line-height: 1.5;
    word-break: break-word;
}
.detail-row .label { color: var(--text-muted); margin-right: 6px; }

.detail-section {
    font-size: 10px;
    text-transform: uppercase;
    letter-spacing: 1px;
    color: var(--text-muted);
    margin: 12px 0 5px;
    padding-bottom: 3px;
    border-bottom: 1px solid var(--border);
}

.detail-links { display: flex; flex-direction: column; gap: 1px; }
.node-link {
    font-family: var(--font-mono);
    font-size: 11.5px;
    padding: 3px 7px;
    border-radius: var(--radius-xs);
    cursor: pointer;
    transition: background .12s;
    line-height: 1.45;
}
.node-link:hover { background: var(--bg-hover); }

.trace-panel {
    padding: 14px 14px 10px;
    border-bottom: 1px solid var(--border);
    background: linear-gradient(180deg, rgba(96,165,250,.05), transparent);
}
.trace-row {
    display: flex;
    justify-content: space-between;
    font-size: 12px;
    color: var(--text-soft);
    padding: 2.5px 0;
}
.trace-row .label { color: var(--text-muted); }
.trace-value { font-family: var(--font-mono); font-weight: 600; }

.stats-panel {
    padding: 12px 14px 16px;
    border-top: 1px solid var(--border);
    flex-shrink: 0;
}
.stats-panel h3 {
    font-size: 10.5px !important;
    text-transform: uppercase;
    letter-spacing: 1.2px;
    color: var(--text-muted);
    margin-bottom: 8px;
}
.stat-row {
    display: flex;
    justify-content: space-between;
    font-size: 12px;
    padding: 2px 0;
    color: var(--text-soft);
}
.stat-row .stat-value { font-family: var(--font-mono); color: var(--text); font-weight: 600; }

/* ============ Status bar ============ */
.status-bar {
    grid-column: 1 / -1;
    padding: 6px 16px;
    font-size: 11.5px;
    font-family: var(--font-mono);
    color: var(--text-muted);
    background: var(--bg-secondary);
    border-top: 1px solid var(--border);
    display: flex;
    align-items: center;
    gap: 9px;
    white-space: nowrap;
    overflow: hidden;
    text-overflow: ellipsis;
}
.status-bar::before {
    content: "";
    width: 7px; height: 7px;
    border-radius: 50%;
    background: var(--state-color);
    box-shadow: 0 0 7px rgba(74,222,128,.7);
    animation: pulse 2.4s ease-in-out infinite;
    flex-shrink: 0;
}
@keyframes pulse {
    0%, 100% { opacity: 1; }
    50% { opacity: .45; }
}

/* ============ Overlays (paste dialogs, help) ============ */
.paste-overlay {
    position: fixed;
    inset: 0;
    background: rgba(5,7,12,.7);
    backdrop-filter: blur(6px);
    display: flex;
    align-items: center;
    justify-content: center;
    z-index: 100;
    animation: fade-in .18s ease;
}
@keyframes fade-in { from { opacity: 0; } to { opacity: 1; } }

.paste-dialog {
    background: var(--bg-panel);
    border: 1px solid var(--border-strong);
    border-radius: 14px;
    padding: 22px;
    width: min(640px, 90vw);
    box-shadow: var(--shadow-2);
    animation: hero-in .25s cubic-bezier(.2,.8,.2,1);
}
.paste-dialog h3 {
    font-size: 14px;
    margin-bottom: 12px;
    font-weight: 700;
}
.paste-dialog textarea {
    height: 290px;
    resize: vertical;
    margin-bottom: 12px;
    line-height: 1.5;
}
.paste-dialog .btn-group { justify-content: flex-end; }

/* keyboard help */
.help-table { width: 100%; border-collapse: collapse; }
.help-table td { padding: 5px 8px; font-size: 12.5px; color: var(--text-soft); }
.help-table td:first-child { width: 150px; }
.help-table kbd {
    font-family: var(--font-mono);
    font-size: 11px;
    background: var(--bg-input);
    border: 1px solid var(--border-strong);
    border-bottom-width: 2px;
    border-radius: 5px;
    padding: 2px 7px;
    color: var(--text);
}

/* ============ Toasts ============ */
.toast-container {
    position: fixed;
    bottom: 46px;
    right: 18px;
    display: flex;
    flex-direction: column;
    gap: 8px;
    z-index: 200;
    pointer-events: none;
}
.toast {
    background: rgba(19,23,36,.95);
    border: 1px solid var(--border-strong);
    border-left: 3px solid var(--accent);
    border-radius: 10px;
    padding: 10px 16px;
    font-size: 12.5px;
    color: var(--text);
    box-shadow: var(--shadow-2);
    backdrop-filter: blur(10px);
    animation: toast-in .25s cubic-bezier(.2,.8,.2,1);
    max-width: 380px;
}
.toast.error { border-left-color: var(--bad-color); }
.toast.success { border-left-color: var(--state-color); }
.toast.leaving { animation: toast-out .3s ease forwards; }
@keyframes toast-in {
    from { opacity: 0; transform: translateX(24px); }
    to   { opacity: 1; transform: none; }
}
@keyframes toast-out {
    to { opacity: 0; transform: translateX(24px); }
}

/* ============ Misc ============ */
.hidden { display: none !important; }

.subgraph-info {
    font-size: 11.5px;
    color: var(--text-muted);
    padding-bottom: 7px;
}

.depth-control { margin-top: 8px; }
#depth-value {
    font-family: var(--font-mono);
    font-size: 11px;
    min-width: 26px;
    text-align: right;
    color: var(--accent);
}