IntegerExpressions.cs

// Copyright 2010-2018 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

namespace Google.OrTools.Sat
{
  using System;
  using System.Collections.Generic;
  using Google.OrTools.Util;

  // Helpers.

  // IntVar[] helper class.
  public static class IntVarArrayHelper
  {
    [Obsolete("This Sum method is deprecated, please use LinearExpr.Sum() instead.")]
    public static LinearExpr Sum(this IntVar[] vars)
    {
      return LinearExpr.Sum(vars);
    }
    [Obsolete("This ScalProd method is deprecated, please use LinearExpr.ScalProd() instead.")]
    public static LinearExpr ScalProd(this IntVar[] vars, int[] coeffs)
    {
      return LinearExpr.ScalProd(vars, coeffs);
    }
    [Obsolete("This ScalProd method is deprecated, please use LinearExpr.ScalProd() instead.")]
    public static LinearExpr ScalProd(this IntVar[] vars, long[] coeffs)
    {
      return LinearExpr.ScalProd(vars, coeffs);
    }
  }

  public interface ILiteral
  {
    ILiteral Not();
    int GetIndex();
  }

  // Holds a linear expression.
  public class LinearExpr
  {

    public static LinearExpr Sum(IEnumerable<IntVar> vars)
    {
      return new SumArray(vars);
    }

    public static LinearExpr Sum(IEnumerable<LinearExpr> exprs)
    {
      return new SumArray(exprs);
    }

    public static LinearExpr ScalProd(IEnumerable<IntVar> vars, IEnumerable<int> coeffs)
    {
      return new SumArray(vars, coeffs);
    }

    public static LinearExpr ScalProd(IEnumerable<IntVar> vars, IEnumerable<long> coeffs)
    {
      return new SumArray(vars, coeffs);
    }

    public static LinearExpr Term(IntVar var, long coeff)
    {
      return Prod(var, coeff);
    }

    public int Index
    {
      get { return GetIndex(); }
    }

    public virtual int GetIndex()
    {
      throw new NotImplementedException();
    }

    public virtual string ShortString()
    {
      return ToString();
    }

    public static LinearExpr operator +(LinearExpr a, LinearExpr b)
    {
      return new SumArray(a, b);
    }

    public static LinearExpr operator +(LinearExpr a, long v)
    {
      return new SumArray(a, v);
    }

    public static LinearExpr operator +(long v, LinearExpr a)
    {
      return new SumArray(a, v);
    }

    public static LinearExpr operator -(LinearExpr a, LinearExpr b)
    {
      return new SumArray(a, Prod(b, -1));
    }

    public static LinearExpr operator -(LinearExpr a, long v)
    {
      return new SumArray(a, -v);
    }

    public static LinearExpr operator -(long v, LinearExpr a)
    {
      return new SumArray(Prod(a, -1), v);
    }

    public static LinearExpr operator *(LinearExpr a, long v)
    {
      return Prod(a, v);
    }

    public static LinearExpr operator *(long v, LinearExpr a)
    {
      return Prod(a, v);
    }

    public static LinearExpr operator -(LinearExpr a)
    {
      return Prod(a, -1);
    }

    public static BoundedLinearExpression operator ==(LinearExpr a, LinearExpr b)
    {
      return new BoundedLinearExpression(a, b, true);
    }

    public static BoundedLinearExpression operator !=(LinearExpr a, LinearExpr b)
    {
      return new BoundedLinearExpression(a, b, false);
    }

    public static BoundedLinearExpression operator ==(LinearExpr a, long v)
    {
      return new BoundedLinearExpression(a, v, true);
    }

    public static BoundedLinearExpression operator !=(LinearExpr a, long v)
    {
      return new BoundedLinearExpression(a, v, false);
    }

    public static BoundedLinearExpression operator >=(LinearExpr a, long v)
    {
      return new BoundedLinearExpression(v, a, Int64.MaxValue);
    }

    public static BoundedLinearExpression operator >=(long v, LinearExpr a)
    {
      return a <= v;
    }

    public static BoundedLinearExpression operator >(LinearExpr a, long v)
    {
      return new BoundedLinearExpression(v + 1, a, Int64.MaxValue);
    }

    public static BoundedLinearExpression operator >(long v, LinearExpr a)
    {
      return a < v;
    }

    public static BoundedLinearExpression operator <=(LinearExpr a, long v)
    {
      return new BoundedLinearExpression(Int64.MinValue, a, v);
    }

    public static BoundedLinearExpression operator <=(long v, LinearExpr a)
    {
      return a >= v;
    }

    public static BoundedLinearExpression operator <(LinearExpr a, long v)
    {
      return new BoundedLinearExpression(Int64.MinValue, a, v - 1);
    }

