From 9b75cf11c9ba2ea1f8a6c73d5c2f1c6b1bfd32de Mon Sep 17 00:00:00 2001
From: cannorin <13620400+cannorin@users.noreply.github.com>
Date: Sun, 2 Nov 2025 16:10:35 +0900
Subject: [PATCH] kripke: improve constant optimization (#107)

* kripke: improve constant optimization

* kripke: improve constant optimization (2)

---------

Co-authored-by: cannorin <cannorin@users.noreply.github.com>
---
 packages/kripke/src/sat.ts | 25 +++++++++++--------------
 1 file changed, 11 insertions(+), 14 deletions(-)

diff --git a/packages/kripke/src/sat.ts b/packages/kripke/src/sat.ts
index 919b3ab..71f0ae7 100644
--- a/packages/kripke/src/sat.ts
+++ b/packages/kripke/src/sat.ts
@@ -72,11 +72,9 @@ export function buildContext(frame: Frame, fml: Formula): Context {
         addConstants(f.fml);
         for (const w1 of worlds) {
           const xs = next[w1].map((w2) => constant.get(`${w2}:${f.fml.tag}`));
-          if (xs.some((x) => x === undefined)) continue;
-          constant.set(
-            `${w1}:${f.tag}`,
-            xs.every((x) => x === true),
-          );
+          if (xs.some((x) => x === false))
+            constant.set(`${w1}:${f.tag}`, false);
+          if (xs.every((x) => x === true)) constant.set(`${w1}:${f.tag}`, true);
         }
         return;
       }
@@ -84,11 +82,9 @@ export function buildContext(frame: Frame, fml: Formula): Context {
         addConstants(f.fml);
         for (const w1 of worlds) {
           const xs = next[w1].map((w2) => constant.get(`${w2}:${f.fml.tag}`));
-          if (xs.some((x) => x === undefined)) continue;
-          constant.set(
-            `${w1}:${f.tag}`,
-            xs.some((x) => x === true),
-          );
+          if (xs.some((x) => x === true)) constant.set(`${w1}:${f.tag}`, true);
+          if (xs.every((x) => x === false))
+            constant.set(`${w1}:${f.tag}`, false);
         }
         return;
       }
@@ -98,8 +94,9 @@ export function buildContext(frame: Frame, fml: Formula): Context {
         for (const w of worlds) {
           const l = constant.get(`${w}:${f.left.tag}`);
           const r = constant.get(`${w}:${f.right.tag}`);
-          if (l === undefined || r === undefined) continue;
-          constant.set(`${w}:${f.tag}`, l || r);
+          if (l === true || r === true) constant.set(`${w}:${f.tag}`, true);
+          else if (l === false && r === false)
+            constant.set(`${w}:${f.tag}`, false);
         }
         return;
       }
@@ -109,8 +106,8 @@ export function buildContext(frame: Frame, fml: Formula): Context {
         for (const w of worlds) {
           const l = constant.get(`${w}:${f.left.tag}`);
           const r = constant.get(`${w}:${f.right.tag}`);
-          if (l === undefined || r === undefined) continue;
-          constant.set(`${w}:${f.tag}`, l && r);
+          if (l === false || r === false) constant.set(`${w}:${f.tag}`, false);
+          if (l === true && r === true) constant.set(`${w}:${f.tag}`, true);
         }
         return;
       }