IntegerExpressions.cs

Go to the documentation of this file.

// 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