// Copyright (c) 2015, 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.

library dart2js.cps_ir.octagon;

import 'dart:collection';

/// For every variable in the constraint system, two [SignedVariable]s exist,
/// representing the positive and negative uses of the variable.
///
/// For instance, `v1 - v2` is represented as `v1 + (-v2)`, with -v2 being
/// a "negative use" of v2.
class SignedVariable {
  /// Negated version of this variable.
  SignedVariable _negated;
  SignedVariable get negated => _negated;

  /// Constraints that mention this signed variable.
  final List<Constraint> _constraints = <Constraint>[];

  static int _hashCount = 0;
  final int hashCode = (_hashCount = _hashCount + 1) & 0x0fffffff;

  SignedVariable._make() {
    _negated = new SignedVariable._makeTwin(this);
  }

  SignedVariable._makeTwin(this._negated);
}

/// A constraint of form `v1 + v2 <= k`.
class Constraint {
  final SignedVariable v1, v2;
  final int bound;

  Constraint(this.v1, this.v2, this.bound);
}

/// A system of constraints of form `v1 + v2 <= k`.
///
/// Constraints can be added and removed in stack-order.  The octagon will
/// always determine whether it is in a solvable state, but will otherwise
/// not optimize its internal representation.
///
/// There is currently no support for querying the upper and lower bounds
/// of a variable, (which can be used to approximate ternary constraints
/// `v1 + v2 + v3 <= k`), but it is something we could consider adding.
class Octagon {
  /// Number of constraints that have been added since the constraint system
  /// became unsolvable (including the constraint that made it unsolvable).
  ///
  /// This is well-defined because constraints are pushed/popped in stack order.
  int _unsolvableCounter = 0;

  /// True if the constraint system is unsolvable in its current state.
  ///
  /// It will remain unsolvable until a number of constraints have been popped.
  bool get isUnsolvable => _unsolvableCounter > 0;

  /// True if the constraint system is solvable in its current state.
  bool get isSolvable => _unsolvableCounter == 0;

  /// Make a new variable, optionally with known lower and upper bounds
  /// (both inclusive).
  ///
  /// The constraints generated for [min] and [max] are also expressible using
  /// [Constraint] objects, but the constraints added in [makeVariable] live
  /// outside the stack discipline (i.e. the bounds are never popped), which is
  /// useful when generating variables on-the-fly.
  SignedVariable makeVariable([int min, int max]) {
    SignedVariable v1 = new SignedVariable._make();
    if (min != null) {
      // v1 >= min   <==>   -v1 - v1 <= -2 * min
      v1.negated._constraints
          .add(new Constraint(v1.negated, v1.negated, -2 * min));
    }
    if (max != null) {
      // v1 <= max   <==>   v1 + v1 <= 2 * max
      v1._constraints.add(new Constraint(v1, v1, 2 * max));
    }
    return v1;
  }

  /// Add the constraint `v1 + v2 <= k`.
  ///
  /// The constraint should be removed again using [popConstraint].
  void pushConstraint(Constraint constraint) {
    if (_unsolvableCounter > 0 ||
        _unsolvableCounter == 0 && _checkUnsolvable(constraint)) {
      ++_unsolvableCounter;
    }
    constraint.v1._constraints.add(constraint);
    if (constraint.v1 != constraint.v2) {
      constraint.v2._constraints.add(constraint);
    }
  }

  /// Remove a constraint that was previously added with [pushConstraint].
  ///
  /// Constraints must be added and removed in stack-order.
  void popConstraint(Constraint constraint) {
    assert(constraint.v1._constraints.last == constraint);
    assert(constraint.v2._constraints.last == constraint);
    constraint.v1._constraints.removeLast();
    if (constraint.v1 != constraint.v2) {
      constraint.v2._constraints.removeLast();
    }
    if (_unsolvableCounter > 0) {
      --_unsolvableCounter;
    }
  }

  /// Return true if [constraint] would make the constraint system unsolvable.
  ///
  /// Assumes the system is currently solvable.
  bool _checkUnsolvable(Constraint constraint) {
    // Constraints are transitively composed like so:
    //    v1 + v2 <= k1
    //   -v2 + v3 <= k2
    // implies:
    //    v1 + v3 <= k1 + k2
    //
    // We construct a graph such that the tightest bound on `v1 + v3` is the
    // weight of the shortest path from `v1` to `-v3`.
    //
    // Every constraint `v1 + v2 <= k` gives rise to two edges:
    //     (v1) --k--> (-v2)
    //     (v2) --k--> (-v1)
    //
    // The system is unsolvable if and only if a negative-weight cycle exists
    // in this graph (this corresponds to a variable being less than itself).

    // Check if a negative-weight cycle would be created by adding [constraint].
    int length = _cycleLength(constraint);
    return length != null && length < 0;
  }

  /// Returns the length of the shortest simple cycle that would be created by
  /// adding [constraint] to the graph.
  ///
  /// Assumes there are no existing negative-weight cycles. The new cycle
  /// may have negative weight as [constraint] has not been added yet.
  int _cycleLength(Constraint constraint) {
    // Single-source shortest path using a FIFO queue.
    Queue<SignedVariable> worklist = new Queue<SignedVariable>();
    Map<SignedVariable, int> distance = {};
    void updateDistance(SignedVariable v, int newDistance) {
      int oldDistance = distance[v];
      if (oldDistance == null || oldDistance > newDistance) {
        distance[v] = newDistance;
        worklist.addLast(v);
      }
    }
    void iterateWorklist() {
      while (!worklist.isEmpty) {
        SignedVariable v1 = worklist.removeFirst();
        int distanceToV1 = distance[v1];
        for (Constraint c in v1._constraints) {
          SignedVariable v2 = c.v1 == v1 ? c.v2 : c.v1;
          updateDistance(v2.negated, distanceToV1 + c.bound);
        }
      }
    }
    // Two new edges will be added by the constraint `v1 + v2 <= k`:
    //
    //   A. (v1) --> (-v2)
    //   B. (v2) --> (-v1)
    //
    // We need to check for two kinds of cycles:
    //
    //   Using only A:       (-v2) --> (v1) --A--> (-v2)
    //   Using B and then A: (-v2) --> (v2) --B--> (-v1) --> (v1) --A--> (-v2)
    //
    // Because of the graph symmetry, cycles using only B or using A and then B
    // exist if and only if the corresponding cycle above exist, so there is no
    // need to check for those.
    //
    // Do a single-source shortest paths reaching out from (-v2).
    updateDistance(constraint.v2.negated, 0);
    iterateWorklist();
    if (constraint.v1 != constraint.v2) {
      int distanceToV2 = distance[constraint.v2];
      if (distanceToV2 != null) {
        // Allow one use of the B edge.
        // This must be done outside fixpoint iteration as an infinite loop
        // would arise when an negative-weight cycle using only B exists.
        updateDistance(constraint.v1.negated, distanceToV2 + constraint.bound);
        iterateWorklist();
      }
    }
    // Get the distance to (v1) and check if the A edge would complete a cycle.
    int distanceToV1 = distance[constraint.v1];
    if (distanceToV1 == null) return null;
    return distanceToV1 + constraint.bound;
  }
}