From fef4ddfbba500428f94fd1299d4bee4990f88f85 Mon Sep 17 00:00:00 2001 From: Zaid Abdulla Date: Mon, 17 Aug 2020 16:34:57 -0700 Subject: [PATCH] Fix canRaise bug wrecking expression synthesis --- lib/common/boolean-expression.ts | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) diff --git a/lib/common/boolean-expression.ts b/lib/common/boolean-expression.ts index 0ec808f..33f3355 100644 --- a/lib/common/boolean-expression.ts +++ b/lib/common/boolean-expression.ts @@ -1065,6 +1065,29 @@ function mapCallback(exp: Expression | BoolExprSynth): Expression { return exp; } +function getCanRaiseCallback( + isNull: Map +): (idx: number, set: Set) => boolean { + return (idx: number, set: Set): boolean => { + const i = idx >> 2; + const n = isNull.get(i); + if (n != null) { + if (!(idx & 1)) return true; + if (set.has((n << 2) ^ 2)) return true; + if (set.has((n << 2) ^ 3)) return true; + return !set.has(idx ^ 3); + } + for (const [k, v] of isNull) { + if (v !== i) continue; + if (set.has((k << 2) ^ 1)) continue; + if (set.has((k << 2) ^ 3)) continue; + if (set.has((k << 2) ^ 0)) return false; + if (set.has((k << 2) ^ 2)) return false; + } + return true; + }; +} + export function minimize(expr: Expression, boolean = false): Expression { expr = normalize(expr); expr = map(expr, mapCallback); @@ -1076,8 +1099,7 @@ export function minimize(expr: Expression, boolean = false): Expression { Array.from(context).map(([k, v]) => [v, JSON.parse(k) as Expression]) ); const { dcSet, isNull } = generateDcSetAndIsNull(variables); - const canRaise = (idx: number, set: Set): boolean => - !isNull.has(idx >> 2) || !(idx & 1) || !set.has(idx ^ 3); + const canRaise = getCanRaiseCallback(isNull); const res: Expression = ["CASE"]; for (let i = 1; i < expr.length; i += 2) { let minterms = sanitizeMinterms(whens[(i - 1) / 2], isNull); @@ -1149,8 +1171,7 @@ export function unionDiff( isNull ); - const canRaise = (idx: number, set: Set): boolean => - !isNull.has(idx >> 2) || !(idx & 1) || !set.has(idx ^ 3); + const canRaise = getCanRaiseCallback(isNull); const union = espresso(unionMinterms, dcSet, { canRaise }); const diff = espresso(diffMinterms, dcSet, { canRaise });