updated visualization page

Author: jackeown

docusaurus-site/src/components/ProofSearchCanvas.js

@@ -23,6 +23,7 @@ const LIGHT_COLORS = {
   tooltipSym: '#f8f4f4',
   tooltipPunct: '#c0b0b0',
   subsumed: '#ff4d4d',
+  negated: '#7c3aed',
   highlight: '#fff59d',
 };
 
@@ -48,6 +49,7 @@ const DARK_COLORS = {
   tooltipSym: '#f3eaea',
   tooltipPunct: '#b9aaaa',
   subsumed: '#ff4d4d',
+  negated: '#c084fc',
   highlight: '#fff59d',
 };
 
@@ -133,6 +135,7 @@ export default function ProofSearchCanvas({
           prevStatus: null,
           statusChangedAt: now,
           subsumed: Boolean(clause.subsumed),
+          negated: Boolean(clause.negated),
           x: baseX + Math.cos(angle) * radius,
           y: baseY + Math.sin(angle) * radius,
           vx: 0,
@@ -157,6 +160,7 @@ export default function ProofSearchCanvas({
           node.statusChangedAt = now;
         }
         node.subsumed = Boolean(clause.subsumed);
+        node.negated = Boolean(clause.negated);
       }
     });
     // Remove nodes that are no longer in the current clause set