    public static BoundedLinearExpression operator <(long v, LinearExpr a)
    {
      return a > v;
    }

    public static BoundedLinearExpression operator >=(LinearExpr a, LinearExpr b)
    {
      return new BoundedLinearExpression(0, a - b, Int64.MaxValue);
    }

    public static BoundedLinearExpression operator >(LinearExpr a, LinearExpr b)
    {
      return new BoundedLinearExpression(1, a - b, Int64.MaxValue);
    }

    public static BoundedLinearExpression operator <=(LinearExpr a, LinearExpr b)
    {
      return new BoundedLinearExpression(Int64.MinValue, a - b, 0);
    }

    public static BoundedLinearExpression operator <(LinearExpr a, LinearExpr b)
    {
      return new BoundedLinearExpression(Int64.MinValue, a - b, -1);
    }

    public static LinearExpr Prod(LinearExpr e, long v)
    {
      if (v == 1)
      {
        return e;
      }
      else if (e is ProductCst)
      {
        ProductCst p = (ProductCst)e;
        return new ProductCst(p.Expr, p.Coeff * v);
      }
      else
      {
        return new ProductCst(e, v);
      }
    }

    public static long GetVarValueMap(LinearExpr e,
                                      long initial_coeff,
                                      Dictionary<IntVar, long> dict)
    {
      List<LinearExpr> exprs = new List<LinearExpr>();
      List<long> coeffs = new List<long>();
      if ((Object)e != null)
      {
        exprs.Add(e);
        coeffs.Add(initial_coeff);
      }
      long constant = 0;

      while (exprs.Count > 0)
      {
        LinearExpr expr = exprs[0];
        exprs.RemoveAt(0);
        long coeff = coeffs[0];
        coeffs.RemoveAt(0);
        if (coeff == 0 || (Object)expr == null) continue;

        if (expr is ProductCst)
        {
          ProductCst p = (ProductCst)expr;
          if (p.Coeff != 0)
          {
            exprs.Add(p.Expr);
            coeffs.Add(p.Coeff * coeff);
          }
        }
        else if (expr is SumArray)
        {
          SumArray a = (SumArray)expr;
          constant += coeff * a.Constant;
          foreach (LinearExpr sub in a.Expressions)
          {
            if (sub is IntVar)
            {
              IntVar i = (IntVar)sub;
              if (dict.ContainsKey(i))
              {
                dict[i] += coeff;
              }
              else
              {
                dict.Add(i, coeff);
              }
            }
            else if (sub is ProductCst && ((ProductCst)sub).Expr is IntVar)
            {
              ProductCst sub_prod = (ProductCst)sub;
              IntVar i = (IntVar)sub_prod.Expr;
              long sub_coeff = sub_prod.Coeff;

              if (dict.ContainsKey(i))
              {
                dict[i] += coeff * sub_coeff;
              }
              else
              {
                dict.Add(i, coeff * sub_coeff);
              }
            }
            else
            {
              exprs.Add(sub);
              coeffs.Add(coeff);
            }
          }
        }
        else if (expr is IntVar)
        {
          IntVar i = (IntVar)expr;
          if (dict.ContainsKey(i))
          {
            dict[i] += coeff;
          }
          else
          {
            dict.Add(i, coeff);
          }
        }
        else if (expr is NotBooleanVariable)
        {
          IntVar i = ((NotBooleanVariable)expr).NotVar();
          if (dict.ContainsKey(i))
          {
            dict[i] -= coeff;
          }
          else
          {
            dict.Add(i, -coeff);
          }
          constant += coeff;
        }
        else
        {
          throw new ArgumentException("Cannot interpret '" + expr.ToString() +
                                      "' in an integer expression");
        }
      }
      return constant;
    }
  }

  public class ProductCst : LinearExpr
  {
    public ProductCst(LinearExpr e, long v)
    {
      expr_ = e;
      coeff_ = v;
    }

    public LinearExpr Expr
    {
      get { return expr_; }
    }

    public long Coeff
    {
      get { return coeff_; }
    }

    private LinearExpr expr_;
    private long coeff_;

  }

  public class SumArray : LinearExpr
  {
    public SumArray(LinearExpr a, LinearExpr b)
    {
      expressions_ = new List<LinearExpr>();
      AddExpr(a);
      AddExpr(b);
      constant_ = 0L;
    }

    public SumArray(LinearExpr a, long b)
    {
      expressions_ = new List<LinearExpr>();
      AddExpr(a);
      constant_ = b;
    }

    public SumArray(IEnumerable<LinearExpr> exprs)
    {
      expressions_ = new List<LinearExpr>(exprs);
      constant_ = 0L;
    }

