(proposition: Expression)
| 280 | // `And(p > 0, p < −5)` reported `'contradiction'` yet left `p > 0`). |
| 281 | // |
| 282 | // Validate the whole conjunction in an isolated child scope first: the |
| 283 | // child inherits the caller's assumptions (copied) and symbol bindings (via |
| 284 | // the scope chain) but discards all of its own mutations on `popScope`. If |
| 285 | // the trial contradicts, nothing touched the caller's scope. Only a |
| 286 | // contradiction-free trial is replayed for real in the caller's scope, |
| 287 | // reproducing the historical `ok`/`tautology`/`not-a-predicate` outcome |
| 288 | // (including the partial application of the valid conjuncts in the |
| 289 | // `not-a-predicate` case). |
| 290 | ce.pushScope(); |
| 291 | let trial: AssumeResult; |
| 292 | try { |
| 293 | trial = assumeConjunctionInner(proposition); |
| 294 | } finally { |
| 295 | ce.popScope(); |
| 296 | } |
| 297 | if (trial === 'contradiction' || trial === 'internal-error') return trial; |
| 298 | |
| 299 | return assumeConjunctionInner(proposition); |
| 300 | } |
| 301 | |
| 302 | function assumeConjunctionInner(proposition: Expression): AssumeResult { |
| 303 | if (!isFunction(proposition)) return 'not-a-predicate'; |
| 304 | let sawOk = false; |
| 305 | let sawNotAPredicate = false; |
| 306 | for (const conjunct of proposition.ops) { |
| 307 | const result = assume(conjunct); |
| 308 | if (result === 'contradiction' || result === 'internal-error') |
| 309 | return result; |
| 310 | if (result === 'not-a-predicate') sawNotAPredicate = true; |
| 311 | else if (result === 'ok') sawOk = true; |
| 312 | } |
| 313 | if (sawNotAPredicate) return 'not-a-predicate'; |
| 314 | return sawOk ? 'ok' : 'tautology'; |
| 315 | } |
| 316 | |
| 317 | /** |
| 318 | * Assume a disequality `NotEqual(x, v)` or `NotEqual(Part(x), v)` |
| 319 | * (design §4.1; stored in the §3.2 normal form `NotEqual(subject, v)`). |
| 320 | */ |
| 321 | function assumeNotEqual(proposition: Expression): AssumeResult { |
| 322 | console.assert(proposition.operator === 'NotEqual'); |
| 323 | if (!isFunction(proposition) || proposition.ops.length !== 2) |
| 324 | return 'not-a-predicate'; |
| 325 | return storeNotEqual(proposition.engine, proposition.op1, proposition.op2); |
| 326 | } |
| 327 | |
| 328 | /** |
| 329 | * Store a `NotEqual(lhs, rhs)` fact in the assumptions DB. |
| 330 | * |
| 331 | * Contradiction scope (design §4.3): if neither side has unknowns (e.g. |
| 332 | * the symbol has an assigned value), the disequality is decided now and |
| 333 | * yields `'tautology'`/`'contradiction'` instead of being stored. |
| 334 | */ |
| 335 | function storeNotEqual( |
| 336 | ce: ComputeEngine, |
| 337 | lhs: Expression, |
| 338 | rhs: Expression |
| 339 | ): AssumeResult { |
no test coverage detected