﻿ Solver.cs
 File: System\Data\Common\Utils\Boolean\Solver.cs Project: ndp\fx\src\DataEntity\System.Data.Entity.csproj (System.Data.Entity)
 ```//--------------------------------------------------------------------- // // Copyright (c) Microsoft Corporation. All rights reserved. // // // @owner Microsoft // @backupOwner Microsoft //--------------------------------------------------------------------- using System; using System.Collections.Generic; using System.Linq; namespace System.Data.Common.Utils.Boolean { using IfThenElseKey = Triple; using System.Diagnostics; /// /// Supports construction of canonical Boolean expressions as Reduced Ordered /// Boolean Decision Diagrams (ROBDD). As a side effect, supports simplification and SAT: /// /// - The canonical form of a valid expression is Solver.One /// - The canonical form of an unsatisfiable expression is Solver.Zero /// - The lack of redundancy in the trees allows us to produce compact representations /// of expressions /// /// Any method taking a Vertex argument requires that the argument is either /// a 'sink' (Solver.One or Solver.Zero) or generated by this Solver instance. /// internal sealed class Solver { #region Fields readonly Dictionary _computedIfThenElseValues = new Dictionary(); readonly Dictionary _knownVertices = new Dictionary(VertexValueComparer.Instance); int _variableCount; // a standard Boolean variable has children '1' and '0' internal readonly static Vertex[] BooleanVariableChildren = new Vertex[] { Vertex.One, Vertex.Zero }; #endregion #region Expression factory methods internal int CreateVariable() { return ++_variableCount; } internal Vertex Not(Vertex vertex) { // Not(v) iff. 'if v then 0 else 1' return IfThenElse(vertex, Vertex.Zero, Vertex.One); } internal Vertex And(IEnumerable children) { // assuming input vertices v1, v2, ..., vn: // // v1 // 0|\1 // | v2 // |/0 \1 // | ... // | /0 \1 // | vn // | /0 \1 // FALSE TRUE // // order the children to minimize churn when building tree bottom up return children .OrderByDescending(child => child.Variable) .Aggregate(Vertex.One, (left, right) => IfThenElse(left, right, Vertex.Zero)); } internal Vertex And(Vertex left, Vertex right) { // left AND right iff. if 'left' then 'right' else '0' return IfThenElse(left, right, Vertex.Zero); } internal Vertex Or(IEnumerable children) { // assuming input vertices v1, v2, ..., vn: // // v1 // 1|\0 // | v2 // |/1 \0 // | ... // | /1 \0 // | vn // | /1 \0 // TRUE FALSE // // order the children to minimize churn when building tree bottom up return children .OrderByDescending(child => child.Variable) .Aggregate(Vertex.Zero, (left, right) => IfThenElse(left, Vertex.One, right)); } /// /// Creates a leaf vertex; all children must be sinks /// internal Vertex CreateLeafVertex(int variable, Vertex[] children) { Debug.Assert(null != children, "children must be specified"); Debug.Assert(2 <= children.Length, "must be at least 2 children"); Debug.Assert(children.All(child => child != null), "children must not be null"); Debug.Assert(children.All(child => child.IsSink()), "children must be sinks"); Debug.Assert(variable <= _variableCount, "variable out of range"); return GetUniqueVertex(variable, children); } #endregion #region Private helper methods /// /// Returns a Vertex with the given configuration. If this configuration /// is known, returns the existing vertex. Otherwise, a new /// vertex is created. This ensures the vertex is unique in the context /// of this solver. /// private Vertex GetUniqueVertex(int variable, Vertex[] children) { AssertVerticesValid(children); Vertex result = new Vertex(variable, children); // see if we know this vertex already Vertex canonicalResult; if (_knownVertices.TryGetValue(result, out canonicalResult)) { return canonicalResult; } // remember the vertex (because it came first, it's canonical) _knownVertices.Add(result, result); return result; } /// /// Composes the given vertices to produce a new ROBDD. /// private Vertex IfThenElse(Vertex condition, Vertex then, Vertex @else) { AssertVertexValid(condition); AssertVertexValid(then); AssertVertexValid(@else); // check for terminal conditions in the recursion if (condition.IsOne()) { // if '1' then 'then' else '@else' iff. 'then' return then; } if (condition.IsZero()) { // if '0' then 'then' else '@else' iff. '@else' return @else; } if (then.IsOne() && @else.IsZero()) { // if 'condition' then '1' else '0' iff. condition return condition; } if (then.Equals(@else)) { // if 'condition' then 'x' else 'x' iff. x return then; } Vertex result; IfThenElseKey key = new IfThenElseKey(condition, then, @else); // check if we've already computed this result if (_computedIfThenElseValues.TryGetValue(key, out result)) { return result; } int topVariableDomainCount; int topVariable = DetermineTopVariable(condition, then, @else, out topVariableDomainCount); // Recursively compute the new BDD node // Note that we preserve the 'ordered' invariant since the child nodes // cannot contain references to variables < topVariable, and // the topVariable is eliminated from the children through // the call to EvaluateFor. Vertex[] resultCases = new Vertex[topVariableDomainCount]; bool allResultsEqual = true; for (int i = 0; i < topVariableDomainCount; i++) { resultCases[i] = IfThenElse( EvaluateFor(condition, topVariable, i), EvaluateFor(then, topVariable, i), EvaluateFor(@else, topVariable, i)); if (i > 0 && // first vertex is equivalent to itself allResultsEqual && // we've already found a mismatch !resultCases[i].Equals(resultCases[0])) { allResultsEqual = false; } } // if the results are identical, any may be returned if (allResultsEqual) { return resultCases[0]; } // create new vertex result = GetUniqueVertex(topVariable, resultCases); // remember result so that we don't try to compute this if-then-else pattern again _computedIfThenElseValues.Add(key, result); return result; } /// /// Given parts of an if-then-else statement, determines the top variable (nearest /// root). Used to determine which variable forms the root of a composed Vertex. /// private static int DetermineTopVariable(Vertex condition, Vertex then, Vertex @else, out int topVariableDomainCount) { int topVariable; if (condition.Variable < then.Variable) { topVariable = condition.Variable; topVariableDomainCount = condition.Children.Length; } else { topVariable = then.Variable; topVariableDomainCount = then.Children.Length; } if (@else.Variable < topVariable) { topVariable = @else.Variable; topVariableDomainCount = @else.Children.Length; } return topVariable; } /// /// Returns 'vertex' evaluated for the given value of 'variable'. Requires that /// the variable is less than or equal to vertex.Variable. /// private static Vertex EvaluateFor(Vertex vertex, int variable, int variableAssigment) { if (variable < vertex.Variable) { // If the variable we're setting is less than the vertex variable, the // the Vertex 'ordered' invariant ensures that the vertex contains no reference // to that variable. Binding the variable is therefore a no-op. return vertex; } Debug.Assert(variable == vertex.Variable, "variable must be less than or equal to vertex.Variable"); // If the 'vertex' is conditioned on the given 'variable', the children // represent the decompositions of the function for various assignments // to that variable. Debug.Assert(variableAssigment < vertex.Children.Length, "variable assignment out of range"); return vertex.Children[variableAssigment]; } /// /// Checks requirements for vertices. /// [Conditional("DEBUG")] private void AssertVerticesValid(IEnumerable vertices) { Debug.Assert(null != vertices); foreach (Vertex vertex in vertices) { AssertVertexValid(vertex); } } /// /// Checks requirements for a vertex argument (must not be null, and must be in scope /// for this solver) /// [Conditional("DEBUG")] private void AssertVertexValid(Vertex vertex) { Debug.Assert(vertex != null, "vertex must not be null"); // sinks are ok if (!vertex.IsSink()) { // so are vertices created by this solver Vertex comparisonVertex; Debug.Assert(_knownVertices.TryGetValue(vertex, out comparisonVertex) && comparisonVertex.Equals(vertex), "vertex not created by this solver"); } } #endregion /// /// Supports value comparison of vertices. In general, we use reference comparison /// since the Solver ensures a single instance of each canonical Vertex. The Solver /// needs this comparer to ensure a single instance of each canonical Vertex though... /// private class VertexValueComparer : IEqualityComparer { private VertexValueComparer() { } internal static readonly VertexValueComparer Instance = new VertexValueComparer(); public bool Equals(Vertex x, Vertex y) { if (x.IsSink()) { // sync nodes '1' and '0' each have one static instance; use reference return x.Equals(y); } if (x.Variable != y.Variable || x.Children.Length != y.Children.Length) { return false; } for (int i = 0; i < x.Children.Length; i++) { // use reference comparison for the children (they must be // canonical already) if (!x.Children[i].Equals(y.Children[i])) { return false; } } return true; } public int GetHashCode(Vertex vertex) { // sync nodes '1' and '0' each have one static instance; use reference if (vertex.IsSink()) { return vertex.GetHashCode(); } Debug.Assert(2 <= vertex.Children.Length, "internal vertices must have at least 2 children"); unchecked { return ((vertex.Children[0].GetHashCode() << 5) + 1) + vertex.Children[1].GetHashCode(); } } } } /// /// Record structure containing three values. /// struct Triple : IEquatable> where T1 : IEquatable where T2 : IEquatable where T3 : IEquatable { readonly T1 _value1; readonly T2 _value2; readonly T3 _value3; internal Triple(T1 value1, T2 value2, T3 value3) { Debug.Assert(null != (object)value1, "null key element"); Debug.Assert(null != (object)value2, "null key element"); Debug.Assert(null != (object)value3, "null key element"); _value1 = value1; _value2 = value2; _value3 = value3; } public bool Equals(Triple other) { return _value1.Equals(other._value1) && _value2.Equals(other._value2) && _value3.Equals(other._value3); } public override bool Equals(object obj) { Debug.Fail("used typed Equals"); return base.Equals(obj); } public override int GetHashCode() { return _value1.GetHashCode() ^ _value2.GetHashCode() ^ _value3.GetHashCode(); } } } ```