    public SumArray(IEnumerable<IntVar> vars)
    {
      expressions_ = new List<LinearExpr>(vars);
      constant_ = 0L;
    }

    public SumArray(IntVar[] vars, long[] coeffs)
    {
      expressions_ = new List<LinearExpr>(vars.Length);
      for (int i = 0; i < vars.Length; ++i)
      {
        AddExpr(Prod(vars[i], coeffs[i]));
      }
      constant_ = 0L;
    }
    public SumArray(IEnumerable<IntVar> vars, IEnumerable<long> coeffs)
    {
      List<IntVar> tmp_vars = new List<IntVar>();
      foreach (IntVar v in vars)
      {
        tmp_vars.Add(v);
      }
      List<long> tmp_coeffs = new List<long>();
      foreach (long c in coeffs)
      {
        tmp_coeffs.Add(c);
      }
      if (tmp_vars.Count != tmp_coeffs.Count)
      {
        throw new ArgumentException(
          "in SumArray(vars, coeffs), the two lists do not have the same length");
      }
      IntVar[] flat_vars = tmp_vars.ToArray();
      long[] flat_coeffs = tmp_coeffs.ToArray();
      expressions_ = new List<LinearExpr>(flat_vars.Length);
      for (int i = 0; i < flat_vars.Length; ++i)
      {
        expressions_.Add(Prod(flat_vars[i], flat_coeffs[i]));
      }
      constant_ = 0L;
    }

    public SumArray(IEnumerable<IntVar> vars, IEnumerable<int> coeffs)
    {
      List<IntVar> tmp_vars = new List<IntVar>();
      foreach (IntVar v in vars)
      {
        tmp_vars.Add(v);
      }
      List<long> tmp_coeffs = new List<long>();
      foreach (int c in coeffs)
      {
        tmp_coeffs.Add(c);
      }
      if (tmp_vars.Count != tmp_coeffs.Count)
      {
        throw new ArgumentException(
          "in SumArray(vars, coeffs), the two lists do not have the same length");
      }
      IntVar[] flat_vars = tmp_vars.ToArray();
      long[] flat_coeffs = tmp_coeffs.ToArray();
      expressions_ = new List<LinearExpr>(flat_vars.Length);
      for (int i = 0; i < flat_vars.Length; ++i)
      {
        expressions_.Add(Prod(flat_vars[i], flat_coeffs[i]));
      }
      constant_ = 0L;
    }

    public void AddExpr(LinearExpr expr)
    {
      if ((Object)expr != null)
      {
        expressions_.Add(expr);
      }
    }

    public List<LinearExpr> Expressions
    {
      get { return expressions_; }
    }

    public long Constant
    {
      get { return constant_; }
    }

    public override string ShortString()
    {
      return String.Format("({0})", ToString());
    }

    public override string ToString()
    {
      string result = "";
      foreach (LinearExpr expr in expressions_)
      {
        if ((Object)expr == null) continue;
        if (!String.IsNullOrEmpty(result))
        {
          result += String.Format(" + ");
        }

        result += expr.ShortString();
      }
      return result;
    }

    private List<LinearExpr> expressions_;
    private long constant_;
  }

  public class IntVar : LinearExpr, ILiteral
  {
    public IntVar(CpModelProto model, Domain domain, string name)
    {
      model_ = model;
      index_ = model.Variables.Count;
      var_ = new IntegerVariableProto();
      var_.Name = name;
      var_.Domain.Add(domain.FlattenedIntervals());
      model.Variables.Add(var_);
      negation_ = null;
    }

    public int Index
    {
      get { return index_; }
    }

    public override int GetIndex()
    {
      return index_;
    }

    public IntegerVariableProto Proto
    {
      get { return var_; }
      set { var_ = value; }
    }

    public Domain Domain
    {
      get { return SatHelper.VariableDomain(var_); }
    }

    public override string ToString()
    {
      return var_.ToString();
    }

    public override string ShortString()
    {
      if (var_.Name != null)
      {
        return var_.Name;
      }
      else
      {
        return var_.ToString();
      }
    }

    public string Name()
    {
      return var_.Name;
    }

    public ILiteral Not()
    {
      foreach (long b in var_.Domain)
      {
        if (b < 0 || b > 1)
        {
          throw new ArgumentException(
              "Cannot call Not() on a non boolean variable");
        }
      }
      if (negation_ == null)
      {
        negation_ = new NotBooleanVariable(this);
      }
      return negation_;
    }

    private CpModelProto model_;
    private int index_;
    private List<long> bounds_;
    private IntegerVariableProto var_;
    private NotBooleanVariable negation_;
  }

