applyBetaToAlphaRoute function

Map<Logic, (Set<Logic>, List<int>)> applyBetaToAlphaRoute(DefaultMap<Logic, Set<Logic>> alphaImplications, List<(Logic, Logic)> betaRules)

apply additional beta-rules (And conditions) to already-built alpha implication tables

e.g.

alphaImplications:

a -> b, !c, d b -> d ...

betaRules: &(b,d) -> e

then we'll extend a's rule to the following a -> b, !c, d, e

Implementation

Map<Logic, (Set<Logic>, List<int>)> applyBetaToAlphaRoute(
    DefaultMap<Logic, Set<Logic>> alphaImplications,
    List<(Logic, Logic)> betaRules) {
  final Map<Logic, (Set<Logic>, List<int>)> xImpl = {};
  for (final x in alphaImplications.keys) {
    xImpl[x] = (alphaImplications[x].toSet(), <int>[]);
  }
  for (final (bCond, _) in betaRules) {
    for (final bk in bCond.args) {
      if (xImpl.containsKey(bk)) {
        continue;
      }
      xImpl[bk] = (<Logic>{}, <int>[]);
    }
  }

  // static extensions to alpha rules:
  // A: x -> a,b   B: &(a,b) -> c  ==>  A: x -> a,b,c
  bool seenStaticExtension = true;
  while (seenStaticExtension) {
    seenStaticExtension = false;

    for (final (bCond, bImpl) in betaRules) {
      if (bCond is! And) {
        throw ArgumentError("Cond is not And");
      }
      final bArgs = bCond.args.toSet();
      for (final entry in xImpl.entries) {
        final (x, value) = (entry.key, entry.value);
        final (xImpls, bb) = value;
        final xAll = xImpls.union({x});
        // A: ... -> a   B: &(...) -> a  is non-informative
        if (!xAll.contains(bImpl) && xAll.containsAll(bArgs)) {
          xImpls.add(bImpl);

          // we introduced new implication - now we have to restore
          // completeness of the whole set.
          final bImplImpl = xImpl[bImpl];
          if (bImplImpl != null) {
            xImpls.addAll(bImplImpl.$1);
          }
          seenStaticExtension = true;
        }
      }
    }
  }

  // attach beta-nodes which can be possibly triggered by an alpha-chain
  for (int bIdx = 0; bIdx < betaRules.length; bIdx++) {
    final (bCond, bImpl) = betaRules[bIdx];
    final bArgs = bCond.args.toSet();
    for (final entry in xImpl.entries) {
      final (x, value) = (entry.key, entry.value);
      final (xImpls, bb) = value;
      final xAll = xImpls.union({x});
      // A: ... -> a   B: &(...) -> a      (non-informative)
      if (xAll.contains(bImpl)) {
        continue;
      }
      // A: x -> a...  B: &(!a,...) -> ... (will never trigger)
      // A: x -> a...  B: &(...) -> !a     (will never trigger)
      if ([
        for (final xi in xAll)
          (bArgs.contains(Not.create(xi)) || bImpl == Not.create(xi))
      ].any((b) => b)) {
        continue;
      }

      if (bArgs.intersection(xAll).isNotEmpty) {
        bb.add(bIdx);
      }
    }
  }

  return xImpl;
}