cannorin/cannorin.net
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

kripke: improve constant optimization (#107)

Browse Source 
* kripke: improve constant optimization

* kripke: improve constant optimization (2)

---------

Co-authored-by: cannorin <cannorin@users.noreply.github.com>
This commit is contained in:
cannorin
2025-11-02 16:10:35 +09:00
committed by GitHub
parent 09f1aaf68b
commit 9b75cf11c9
1 changed files with 11 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files

25
packages/kripke/src/sat.ts
View File

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