  public class NotBooleanVariable : LinearExpr, ILiteral
  {
    public NotBooleanVariable(IntVar boolvar)
    {
      boolvar_ = boolvar;
    }

    public override int GetIndex()
    {
      return -boolvar_.Index - 1;
    }

    public ILiteral Not()
    {
      return boolvar_;
    }

    public IntVar NotVar()
    {
      return boolvar_;
    }

    public override string ShortString()
    {
      return String.Format("Not({0})", boolvar_.ShortString());
    }

    private IntVar boolvar_;
  }

  public class BoundedLinearExpression
  {
    public enum Type
    {
      BoundExpression,
      VarEqVar,
      VarDiffVar,
      VarEqCst,
      VarDiffCst,
    }

    public BoundedLinearExpression(long lb, LinearExpr expr, long ub)
    {
      left_ = expr;
      right_ = null;
      lb_ = lb;
      ub_ = ub;
      type_ = Type.BoundExpression;
    }

    public BoundedLinearExpression(LinearExpr left, LinearExpr right,
                                  bool equality)
    {
      left_ = left;
      right_ = right;
      lb_ = 0;
      ub_ = 0;
      type_ = equality ? Type.VarEqVar : Type.VarDiffVar;
    }

    public BoundedLinearExpression(LinearExpr left, long v, bool equality)
    {
      left_ = left;
      right_ = null;
      lb_ = v;
      ub_ = 0;
      type_ = equality ? Type.VarEqCst : Type.VarDiffCst;
    }

    bool IsTrue()
    {
      if (type_ == Type.VarEqVar)
      {
        return (object)left_ == (object)right_;
      }
      else if (type_ == Type.VarDiffVar)
      {
        return (object)left_ != (object)right_;
      }
      return false;
    }

    public static bool operator true(BoundedLinearExpression bie)
    {
      return bie.IsTrue();
    }

    public static bool operator false(BoundedLinearExpression bie)
    {
      return !bie.IsTrue();
    }

    public override string ToString()
    {
      switch (type_)
      {
        case Type.BoundExpression:
          return String.Format("{0} <= {1} <= {2}", lb_, left_, ub_);
        case Type.VarEqVar:
          return String.Format("{0} == {1}", left_, right_);
        case Type.VarDiffVar:
          return String.Format("{0} != {1}", left_, right_);
        case Type.VarEqCst:
          return String.Format("{0} == {1}", left_, lb_);
        case Type.VarDiffCst:
          return String.Format("{0} != {1}", left_, lb_);
        default:
          throw new ArgumentException("Wrong mode in BoundedLinearExpression.");
      }
    }

    public static BoundedLinearExpression operator <=(BoundedLinearExpression a,
                                                     long v)
    {
      if (a.CtType != Type.BoundExpression || a.Ub != Int64.MaxValue)
      {
        throw new ArgumentException(
            "Operator <= not supported for this BoundedLinearExpression");
      }
      return new BoundedLinearExpression(a.Lb, a.Left, v);
    }

    public static BoundedLinearExpression operator <(BoundedLinearExpression a,
                                                    long v)
    {
      if (a.CtType != Type.BoundExpression || a.Ub != Int64.MaxValue)
      {
        throw new ArgumentException(
            "Operator < not supported for this BoundedLinearExpression");
      }
      return new BoundedLinearExpression(a.Lb, a.Left, v - 1);
    }

    public static BoundedLinearExpression operator >=(BoundedLinearExpression a,
                                                     long v)
    {
      if (a.CtType != Type.BoundExpression || a.Lb != Int64.MinValue)
      {
        throw new ArgumentException(
            "Operator >= not supported for this BoundedLinearExpression");
      }
      return new BoundedLinearExpression(v, a.Left, a.Ub);
    }

    public static BoundedLinearExpression operator >(BoundedLinearExpression a,
                                                    long v)
    {
      if (a.CtType != Type.BoundExpression || a.Lb != Int64.MinValue)
      {
        throw new ArgumentException(
            "Operator < not supported for this BoundedLinearExpression");
      }
      return new BoundedLinearExpression(v + 1, a.Left, a.Ub);
    }

    public LinearExpr Left
    {
      get { return left_; }
    }

    public LinearExpr Right
    {
      get { return right_; }
    }

    public long Lb
    {
      get { return lb_; }
    }

    public long Ub
    {
      get { return ub_; }
    }

    public Type CtType
    {
      get { return type_; }
    }

    private LinearExpr left_;
    private LinearExpr right_;
    private long lb_;
    private long ub_;
    private Type type_;
  }

}  // namespace Google.OrTools.Sat