diff --git a/pkg/status_file/lib/src/disjunctive.dart b/pkg/status_file/lib/src/disjunctive.dart new file mode 100644 index 00000000000..55dd7b7ab34 --- /dev/null +++ b/pkg/status_file/lib/src/disjunctive.dart @@ -0,0 +1,464 @@ +// Copyright (c) 2017, the Dart project authors. Please see the AUTHORS file +// for details. All rights reserved. Use of this source code is governed by a +// BSD-style license that can be found in the LICENSE file. + +import 'expression.dart'; +import '../environment.dart'; + +final Expression T = new LogicExpression.and([]); +final Expression F = new LogicExpression.or([]); + +// Token to combine left and right value of a comparison expression in a +// variable expression. +final String _comparisonToken = "__"; + +/// Transforms an [expression] to disjunctive normal form, which is a +/// standardization where all clauses are separated by `||` (or/disjunction). +/// All clauses must be conjunction (joined by &&) and have negation on +/// literals. +/// +/// It computes the disjunctive normal form by computing a truth table with all +/// terms (truth assignment of variables) that make the [expression] become true +/// and then minimizes the terms. +/// +/// The procedure is exponential so [expression] should not be too big. +Expression toDisjunctiveNormalForm(Expression expression) { + var normalizedExpression = expression.normalize(); + var variableExpression = + _comparisonExpressionsToVariableExpressions(normalizedExpression); + var minTerms = _satisfiableMinTerms(variableExpression); + if (minTerms == null) { + return T; + } else if (minTerms.isEmpty) { + return F; + } + var disjunctiveNormalForm = new LogicExpression.or(minTerms); + disjunctiveNormalForm = _minimizeByComplementation(disjunctiveNormalForm); + return _recoverComparisonExpressions(disjunctiveNormalForm); +} + +/// Complementation is a process that tries to combine the min terms above as +/// much as possible. In each iteration, two minsets can be combined if they +/// differ by only one assignment. Ex: +/// +/// $a && $b can be combined with !$a && $b since they only differ by $a and +/// !$a. This is easier to see if we represent terms as bits. Let the following +/// min terms be defined: +/// +/// m(1): $a && !$b && !$c && !$d -> 1000 +/// m(2): $a && !$b && !$c && $d -> 1001 +/// m(3): $a && !$b && $c && !$d -> 1010 +/// m(4): $a && !$b && $c && $d -> 1011 +/// +/// In the first iteration, m(1) can be combined with m(2) and m(3), m(2) can be +/// combined with m(4) and m(3) can be combined with m(4). We now have: +/// +/// m(1,2): 100- +/// m(1,3): 10-0 +/// m(2,4): 10-1 +/// m(3,4): 101- +/// +/// Let - be a third bit value, which also counts toward difference. Therefore, +/// m(1,2) cannot be combined with m(1,3), but m(1,2) can be combined with +/// m(3,4). We therefore get: +/// +/// m(1,2,3,4): 10-- +/// m(1,3,2,4): 10-- +/// +/// At this point, we have two similar minsets, which we also call implicants, +/// that only differ from the way they were added together. These cannot be +/// added together further, so we are left with only one (does not matter which +/// we pick): +/// +/// m(1,2,3,4): 10-- +/// +/// The minimal disjunctive form is, for this example, $a && !$b. +/// +/// It is often not the case we only have one implicant left, we may have +/// several. +/// +/// m(4,12) +/// m(8,9,10,11) +/// m(8,10,12,14) +/// m(10,11,14,15) +/// +/// From here, we can find the minimum form by simply computing a set cover. We +/// can prune the search space a bit though. In the above example, 4 and 15 is +/// only covered by a single implicant. This means, that those are primary, and +/// has to be included in the cover. We then just need to pick the best +/// solution. +/// +/// More about this algorithm here: +/// https://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm +LogicExpression _minimizeByComplementation(LogicExpression expression) { + var clauses = expression.operands + .map((e) => e is LogicExpression ? e.operands : [e]) + .toList(); + // All min terms should be sorted by amount of 1's + clauses.sort((a, b) { + var onesInA = a.where((e) => !_isNegatedExpression(e)).length; + var onesInB = b.where((e) => !_isNegatedExpression(e)).length; + return onesInA - onesInB; + }); + var combinedMinSets = _combineMinSets( + clauses.map((e) => [new LogicExpression.and(e)]).toList(), []); + List> minCover = _findMinCover(combinedMinSets, []); + var finalOperands = minCover.map((minSet) => _reduceMinSet(minSet)).toList(); + return new LogicExpression.or(finalOperands).normalize(); +} + +/// Computes all assignments of literals that make the [expression] evaluate to +/// true. +List _satisfiableMinTerms(Expression expression) { + var variables = _getVariables(expression); + bool hasNotSatisfiableAssignment = false; + List satisfiableTerms = []; + var environment = new TruthTableEnvironment(variables); + for (int i = 0; i < 1 << variables.length; i++) { + environment.setConfiguration(i); + if (expression.evaluate(environment)) { + var operands = []; + for (int j = 0; j < variables.length; j++) { + if ((i >> j) % 2 == 0) { + operands.add(negate(variables[j])); + } else { + operands.add(variables[j]); + } + } + satisfiableTerms.add(new LogicExpression.and(operands)); + } else { + hasNotSatisfiableAssignment = true; + } + } + if (!hasNotSatisfiableAssignment) { + return null; + } + return satisfiableTerms; +} + +/// The [TruthTableEnvironment] simulates an entry in a truth table where the +/// [variables] are assigned a value bases on the [configuration]. This +/// environment can then be used to evaluate the corresponding expression from +/// which the [variables] was found. +class TruthTableEnvironment extends Environment { + final List variables; + int configuration; + + TruthTableEnvironment(this.variables); + + void setConfiguration(int configuration) { + this.configuration = configuration; + } + + @override + String lookUp(String name) { + int index = -1; + for (int i = 0; i < variables.length; i++) { + if (variables[i] is VariableExpression && + variables[i].toString() == "\$$name") { + index = i; + break; + } + } + assert(index > -1); + var isTrue = (configuration >> index) % 2 == 1; + return isTrue ? "true" : "false"; + } + + @override + void validate(String name, String value, List errors) {} +} + +/// Combines [minSets] recursively as long as possible. Prime implicants (those +/// that cannot be reduced further) are kept track of in [primeImplicants]. When +/// finished the function returns all combined min sets. +List> _combineMinSets( + List> minSets, List> primeImplicants) { + List> combined = new List>(); + var addedInThisIteration = new Set>(); + for (var i = 0; i < minSets.length; i++) { + var minSet = minSets[i]; + var combinedMinSet = false; + for (var j = i + 1; j < minSets.length; j++) { + var otherMinSet = minSets[j]; + if (_canCombine(minSet, otherMinSet)) { + combined.add(minSet.toList(growable: true)..addAll(otherMinSet)); + addedInThisIteration.add(otherMinSet); + combinedMinSet = true; + } + } + if (!combinedMinSet && !addedInThisIteration.contains(minSet)) { + primeImplicants.add(minSet); + } + } + if (combined.isNotEmpty) { + // it is possible to add minsets that are identical: + // ex: min(1,3), min(1,2) min(2,4) min(3,4) could combine to: + // min(1,3,2,4) and min(1,2,3,4) which are identical. + // It is better to reduce such now than to deal with them in an exponential + // search. + return _combineMinSets(_uniqueMinSets(combined), primeImplicants); + } + return primeImplicants; +} + +/// Two min sets can be combined if they only differ by one. We reduce min sets +/// and find their difference based on variables. +bool _canCombine(List a, List b) { + return _difference(_reduceMinSet(a).operands, _reduceMinSet(b).operands) + .length == + 1; +} + +/// This function finds the fixed variables for a collection of implicants in +/// the [minSet]. Unlike the numbering scheme above, ie 10-1 etc. we look +/// directly at variables and count positive and negative occurrences. If we +/// find an implicant with less variables than others, we add the variable to +/// both the positive and negative set, which is effectively setting the value +/// - to that variable. +LogicExpression _reduceMinSet(List minSet) { + var variables = []; + var positive = []; + var negative = []; + for (var implicant in minSet) { + for (var expression in implicant.operands) { + assert(expression is! LogicExpression); + var variable = expression; + if (_isNegatedExpression(expression)) { + _addIfNotPresent(expression, negative); + variable = _getVariables(expression)[0]; + } else { + _addIfNotPresent(expression, positive); + } + _addIfNotPresent(variable, variables); + } + } + for (var implicant in minSet) { + for (var variable in variables) { + bool isFree = implicant.operands.where((literal) { + if (_isNegatedExpression(literal)) { + return negate(literal).compareTo(variable) == 0; + } else { + return literal.compareTo(variable) == 0; + } + }).isEmpty; + if (isFree) { + _addIfNotPresent(variable, positive); + _addIfNotPresent(negate(variable), negative); + } + } + } + for (var neg in negative.toList()) { + var pos = _findFirst(negate(neg), positive); + if (pos != null) { + positive.remove(pos); + negative.remove(neg); + } + } + return new LogicExpression.and(positive..addAll(negative)); +} + +/// [_findMinCover] finds the minimum cover of [primaryImplicants]. Finding a +/// minimum set cover is NP-hard, and we are not trying to be really cleaver +/// here. The implicants that cover only a single truth assignment can be +/// directly added to [cover]. +List> _findMinCover( + List> primaryImplicants, List> cover) { + var minCover = primaryImplicants.toList()..addAll(cover); + if (cover.isEmpty) { + var allImplicants = primaryImplicants.toList(); + for (var implicant in allImplicants) { + for (var exp in implicant) { + bool found = false; + for (var otherImplicant in allImplicants) { + if (implicant != otherImplicant && + _findFirst(exp, otherImplicant) != null) { + found = true; + } + } + if (!found) { + cover.add(implicant); + primaryImplicants.remove(implicant); + break; + } + } + } + if (_isCover(cover, primaryImplicants)) { + return cover; + } + } + for (var implicant in primaryImplicants) { + var newCover = cover.toList()..add(implicant); + if (!_isCover(newCover, primaryImplicants)) { + var newPrimaryList = + primaryImplicants.where((i) => i != implicant).toList(); + newCover = _findMinCover(newPrimaryList, newCover); + } + if (newCover.length < minCover.length) { + minCover = newCover; + } + } + return minCover; +} + +/// Checks if [cover] is a set cover of [implicants] by searching through all +/// expressions in each implicant, to see if the cover has the same expression. +bool _isCover(List> cover, List> implicants) { + for (var implicant in implicants) { + for (var exp in implicant) { + if (cover.where((i) => _findFirst(exp, i) != null).isEmpty) { + return false; + } + } + } + return true; +} + +// Computes the difference between two sets of expressions in disjunctive normal +// form. if the difference is a negation, the difference is only counted once. +List _difference(List As, List Bs) { + var difference = new List() + ..addAll(As.where((a) => _findFirst(a, Bs) == null)) + ..addAll(Bs.where((b) => _findFirst(b, As) == null)); + for (var expression in difference.toList()) { + if (_isNegatedExpression(expression)) { + if (_findFirst(negate(expression), difference) != null) { + difference.remove(expression); + } + } + } + return difference; +} + +/// Finds the first occurrence of [expressionToFind] in [expressions] or +/// returns null. +Expression _findFirst( + expressionToFind, List expressions) { + return expressions.firstWhere( + (otherExpression) => expressionToFind.compareTo(otherExpression) == 0, + orElse: () => null); +} + +/// Adds [expressionToAdd] to [expressions] if is not present. +void _addIfNotPresent( + Expression expressionToAdd, List expressions) { + if (_findFirst(expressionToAdd, expressions) == null) { + expressions.add(expressionToAdd); + } +} + +/// Computes all unique min sets, thereby disregarding the order for which they +/// were combined. +List> _uniqueMinSets( + List> minSets) { + var uniqueMinSets = new List>(); + for (int i = 0; i < minSets.length; i++) { + bool foundEqual = false; + for (var j = i - 1; j >= 0; j--) { + if (_areMinSetsEqual(minSets[i], minSets[j])) { + foundEqual = true; + break; + } + } + if (!foundEqual) { + uniqueMinSets.add(minSets[i]); + } + } + return uniqueMinSets; +} + +/// Measures if two min sets are equal by checking that [minSet1] c [minSet2] +/// and minSet1.length == minSet2.length. +bool _areMinSetsEqual( + List minSet1, List minSet2) { + int found = 0; + for (var expression in minSet1) { + if (_findFirst(expression, minSet2) != null) { + found += 1; + } + } + return found == minSet2.length; +} + +bool _isNegatedExpression(Expression expression) { + return expression is VariableExpression && expression.negate || + expression is ComparisonExpression && expression.negate; +} + +/// Gets all variables occurring in the [expression]. +List _getVariables(Expression expression) { + if (expression is LogicExpression) { + var variables = []; + expression.operands.forEach( + (e) => _getVariables(e).forEach((v) => _addIfNotPresent(v, variables))); + return variables; + } + if (expression is VariableExpression) { + return [new VariableExpression(expression.variable)]; + } + if (expression is ComparisonExpression) { + throw new Exception("Cannot use ComparisonExpression for variables"); + } + return []; +} + +Expression negate(Expression expression, {bool positive: false}) { + if (expression is LogicExpression && expression.isOr) { + return new LogicExpression.and(expression.operands + .map((e) => negate(e, positive: !positive)) + .toList()); + } + if (expression is LogicExpression && expression.isAnd) { + return new LogicExpression.or(expression.operands + .map((e) => negate(e, positive: !positive)) + .toList()); + } + if (expression is ComparisonExpression) { + return new ComparisonExpression( + expression.left, expression.right, !expression.negate); + } + if (expression is VariableExpression) { + return new VariableExpression(expression.variable, + negate: !expression.negate); + } + return expression; +} + +// Convert ComparisonExpressions to VariableExpression to make sure looking +// we can se individual variables truthiness in the [TruthTableEnvironment]. +Expression _comparisonExpressionsToVariableExpressions(Expression expression) { + if (expression is LogicExpression) { + return new LogicExpression( + expression.op, + expression.operands + .map((exp) => _comparisonExpressionsToVariableExpressions(exp)) + .toList()); + } + if (expression is ComparisonExpression) { + return new VariableExpression( + new Variable( + expression.left.name + _comparisonToken + expression.right), + negate: expression.negate); + } + return expression; +} + +Expression _recoverComparisonExpressions(Expression expression) { + if (expression is LogicExpression) { + return new LogicExpression( + expression.op, + expression.operands + .map((exp) => _recoverComparisonExpressions(exp)) + .toList()); + } + if (expression is VariableExpression && + expression.variable.name.contains(_comparisonToken)) { + int tokenIndex = expression.variable.name.indexOf(_comparisonToken); + return new ComparisonExpression( + new Variable(expression.variable.name.substring(0, tokenIndex)), + expression.variable.name + .substring(tokenIndex + _comparisonToken.length), + expression.negate); + } + return expression; +} diff --git a/pkg/status_file/lib/src/expression.dart b/pkg/status_file/lib/src/expression.dart index 386464f8fbc..16a5bbdc367 100644 --- a/pkg/status_file/lib/src/expression.dart +++ b/pkg/status_file/lib/src/expression.dart @@ -89,10 +89,10 @@ class _Token { } /// A reference to a variable. -class _Variable { +class Variable { final String name; - _Variable(this.name); + Variable(this.name); String lookup(Environment environment) { var value = environment.lookUp(name); @@ -116,12 +116,12 @@ class _Variable { /// $variable == someValue /// ``` /// Negate the result if [negate] is true. -class _ComparisonExpression extends Expression { - final _Variable left; +class ComparisonExpression extends Expression { + final Variable left; final String right; final bool negate; - _ComparisonExpression(this.left, this.right, this.negate); + ComparisonExpression(this.left, this.right, this.negate); void validate(Environment environment, List errors) { environment.validate(left.name, right, errors); @@ -134,15 +134,15 @@ class _ComparisonExpression extends Expression { Expression normalize() { // Replace Boolean comparisons with a straight variable expression. if (right == "true") { - return new _VariableExpression(left, negate: negate); + return new VariableExpression(left, negate: negate); } else if (right == "false") { - return new _VariableExpression(left, negate: !negate); + return new VariableExpression(left, negate: !negate); } else { return this; } } - int _compareToMyType(_ComparisonExpression other) { + int _compareToMyType(ComparisonExpression other) { if (left.name != other.left.name) { return left.name.compareTo(other.left.name); } @@ -178,11 +178,11 @@ class _ComparisonExpression extends Expression { /// ``` /// $variable != true /// ``` -class _VariableExpression extends Expression { - final _Variable variable; +class VariableExpression extends Expression { + final Variable variable; final bool negate; - _VariableExpression(this.variable, {this.negate = false}); + VariableExpression(this.variable, {this.negate = false}); void validate(Environment environment, List errors) { // It must be a Boolean, so it should allow either Boolean value. @@ -195,7 +195,7 @@ class _VariableExpression extends Expression { /// Variable expressions are fine as they are. Expression normalize() => this; - int _compareToMyType(_VariableExpression other) { + int _compareToMyType(VariableExpression other) { if (variable.name != other.variable.name) { return variable.name.compareTo(other.variable.name); } @@ -209,13 +209,19 @@ class _VariableExpression extends Expression { } /// A logical `||` or `&&` expression. -class _LogicExpression extends Expression { +class LogicExpression extends Expression { /// The operator, `||` or `&&`. final String op; final List operands; - _LogicExpression(this.op, this.operands); + LogicExpression(this.op, this.operands); + + LogicExpression.and(this.operands) : op = _Token.and; + LogicExpression.or(this.operands) : op = _Token.or; + + bool get isAnd => op == _Token.and; + bool get isOr => op == _Token.or; void validate(Environment environment, List errors) { for (var operand in operands) { @@ -238,18 +244,18 @@ class _LogicExpression extends Expression { // order. // Recurse into the operands, sort them, and remove duplicates. - var normalized = new _LogicExpression( + var normalized = new LogicExpression( op, operands.map((operand) => operand.normalize()).toList()) .operands; normalized = flatten(normalized); var ordered = new SplayTreeSet.from(normalized).toList(); - return new _LogicExpression(op, ordered); + return new LogicExpression(op, ordered); } List flatten(List operands) { var newOperands = []; for (var operand in operands) { - if (operand is _LogicExpression && operand.op == op) { + if (operand is LogicExpression && operand.op == op) { newOperands.addAll(operand.operands); } else { newOperands.add(operand); @@ -258,7 +264,7 @@ class _LogicExpression extends Expression { return newOperands; } - int _compareToMyType(_LogicExpression other) { + int _compareToMyType(LogicExpression other) { // Put "&&" before "||". if (op != other.op) return op == _Token.and ? -1 : 1; @@ -280,7 +286,7 @@ class _LogicExpression extends Expression { String toString() { String parenthesize(Expression operand) { var result = operand.toString(); - if (op == "&&" && operand is _LogicExpression && operand.op == "||") { + if (isAnd && operand is LogicExpression && operand.isOr) { result = "($result)"; } @@ -316,7 +322,7 @@ class _ExpressionParser { if (operands.length == 1) return operands.single; - return new _LogicExpression(_Token.or, operands); + return new LogicExpression(_Token.or, operands); } Expression _parseAnd() { @@ -327,10 +333,12 @@ class _ExpressionParser { if (operands.length == 1) return operands.single; - return new _LogicExpression(_Token.and, operands); + return new LogicExpression(_Token.and, operands); } Expression _parsePrimary() { + // TODO(mkroghj,rnystrom) If DNF is enforced, the need to parse parenthesis + // should go away. Remove this when all section headers has dnf'ed. if (_scanner.match(_Token.leftParen)) { var value = _parseOr(); if (!_scanner.match(_Token.rightParen)) { @@ -357,7 +365,7 @@ class _ExpressionParser { "Expected identifier in expression, got ${_scanner.current}"); } - var left = new _Variable(_scanner.current); + var left = new Variable(_scanner.current); _scanner.advance(); if (!negate && @@ -371,9 +379,9 @@ class _ExpressionParser { } var right = _scanner.advance(); - return new _ComparisonExpression(left, right, isNotEquals); + return new ComparisonExpression(left, right, isNotEquals); } else { - return new _VariableExpression(left, negate: negate); + return new VariableExpression(left, negate: negate); } } } diff --git a/pkg/status_file/test/status_expression_dnf_test.dart b/pkg/status_file/test/status_expression_dnf_test.dart new file mode 100644 index 00000000000..475b6642efa --- /dev/null +++ b/pkg/status_file/test/status_expression_dnf_test.dart @@ -0,0 +1,72 @@ +// Copyright (c) 2017, the Dart project authors. Please see the AUTHORS file +// for details. All rights reserved. Use of this source code is governed by a +// BSD-style license that can be found in the LICENSE file. + +import "package:expect/expect.dart"; +import "package:status_file/src/expression.dart"; +import 'package:status_file/src/disjunctive.dart'; + +main() { + testDnf(); +} + +void shouldDnfTo(String input, String expected) { + var expression = Expression.parse(input); + Expect.equals(expected, toDisjunctiveNormalForm(expression).toString()); +} + +void shouldDnfToExact(String input, Expression expected) { + var expression = Expression.parse(input); + Expect.equals(expected, toDisjunctiveNormalForm(expression)); +} + +void shouldBeSame(String input) { + shouldDnfTo(input, input); +} + +void testDnf() { + shouldBeSame(r'$a'); + shouldBeSame(r'$a || $b'); + shouldBeSame(r'$a || $b && $c'); + shouldBeSame(r'$a && $b || $b && $c'); + shouldBeSame(r'$a && $b && $c'); + shouldBeSame(r'$a || $b || $c'); + shouldBeSame(r'!$a'); + shouldBeSame(r'!$a && $b'); + shouldBeSame(r'$a && !$b'); + shouldBeSame(r'$a && $b'); + shouldBeSame(r'!$a && !$b'); + + // Testing True. + shouldDnfToExact(r'$a || !$a', T); + shouldDnfToExact(r'!$a || !$b || $a && $b', T); + + // Testing False + shouldDnfToExact(r'$a && !$a', F); + shouldDnfToExact(r'($a || $b) && !$a && !$b', F); + + // Testing dnf and simple minimization (duplicates). + shouldDnfTo(r'$a && ($b || $c)', r'$a && $b || $a && $c'); + shouldDnfTo(r'($a || $b) && ($c || $d)', + r'$a && $c || $a && $d || $b && $c || $b && $d'); + + // Testing minimizing by complementation + // The following two examples can be found here: + // https://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm + shouldDnfTo( + r"$a && !$b && !$c && !$d || $a && !$b && !$c && $d || " + r"$a && !$b && $c && !$d || $a && !$b && $c && $d", + r"$a && !$b"); + + shouldDnfTo( + r"!$a && $b && !$c && !$d || $a && !$b && !$c && !$d || " + r"$a && !$b && $c && !$d || $a && !$b && $c && $d || $a && $b && !$c && !$d ||" + r" $a && $b && $c && $d || $a && !$b && !$c && $d || $a && $b && $c && !$d", + r"$a && !$b || $a && $c || $b && !$c && !$d"); + + // Test that an expression is converted to dnf and minified correctly. + shouldDnfTo(r'($a || $b) && ($a || $c)', r'$a || $b && $c'); + shouldDnfTo(r'(!$a || $b) && ($a || $b)', r'$b'); + shouldDnfTo(r'($a || $b || $c) && (!$a || !$b)', + r'$a && !$b || !$a && $b || !$b && $c'); +}