Grade a Wolfram batch result with the same soundness+completeness oracle as * CE: a returned real root is sound iff |residual| < TOL.
(c: Case, res: any)
| 137 | function runWolframAll(): Record<string, any> { |
| 138 | const by: Record<string, any> = {}; |
| 139 | const tasks = cases.map((c) => { |
| 140 | try { |
| 141 | return { id: c.id, op: 'solve', expr: mathJsonToWL(c.ce.mathjson), var: c.ce.var, points: [] }; |
| 142 | } catch (e: any) { |
| 143 | by[c.id] = { status: 'error', error: String(e?.message ?? e).slice(0, 120) }; |
| 144 | return null; |
| 145 | } |
| 146 | }).filter(Boolean); |
| 147 | if (!tasks.length) return by; |
| 148 | const tmp = join(tmpdir(), `solve-wl-${process.pid}.json`); |
| 149 | writeFileSync(tmp, JSON.stringify({ real: false, tasks })); |
| 150 | try { |
| 151 | const out = execFileSync(NODE, [WOLFRAM_BATCH, tmp], { encoding: 'utf8', timeout: 1800000, maxBuffer: 64 * 1024 * 1024 }); |
| 152 | for (const line of out.trim().split('\n')) { try { const o = JSON.parse(line); if (o.id) by[o.id] = o; } catch {} } |
| 153 | } catch (e: any) { console.error('wolfram failed:', (e.message || e).toString().split('\n')[0]); } |
| 154 | return by; |
| 155 | } |
| 156 | |
| 157 | /** Grade a Wolfram batch result with the same soundness+completeness oracle as |
| 158 | * CE: a returned real root is sound iff |residual| < TOL. */ |
| 159 | function gradeWolfram(c: Case, res: any): { v: Verdict; note?: string } { |