mcs/class/referencesource/System.Data.Entity/System/Data/Common/Utils/Boolean/Solver.cs

   1 //---------------------------------------------------------------------
   2 // <copyright file="Solver.cs" company="Microsoft">
   3 //      Copyright (c) Microsoft Corporation.  All rights reserved.
   4 // </copyright>
   5 //
   6 // @owner [....]
   7 // @backupOwner [....]
   8 //---------------------------------------------------------------------
   9
  10 using System;
  11 using System.Collections.Generic;
  12 using System.Linq;
  13
  14 namespace System.Data.Common.Utils.Boolean
  15 {
  16     using IfThenElseKey = Triple<Vertex, Vertex, Vertex>;
  17     using System.Diagnostics;
  18
  19     /// <summary>
  20     /// Supports construction of canonical Boolean expressions as Reduced Ordered
  21     /// Boolean Decision Diagrams (ROBDD). As a side effect, supports simplification and SAT:
  22     ///
  23     /// - The canonical form of a valid expression is Solver.One
  24     /// - The canonical form of an unsatisfiable expression is Solver.Zero
  25     /// - The lack of redundancy in the trees allows us to produce compact representations
  26     /// of expressions
  27     ///
  28     /// Any method taking a Vertex argument requires that the argument is either
  29     /// a 'sink' (Solver.One or Solver.Zero) or generated by this Solver instance.
  30     /// </summary>
  31     internal sealed class Solver
  32     {
  33         #region Fields
  34         readonly Dictionary<IfThenElseKey, Vertex> _computedIfThenElseValues =
  35             new Dictionary<IfThenElseKey, Vertex>();
  36         readonly Dictionary<Vertex, Vertex> _knownVertices =
  37             new Dictionary<Vertex, Vertex>(VertexValueComparer.Instance);
  38         int _variableCount;
  39         // a standard Boolean variable has children '1' and '0'
  40         internal readonly static Vertex[] BooleanVariableChildren = new Vertex[] { Vertex.One, Vertex.Zero };
  41         #endregion
  42
  43         #region Expression factory methods
  44         internal int CreateVariable()
  45         {
  46             return ++_variableCount;
  47         }
  48
  49         internal Vertex Not(Vertex vertex)
  50         {
  51             // Not(v) iff. 'if v then 0 else 1'
  52             return IfThenElse(vertex, Vertex.Zero, Vertex.One);
  53         }
  54
  55         internal Vertex And(IEnumerable<Vertex> children)
  56         {
  57             // assuming input vertices v1, v2, ..., vn:
  58             //
  59             //  v1
  60             //  0|\1
  61             //   |  v2
  62             //   |/0  \1
  63             //   |    ...
  64             //   |  /0  \1
  65             //   |        vn
  66             //   |     /0   \1
  67             //   FALSE       TRUE
  68             //
  69             // order the children to minimize churn when building tree bottom up
  70             return children
  71                 .OrderByDescending(child => child.Variable)
  72                 .Aggregate(Vertex.One, (left, right) => IfThenElse(left, right, Vertex.Zero));
  73         }
  74
  75         internal Vertex And(Vertex left, Vertex right)
  76         {
  77             // left AND right iff. if 'left' then 'right' else '0'
  78             return IfThenElse(left, right, Vertex.Zero);
  79         }
  80
  81         internal Vertex Or(IEnumerable<Vertex> children)
  82         {
  83             // assuming input vertices v1, v2, ..., vn:
  84             //
  85             //  v1
  86             //  1|\0
  87             //   |  v2
  88             //   |/1  \0
  89             //   |    ...
  90             //   |  /1  \0
  91             //   |        vn
  92             //   |     /1   \0
  93             //   TRUE       FALSE
  94             //
  95             // order the children to minimize churn when building tree bottom up
  96             return children
  97                 .OrderByDescending(child => child.Variable)
  98                 .Aggregate(Vertex.Zero, (left, right) => IfThenElse(left, Vertex.One, right));
  99         }
 100
 101         /// <summary>
 102         /// Creates a leaf vertex; all children must be sinks
 103         /// </summary>
 104         internal Vertex CreateLeafVertex(int variable, Vertex[] children)
 105         {
 106             Debug.Assert(null != children, "children must be specified");
 107             Debug.Assert(2 <= children.Length, "must be at least 2 children");
 108             Debug.Assert(children.All(child => child != null), "children must not be null");
 109             Debug.Assert(children.All(child => child.IsSink()), "children must be sinks");
 110             Debug.Assert(variable <= _variableCount, "variable out of range");
 111
 112             return GetUniqueVertex(variable, children);
 113         }
 114         #endregion
 115
 116         #region Private helper methods
 117         /// <summary>
 118         /// Returns a Vertex with the given configuration. If this configuration
 119         /// is known, returns the existing vertex. Otherwise, a new
 120         /// vertex is created. This ensures the vertex is unique in the context
 121         /// of this solver.
 122         /// </summary>
 123         private Vertex GetUniqueVertex(int variable, Vertex[] children)
 124         {
 125             AssertVerticesValid(children);
 126
 127             Vertex result = new Vertex(variable, children);
 128
 129             // see if we know this vertex already
 130             Vertex canonicalResult;
 131             if (_knownVertices.TryGetValue(result, out canonicalResult))
 132             {
 133                 return canonicalResult;
 134             }
 135
 136             // remember the vertex (because it came first, it's canonical)
 137             _knownVertices.Add(result, result);
 138
 139             return result;
 140         }
 141
 142         /// <summary>
 143         /// Composes the given vertices to produce a new ROBDD.
 144         /// </summary>
 145         private Vertex IfThenElse(Vertex condition, Vertex then, Vertex @else)
 146         {
 147             AssertVertexValid(condition);
 148             AssertVertexValid(then);
 149             AssertVertexValid(@else);
 150
 151             // check for terminal conditions in the recursion
 152             if (condition.IsOne())
 153             {
 154                 // if '1' then 'then' else '@else' iff. 'then'
 155                 return then;
 156             }
 157             if (condition.IsZero())
 158             {
 159                 // if '0' then 'then' else '@else' iff. '@else'
 160                 return @else;
 161             }
 162             if (then.IsOne() && @else.IsZero())
 163             {
 164                 // if 'condition' then '1' else '0' iff. condition
 165                 return condition;
 166             }
 167             if (then.Equals(@else))
 168             {
 169                 // if 'condition' then 'x' else 'x' iff. x
 170                 return then;
 171             }
 172
 173             Vertex result;
 174             IfThenElseKey key = new IfThenElseKey(condition, then, @else);
 175
 176             // check if we've already computed this result
 177             if (_computedIfThenElseValues.TryGetValue(key, out result))
 178             {
 179                 return result;
 180             }
 181
 182             int topVariableDomainCount;
 183             int topVariable = DetermineTopVariable(condition, then, @else, out topVariableDomainCount);
 184
 185             // Recursively compute the new BDD node
 186             // Note that we preserve the 'ordered' invariant since the child nodes
 187             // cannot contain references to variables < topVariable, and
 188             // the topVariable is eliminated from the children through
 189             // the call to EvaluateFor.
 190             Vertex[] resultCases = new Vertex[topVariableDomainCount];
 191             bool allResultsEqual = true;
 192             for (int i = 0; i < topVariableDomainCount; i++)
 193             {
 194                 resultCases[i] = IfThenElse(
 195                     EvaluateFor(condition, topVariable, i),
 196                     EvaluateFor(then, topVariable, i),
 197                     EvaluateFor(@else, topVariable, i));
 198
 199                 if (i > 0 && // first vertex is equivalent to itself
 200                     allResultsEqual && // we've already found a mismatch
 201                     !resultCases[i].Equals(resultCases[0]))
 202                 {
 203                     allResultsEqual = false;
 204                 }
 205             }
 206
 207             // if the results are identical, any may be returned
 208             if (allResultsEqual)
 209             {
 210                 return resultCases[0];
 211             }
 212
 213             // create new vertex
 214             result = GetUniqueVertex(topVariable, resultCases);
 215
 216             // remember result so that we don't try to compute this if-then-else pattern again
 217             _computedIfThenElseValues.Add(key, result);
 218
 219             return result;
 220         }
 221
 222         /// <summary>
 223         /// Given parts of an if-then-else statement, determines the top variable (nearest
 224         /// root). Used to determine which variable forms the root of a composed Vertex.
 225         /// </summary>
 226         private static int DetermineTopVariable(Vertex condition, Vertex then, Vertex @else, out int topVariableDomainCount)
 227         {
 228             int topVariable;
 229             if (condition.Variable < then.Variable)
 230             {
 231                 topVariable = condition.Variable;
 232                 topVariableDomainCount = condition.Children.Length;
 233             }
 234             else
 235             {
 236                 topVariable = then.Variable;
 237                 topVariableDomainCount = then.Children.Length;
 238             }
 239             if (@else.Variable < topVariable)
 240             {
 241                 topVariable = @else.Variable;
 242                 topVariableDomainCount = @else.Children.Length;
 243             }
 244             return topVariable;
 245         }
 246
 247         /// <summary>
 248         /// Returns 'vertex' evaluated for the given value of 'variable'. Requires that
 249         /// the variable is less than or equal to vertex.Variable.
 250         /// </summary>
 251         private static Vertex EvaluateFor(Vertex vertex, int variable, int variableAssigment)
 252         {
 253             if (variable < vertex.Variable)
 254             {
 255                 // If the variable we're setting is less than the vertex variable, the
 256                 // the Vertex 'ordered' invariant ensures that the vertex contains no reference
 257                 // to that variable. Binding the variable is therefore a no-op.
 258                 return vertex;
 259             }
 260             Debug.Assert(variable == vertex.Variable,
 261                 "variable must be less than or equal to vertex.Variable");
 262
 263             // If the 'vertex' is conditioned on the given 'variable', the children
 264             // represent the decompositions of the function for various assignments
 265             // to that variable.
 266             Debug.Assert(variableAssigment < vertex.Children.Length, "variable assignment out of range");
 267             return vertex.Children[variableAssigment];
 268         }
 269
 270         /// <summary>
 271         /// Checks requirements for vertices.
 272         /// </summary>
 273         [Conditional("DEBUG")]
 274         private void AssertVerticesValid(IEnumerable<Vertex> vertices)
 275         {
 276             Debug.Assert(null != vertices);
 277             foreach (Vertex vertex in vertices)
 278             {
 279                 AssertVertexValid(vertex);
 280             }
 281         }
 282
 283         /// <summary>
 284         /// Checks requirements for a vertex argument (must not be null, and must be in scope
 285         /// for this solver)
 286         /// </summary>
 287         [Conditional("DEBUG")]
 288         private void AssertVertexValid(Vertex vertex)
 289         {
 290             Debug.Assert(vertex != null, "vertex must not be null");
 291
 292             // sinks are ok
 293             if (!vertex.IsSink())
 294             {
 295                 // so are vertices created by this solver
 296                 Vertex comparisonVertex;
 297                 Debug.Assert(_knownVertices.TryGetValue(vertex, out comparisonVertex) &&
 298                     comparisonVertex.Equals(vertex), "vertex not created by this solver");
 299             }
 300         }
 301         #endregion
 302
 303         /// <summary>
 304         /// Supports value comparison of vertices. In general, we use reference comparison
 305         /// since the Solver ensures a single instance of each canonical Vertex. The Solver
 306         /// needs this comparer to ensure a single instance of each canonical Vertex though...
 307         /// </summary>
 308         private class VertexValueComparer : IEqualityComparer<Vertex>
 309         {
 310             private VertexValueComparer() { }
 311
 312             internal static readonly VertexValueComparer Instance = new VertexValueComparer();
 313
 314             public bool Equals(Vertex x, Vertex y)
 315             {
 316                 if (x.IsSink())
 317                 {
 318                     // [....] nodes '1' and '0' each have one static instance; use reference
 319                     return x.Equals(y);
 320                 }
 321
 322                 if (x.Variable != y.Variable ||
 323                     x.Children.Length != y.Children.Length)
 324                 {
 325                     return false;
 326                 }
 327                 for (int i = 0; i < x.Children.Length; i++)
 328                 {
 329                     // use reference comparison for the children (they must be
 330                     // canonical already)
 331                     if (!x.Children[i].Equals(y.Children[i]))
 332                     {
 333                         return false;
 334                     }
 335                 }
 336                 return true;
 337             }
 338
 339             public int GetHashCode(Vertex vertex)
 340             {
 341                 // [....] nodes '1' and '0' each have one static instance; use reference
 342                 if (vertex.IsSink())
 343                 {
 344                     return vertex.GetHashCode();
 345                 }
 346
 347                 Debug.Assert(2 <= vertex.Children.Length, "internal vertices must have at least 2 children");
 348                 unchecked
 349                 {
 350                     return ((vertex.Children[0].GetHashCode() << 5) + 1) + vertex.Children[1].GetHashCode();
 351                 }
 352             }
 353         }
 354     }
 355
 356     /// <summary>
 357     /// Record structure containing three values.
 358     /// </summary>
 359     struct Triple<T1, T2, T3> : IEquatable<Triple<T1, T2, T3>>
 360         where T1 : IEquatable<T1>
 361         where T2 : IEquatable<T2>
 362         where T3 : IEquatable<T3>
 363     {
 364         readonly T1 _value1;
 365         readonly T2 _value2;
 366         readonly T3 _value3;
 367
 368         internal Triple(T1 value1, T2 value2, T3 value3)
 369         {
 370             Debug.Assert(null != (object)value1, "null key element");
 371             Debug.Assert(null != (object)value2, "null key element");
 372             Debug.Assert(null != (object)value3, "null key element");
 373             _value1 = value1;
 374             _value2 = value2;
 375             _value3 = value3;
 376         }
 377
 378         public bool Equals(Triple<T1, T2, T3> other)
 379         {
 380             return _value1.Equals(other._value1) &&
 381                 _value2.Equals(other._value2) &&
 382                 _value3.Equals(other._value3);
 383         }
 384
 385         public override bool Equals(object obj)
 386         {
 387             Debug.Fail("used typed Equals");
 388             return base.Equals(obj);
 389         }
 390
 391         public override int GetHashCode()
 392         {
 393             return _value1.GetHashCode() ^
 394                 _value2.GetHashCode() ^
 395                 _value3.GetHashCode();
 396         }
 397     }
 398 }