@@ -475,6 +479,17 @@ export default function ProofSearchCanvas({
           ctx.restore();
         }
 
+        if (node.negated) {
+          ctx.save();
+          ctx.globalAlpha = 0.9;
+          ctx.strokeStyle = palette.negated;
+          ctx.lineWidth = 2;
+          ctx.beginPath();
+          ctx.arc(node.x, node.y, radius * pulse - 4, 0, Math.PI * 2);
+          ctx.stroke();
+          ctx.restore();
+        }
+
         // Label
         ctx.globalAlpha = 1;
         ctx.fillStyle = palette.text;

docusaurus-site/src/pages/proof-search-visualization.jsx

@@ -241,6 +241,7 @@ export default function ProofSearchVisualization() {
   const runIdRef = useRef(0);
   const cancelRunRef = useRef(null);
   const szsDoneRef = useRef(false);
+  const negatedRef = useRef(new Set());
 
   useEffect(() => {
     outputRef.current = output;
@@ -284,6 +285,7 @@ export default function ProofSearchVisualization() {
   const resetRunState = () => {
     clauseMapRef.current.clear();
     edgeMapRef.current.clear();
+    negatedRef.current.clear();
     setClauses([]);
     setEdges([]);
     setSelectedId(null);
@@ -302,10 +304,21 @@ export default function ProofSearchVisualization() {
       text: text ?? existing?.text ?? '',
       status: status ?? existing?.status ?? 'new',
       subsumed: existing?.subsumed ?? false,
+      negated: existing?.negated ?? negatedRef.current.has(key),
     };
     map.set(key, next);
   };
 
+  const markNegated = (id) => {
+    const key = String(id);
+    negatedRef.current.add(key);
+    const map = clauseMapRef.current;
+    const existing = map.get(key);
+    if (existing) {
+      map.set(key, {...existing, negated: true});
+    }
+  };
+
   const markSubsumed = (id) => {
     const key = String(id);
     const map = clauseMapRef.current;
@@ -328,10 +341,12 @@ export default function ProofSearchVisualization() {
         ids: [],
         statusById: new Map(),
         subsumedById: new Map(),
+        negatedById: new Map(),
       };
       entry.ids.push(String(clause.id));
       entry.statusById.set(String(clause.id), clause.status || 'new');
       entry.subsumedById.set(String(clause.id), Boolean(clause.subsumed));
+      entry.negatedById.set(String(clause.id), Boolean(clause.negated));
       grouped.set(textKey, entry);
     });
 
@@ -354,12 +369,14 @@ export default function ProofSearchVisualization() {
         ? 'passive'
         : (activeIds.length ? 'active' : 'new');
       const subsumed = entry.subsumedById.get(displayId) || false;
+      const negated = entry.negatedById.get(displayId) || false;
       entry.ids.forEach((id) => idToDisplay.set(id, displayId));
       displayClauses.push({
         id: displayId,
         text: entry.text,
         status,
         subsumed,
+        negated,
       });
     });
 
@@ -415,6 +432,12 @@ export default function ProofSearchVisualization() {
   };
 
   const parseOutputLine = (line) => {
+    if (/negated conjecture/i.test(line)) {
+      const idMatch = line.match(/:\s*(\d+)\.\s/);
+      if (idMatch) {
+        markNegated(idMatch[1]);
+      }
+    }
     const reduceMatch = line.match(REDUCE_RE);
     if (reduceMatch) {
       markSubsumed(reduceMatch[2]);
@@ -431,6 +454,16 @@ export default function ProofSearchVisualization() {
         bracket = bracketMatches[bracketMatches.length - 1][1];
         text = text.replace(/\s*\[[^\]]+\]\s*$/, '');
       }
+      if (bracket) {
+        if (/negated conjecture/i.test(bracket)) {
+          markNegated(id);
+        } else {
+          const refs = Array.from(bracket.matchAll(/\b(\d+)\b/g)).map((m) => m[1]);
+          if (refs.some((ref) => negatedRef.current.has(String(ref)))) {
+            markNegated(id);
+          }
+        }
+      }
       if (tag === 'SA') {
         const status = normalizePhaseStatus(phase);
         if (status === 'new') {
@@ -577,25 +610,29 @@ export default function ProofSearchVisualization() {
             <div className={styles.canvasFooter}>
               <div className={styles.legend}>
                 <span className={styles.legendItem}>
-                  <span className={styles.dot} style={{background: '#ff9fb2'}} />
+                  <span className={`${styles.dot} ${styles.legendDotNew}`} />
                   New
                 </span>
                 <span className={styles.legendItem}>
-                  <span className={styles.dot} style={{background: '#b62929'}} />
+                  <span className={`${styles.dot} ${styles.legendDotActive}`} />
                   Active
                 </span>
                 <span className={styles.legendItem}>
-                  <span className={styles.dot} style={{background: '#8a8a8a'}} />
+                  <span className={`${styles.dot} ${styles.legendDotPassive}`} />
                   Passive
                 </span>
                 <span className={styles.legendItem}>
-                  <span className={styles.dot} style={{background: '#f97316'}} />
+                  <span className={`${styles.dot} ${styles.legendDotSelected}`} />
                   Selected
                 </span>
                 <span className={styles.legendItem}>
                   <span className={`${styles.dot} ${styles.subsumedDot}`} />
                   Subsumed
                 </span>
+                <span className={styles.legendItem}>
+                  <span className={`${styles.dot} ${styles.negatedDot}`} />
+                  Negated conjecture
+                </span>
               </div>
               <div className={styles.hint}>
                 {awaitingInput ? 'Waiting for your clause choice…' : 'Awaiting run'}

docusaurus-site/src/pages/proof-search-visualization.module.css

@@ -299,9 +299,47 @@
   border-radius: 50%;
 }
 
+.legendDotNew {
+  background: #ff9fb2;
+}
+
+.legendDotActive {
+  background: #b62929;
+}
+
+.legendDotPassive {
+  background: #8a8a8a;
+}
+
+.legendDotSelected {
+  background: #f97316;
+}
+
+:global([data-theme='dark']) .legendDotNew {
+  background: #ff3b5c;
+}
+
+:global([data-theme='dark']) .legendDotActive {
+  background: #9a1b1b;
+}
+
+:global([data-theme='dark']) .legendDotPassive {
+  background: #5f5f5f;
+}
+
+:global([data-theme='dark']) .legendDotSelected {
+  background: #f59e0b;
+}
+
 .subsumedDot {
   background: rgba(154, 166, 178, 0.6);
   border: 2px solid #ff6b6b;
+  border-style: dashed;
+}
+
+.negatedDot {
+  background: transparent;
+  border: 2px solid #7c3aed;
 }
 
 .modalBackdrop {