1 //---------------------------------------------------------------------
2 // <copyright file="ConversionContext.cs" company="Microsoft">
3 // Copyright (c) Microsoft Corporation. All rights reserved.
8 //---------------------------------------------------------------------
11 using System.Collections.Generic;
14 using System.Diagnostics;
16 namespace System.Data.Common.Utils.Boolean
19 /// Manages state used to translate BoolExpr to decision diagram vertices and back again.
20 /// Specializations exist for generic and DomainConstraint expressions.
22 internal abstract class ConversionContext<T_Identifier>
25 /// Gets the solver instance associated with this conversion context. Used to reterieve
26 /// canonical Decision Diagram vertices for this context.
28 internal readonly Solver Solver = new Solver();
31 /// Given a term in BoolExpr, returns the corresponding decision diagram vertex.
33 internal abstract Vertex TranslateTermToVertex(TermExpr<T_Identifier> term);
36 /// Describes a vertex as a series of literal->vertex successors such that the literal
37 /// logically implies the given vertex successor.
39 internal abstract IEnumerable<LiteralVertexPair<T_Identifier>> GetSuccessors(Vertex vertex);
43 /// VertexLiteral pair, used for ConversionContext.GetSuccessors
45 internal sealed class LiteralVertexPair<T_Identifier>
47 internal readonly Vertex Vertex;
48 internal readonly Literal<T_Identifier> Literal;
50 internal LiteralVertexPair(Vertex vertex, Literal<T_Identifier> literal)
53 this.Literal = literal;
58 /// Generic implementation of a ConversionContext
60 internal sealed class GenericConversionContext<T_Identifier> : ConversionContext<T_Identifier>
62 readonly Dictionary<TermExpr<T_Identifier>, int> _variableMap = new Dictionary<TermExpr<T_Identifier>, int>();
63 Dictionary<int, TermExpr<T_Identifier>> _inverseVariableMap;
65 internal override Vertex TranslateTermToVertex(TermExpr<T_Identifier> term)
68 if (!_variableMap.TryGetValue(term, out variable))
70 variable = Solver.CreateVariable();
71 _variableMap.Add(term, variable);
73 return Solver.CreateLeafVertex(variable, Solver.BooleanVariableChildren);
76 internal override IEnumerable<LiteralVertexPair<T_Identifier>> GetSuccessors(Vertex vertex)
78 LiteralVertexPair<T_Identifier>[] successors = new LiteralVertexPair<T_Identifier>[2];
80 Debug.Assert(2 == vertex.Children.Length);
81 Vertex then = vertex.Children[0];
82 Vertex @else = vertex.Children[1];
84 // get corresponding term expression
85 InitializeInverseVariableMap();
86 TermExpr<T_Identifier> term = _inverseVariableMap[vertex.Variable];
88 // add positive successor (then)
89 Literal<T_Identifier> literal = new Literal<T_Identifier>(term, true);
90 successors[0] = new LiteralVertexPair<T_Identifier>(then, literal);
92 // add negative successor (else)
93 literal = literal.MakeNegated();
94 successors[1] = new LiteralVertexPair<T_Identifier>(@else, literal);
98 private void InitializeInverseVariableMap()
100 if (null == _inverseVariableMap)
102 _inverseVariableMap = _variableMap.ToDictionary(kvp => kvp.Value, kvp => kvp.Key);
108 /// Specialization of ConversionContext for DomainConstraint BoolExpr
110 internal sealed class DomainConstraintConversionContext<T_Variable, T_Element> : ConversionContext<DomainConstraint<T_Variable, T_Element>>
113 /// A map from domain variables to decision diagram variables.
115 readonly Dictionary<DomainVariable<T_Variable, T_Element>, int> _domainVariableToRobddVariableMap =
116 new Dictionary<DomainVariable<T_Variable, T_Element>, int>();
117 Dictionary<int, DomainVariable<T_Variable, T_Element>> _inverseMap;
120 /// Translates a domain constraint term to an N-ary DD vertex.
122 internal override Vertex TranslateTermToVertex(TermExpr<DomainConstraint<T_Variable, T_Element>> term)
124 var range = term.Identifier.Range;
125 var domainVariable = term.Identifier.Variable;
126 var domain = domainVariable.Domain;
128 if (range.All(element => !domain.Contains(element)))
134 if (domain.All(element => range.Contains(element)))
140 // determine assignments for this constraints (if the range contains a value in the domain, '1', else '0')
141 Vertex[] children = domain.Select(element => range.Contains(element) ? Vertex.One : Vertex.Zero).ToArray();
143 // see if we know this variable
145 if (!_domainVariableToRobddVariableMap.TryGetValue(domainVariable, out robddVariable))
147 robddVariable = Solver.CreateVariable();
148 _domainVariableToRobddVariableMap[domainVariable] = robddVariable;
151 // create a new vertex with the given assignments
152 return Solver.CreateLeafVertex(robddVariable, children);
155 internal override IEnumerable<LiteralVertexPair<DomainConstraint<T_Variable, T_Element>>> GetSuccessors(Vertex vertex)
157 InitializeInverseMap();
158 var domainVariable = _inverseMap[vertex.Variable];
160 // since vertex children are ordinally aligned with domain, handle domain as array
161 var domain = domainVariable.Domain.ToArray();
163 // foreach unique successor vertex, build up range
164 Dictionary<Vertex, Set<T_Element>> vertexToRange = new Dictionary<Vertex, Set<T_Element>>();
166 for (int i = 0; i < vertex.Children.Length; i++)
168 Vertex successorVertex = vertex.Children[i];
169 Set<T_Element> range;
170 if (!vertexToRange.TryGetValue(successorVertex, out range))
172 range = new Set<T_Element>(domainVariable.Domain.Comparer);
173 vertexToRange.Add(successorVertex, range);
175 range.Add(domain[i]);
178 foreach (var vertexRange in vertexToRange)
180 var successorVertex = vertexRange.Key;
181 var range = vertexRange.Value;
183 // construct a DomainConstraint including the given range
184 var constraint = new DomainConstraint<T_Variable, T_Element>(domainVariable, range.MakeReadOnly());
185 var literal = new Literal<DomainConstraint<T_Variable, T_Element>>(
186 new TermExpr<DomainConstraint<T_Variable, T_Element>>(constraint), true);
188 yield return new LiteralVertexPair<DomainConstraint<T_Variable, T_Element>>(successorVertex, literal);
192 private void InitializeInverseMap()
194 if (null == _inverseMap)
196 _inverseMap = _domainVariableToRobddVariableMap.ToDictionary(kvp => kvp.Value, kvp => kvp.Key);