Code:
/ 4.0 / 4.0 / DEVDIV_TFS / Dev10 / Releases / RTMRel / ndp / fx / src / DataEntity / System / Data / Common / Utils / Boolean / Solver.cs / 1305376 / Solver.cs
//----------------------------------------------------------------------
//
// Copyright (c) Microsoft Corporation. All rights reserved.
//
//
// @owner [....]
// @backupOwner [....]
//---------------------------------------------------------------------
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 variable----igment)
{
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(variable----igment < vertex.Children.Length, "variable assignment out of range");
return vertex.Children[variable----igment];
}
///
/// 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())
{
// [....] 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)
{
// [....] 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();
}
}
}
// File provided for Reference Use Only by Microsoft Corporation (c) 2007.
//----------------------------------------------------------------------
//
// Copyright (c) Microsoft Corporation. All rights reserved.
//
//
// @owner [....]
// @backupOwner [....]
//---------------------------------------------------------------------
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 variable----igment)
{
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(variable----igment < vertex.Children.Length, "variable assignment out of range");
return vertex.Children[variable----igment];
}
///
/// 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())
{
// [....] 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)
{
// [....] 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();
}
}
}
// File provided for Reference Use Only by Microsoft Corporation (c) 2007.
Link Menu
This book is available now!
Buy at Amazon US or
Buy at Amazon UK
- ObjectDataSourceView.cs
- SafeArrayTypeMismatchException.cs
- PKCS1MaskGenerationMethod.cs
- WebSysDefaultValueAttribute.cs
- MailMessageEventArgs.cs
- DigitalSignature.cs
- Font.cs
- PassportIdentity.cs
- DesignTimeXamlWriter.cs
- ControlFilterExpression.cs
- RoleService.cs
- XhtmlBasicFormAdapter.cs
- StringFunctions.cs
- ReaderWriterLockWrapper.cs
- ResourceDefaultValueAttribute.cs
- PropertyIDSet.cs
- ObjectDataSourceDisposingEventArgs.cs
- HostedHttpTransportManager.cs
- FlagsAttribute.cs
- StreamResourceInfo.cs
- DuplicateWaitObjectException.cs
- HttpHandlersSection.cs
- XmlWellformedWriter.cs
- PersonalizationDictionary.cs
- VolatileEnlistmentMultiplexing.cs
- ObjectListGeneralPage.cs
- TextServicesManager.cs
- Currency.cs
- GenericPrincipal.cs
- CqlGenerator.cs
- ToolStripRendererSwitcher.cs
- EventDescriptor.cs
- NewItemsContextMenuStrip.cs
- DataControlLinkButton.cs
- Visual3DCollection.cs
- ActiveXSite.cs
- EntityExpressionVisitor.cs
- CallbackValidator.cs
- ManualResetEventSlim.cs
- DataGridBoolColumn.cs
- SqlCacheDependencySection.cs
- StringCollection.cs
- RepeatButtonAutomationPeer.cs
- FormClosedEvent.cs
- CommonDialog.cs
- DataColumnPropertyDescriptor.cs
- ProxyWebPart.cs
- PropertyPath.cs
- DebugView.cs
- CSharpCodeProvider.cs
- TriggerBase.cs
- ObjectViewEntityCollectionData.cs
- ProxyRpc.cs
- Dump.cs
- LineBreak.cs
- ContentElementAutomationPeer.cs
- CodeGeneratorOptions.cs
- Paragraph.cs
- CfgArc.cs
- Deserializer.cs
- ClusterSafeNativeMethods.cs
- XmlSubtreeReader.cs
- LocalTransaction.cs
- ColorMatrix.cs
- DateTimeConverter2.cs
- ManagementEventWatcher.cs
- BoundField.cs
- _ContextAwareResult.cs
- GeneralTransform.cs
- GridViewDeleteEventArgs.cs
- StyleTypedPropertyAttribute.cs
- DocumentStream.cs
- XmlSerializationGeneratedCode.cs
- SQLBytesStorage.cs
- ShadowGlyph.cs
- XhtmlBasicControlAdapter.cs
- WindowsToolbarAsMenu.cs
- BroadcastEventHelper.cs
- ReturnEventArgs.cs
- DbSourceCommand.cs
- LineVisual.cs
- NetSectionGroup.cs
- TrackingMemoryStreamFactory.cs
- HtmlTableCell.cs
- SizeValueSerializer.cs
- UnitySerializationHolder.cs
- ReadOnlyActivityGlyph.cs
- TextParagraphProperties.cs
- Latin1Encoding.cs
- BindingGroup.cs
- ClassicBorderDecorator.cs
- WeakRefEnumerator.cs
- GeometryCombineModeValidation.cs
- _DigestClient.cs
- EntityTransaction.cs
- ComPlusAuthorization.cs
- AnimatedTypeHelpers.cs
- SmtpClient.cs
- AuthenticationModuleElement.cs
- MailFileEditor.cs