Function assumeConjunction

src/compute-engine/assume.ts:164–193

* Assume a conjunction: each conjunct is assumed independently * (design §3.2, "shallow saturation"). * * Result: `'contradiction'` if any conjunct contradicts, * `'not-a-predicate'` if any conjunct is unsupported, `'tautology'` if * every conjunct was already known, `'ok'` otherwise.

(proposition: Expression)

  //    restore in the current context): `withValueShield` pushes a fresh
  //    eval-context whose assumptions map is discarded on pop, which would lose
  //    the very fact being recorded, so it cannot be used here.
  return withValueBlindRecording(names, () => assumeDispatch(proposition));

  /** Strip the assigned value of each name for the duration of `fn`, then
   * restore it, so the recording pipeline sees the symbols as valueless (a
   * fact `w > 0` instead of the folded `5 > 0 → True`). */
  function withValueBlindRecording<T>(names: string[], fn: () => T): T {
    const ce = proposition.engine;
    const saved: { name: string; value: Expression }[] = [];
    for (const name of names) {
      const def = ce.lookupDefinition(name);
      if (!isValueDef(def) || def.value.isConstant) continue;
      const value = def.value.value;
      if (value === undefined || value === null) continue;
      saved.push({ name, value });
      ce._setSymbolValue(name, undefined);
    }
    if (saved.length === 0) return fn();
    try {
      return fn();
    } finally {
      for (const { name, value } of saved) ce._setSymbolValue(name, value);
    }
  }
}

function assumeDispatch(proposition: Expression): AssumeResult {
  const op = proposition.operator;
  if (op === 'Element') return assumeElement(proposition);
  if (op === 'NotElement') return assumeNotElement(proposition);
  if (op === 'Equal') return assumeEquality(proposition);
  if (op === 'NotEqual') return assumeNotEqual(proposition);
  if (op === 'And') return assumeConjunction(proposition);