1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
//---------------------------------------------------------------------
// <copyright file="Vertex.cs" company="Microsoft">
// Copyright (c) Microsoft Corporation. All rights reserved.
// </copyright>
//
// @owner Microsoft
// @backupOwner Microsoft
//---------------------------------------------------------------------
using System;
using System.Collections.Generic;
namespace System.Data.Common.Utils.Boolean
{
using System.Diagnostics;
using System.Globalization;
/// <summary>
/// A node in a Reduced Ordered Boolean Decision Diagram. Reads as:
///
/// if 'Variable' then 'Then' else 'Else'
///
/// Invariant: the Then and Else children must refer to 'deeper' variables,
/// or variables with a higher value. Otherwise, the graph is not 'Ordered'.
/// All creation of vertices is mediated by the Solver class which ensures
/// each vertex is unique. Otherwise, the graph is not 'Reduced'.
/// </summary>
sealed class Vertex : IEquatable<Vertex>
{
/// <summary>
/// Initializes a sink BDD node (zero or one)
/// </summary>
private Vertex()
{
this.Variable = int.MaxValue;
this.Children = new Vertex[] { };
}
internal Vertex(int variable, Vertex[] children)
{
EntityUtil.BoolExprAssert(variable < int.MaxValue,
"exceeded number of supported variables");
AssertConstructorArgumentsValid(variable, children);
this.Variable = variable;
this.Children = children;
}
[Conditional("DEBUG")]
private static void AssertConstructorArgumentsValid(int variable, Vertex[] children)
{
Debug.Assert(null != children, "internal vertices must define children");
Debug.Assert(2 <= children.Length, "internal vertices must have at least two children");
Debug.Assert(0 < variable, "internal vertices must have 0 < variable");
foreach (Vertex child in children)
{
Debug.Assert(variable < child.Variable, "children must have greater variable");
}
}
/// <summary>
/// Sink node representing the Boolean function '1' (true)
/// </summary>
internal static readonly Vertex One = new Vertex();
/// <summary>
/// Sink node representing the Boolean function '0' (false)
/// </summary>
internal static readonly Vertex Zero = new Vertex();
/// <summary>
/// Gets the variable tested by this vertex. If this is a sink node, returns
/// int.MaxValue since there is no variable to test (and since this is a leaf,
/// this non-existent variable is 'deeper' than any existing variable; the
/// variable value is larger than any real variable)
/// </summary>
internal readonly int Variable;
/// <summary>
/// Note: do not modify elements.
/// Gets the result when Variable evaluates to true. If this is a sink node,
/// returns null.
/// </summary>
internal readonly Vertex[] Children;
/// <summary>
/// Returns true if this is '1'.
/// </summary>
internal bool IsOne()
{
return object.ReferenceEquals(Vertex.One, this);
}
/// <summary>
/// Returns true if this is '0'.
/// </summary>
internal bool IsZero()
{
return object.ReferenceEquals(Vertex.Zero, this);
}
/// <summary>
/// Returns true if this is '0' or '1'.
/// </summary>
internal bool IsSink()
{
return Variable == int.MaxValue;
}
public bool Equals(Vertex other)
{
return object.ReferenceEquals(this, other);
}
public override bool Equals(object obj)
{
Debug.Fail("used typed Equals");
return base.Equals(obj);
}
public override int GetHashCode()
{
return base.GetHashCode();
}
public override string ToString()
{
if (IsOne())
{
return "_1_";
}
if (IsZero())
{
return "_0_";
}
return String.Format(CultureInfo.InvariantCulture, "<{0}, {1}>", Variable, StringUtil.ToCommaSeparatedString(Children));
}
}
}
|
