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

   1 //---------------------------------------------------------------------
   2 // <copyright file="ConversionContext.cs" company="Microsoft">
   3 //      Copyright (c) Microsoft Corporation.  All rights reserved.
   4 // </copyright>
   5 //
   6 // @owner Microsoft
   7 // @backupOwner Microsoft
   8 //---------------------------------------------------------------------
   9
  10 using System;
  11 using System.Collections.Generic;
  12 using System.Linq;
  13 using System.Text;
  14 using System.Diagnostics;
  15
  16 namespace System.Data.Common.Utils.Boolean
  17 {
  18     /// <summary>
  19     /// Manages state used to translate BoolExpr to decision diagram vertices and back again.
  20     /// Specializations exist for generic and DomainConstraint expressions.
  21     /// </summary>
  22     internal abstract class ConversionContext<T_Identifier>
  23     {
  24         /// <summary>
  25         /// Gets the solver instance associated with this conversion context. Used to reterieve
  26         /// canonical Decision Diagram vertices for this context.
  27         /// </summary>
  28         internal readonly Solver Solver = new Solver();
  29
  30         /// <summary>
  31         /// Given a term in BoolExpr, returns the corresponding decision diagram vertex.
  32         /// </summary>
  33         internal abstract Vertex TranslateTermToVertex(TermExpr<T_Identifier> term);
  34
  35         /// <summary>
  36         /// Describes a vertex as a series of literal->vertex successors such that the literal
  37         /// logically implies the given vertex successor.
  38         /// </summary>
  39         internal abstract IEnumerable<LiteralVertexPair<T_Identifier>> GetSuccessors(Vertex vertex);
  40     }
  41
  42     /// <summary>
  43     /// VertexLiteral pair, used for ConversionContext.GetSuccessors
  44     /// </summary>
  45     internal sealed class LiteralVertexPair<T_Identifier>
  46     {
  47         internal readonly Vertex Vertex;
  48         internal readonly Literal<T_Identifier> Literal;
  49
  50         internal LiteralVertexPair(Vertex vertex, Literal<T_Identifier> literal)
  51         {
  52             this.Vertex = vertex;
  53             this.Literal = literal;
  54         }
  55     }
  56
  57     /// <summary>
  58     /// Generic implementation of a ConversionContext
  59     /// </summary>
  60     internal sealed class GenericConversionContext<T_Identifier> : ConversionContext<T_Identifier>
  61     {
  62         readonly Dictionary<TermExpr<T_Identifier>, int> _variableMap = new Dictionary<TermExpr<T_Identifier>, int>();
  63         Dictionary<int, TermExpr<T_Identifier>> _inverseVariableMap;
  64
  65         internal override Vertex TranslateTermToVertex(TermExpr<T_Identifier> term)
  66         {
  67             int variable;
  68             if (!_variableMap.TryGetValue(term, out variable))
  69             {
  70                 variable = Solver.CreateVariable();
  71                 _variableMap.Add(term, variable);
  72             }
  73             return Solver.CreateLeafVertex(variable, Solver.BooleanVariableChildren);
  74         }
  75
  76         internal override IEnumerable<LiteralVertexPair<T_Identifier>> GetSuccessors(Vertex vertex)
  77         {
  78             LiteralVertexPair<T_Identifier>[] successors = new LiteralVertexPair<T_Identifier>[2];
  79
  80             Debug.Assert(2 == vertex.Children.Length);
  81             Vertex then = vertex.Children[0];
  82             Vertex @else = vertex.Children[1];
  83
  84             // get corresponding term expression
  85             InitializeInverseVariableMap();
  86             TermExpr<T_Identifier> term = _inverseVariableMap[vertex.Variable];
  87
  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);
  91
  92             // add negative successor (else)
  93             literal = literal.MakeNegated();
  94             successors[1] = new LiteralVertexPair<T_Identifier>(@else, literal);
  95             return successors;
  96         }
  97
  98         private void InitializeInverseVariableMap()
  99         {
 100             if (null == _inverseVariableMap)
 101             {
 102                 _inverseVariableMap = _variableMap.ToDictionary(kvp => kvp.Value, kvp => kvp.Key);
 103             }
 104         }
 105     }
 106
 107     /// <summary>
 108     /// Specialization of ConversionContext for DomainConstraint BoolExpr
 109     /// </summary>
 110     internal sealed class DomainConstraintConversionContext<T_Variable, T_Element> : ConversionContext<DomainConstraint<T_Variable, T_Element>>
 111     {
 112         /// <summary>
 113         /// A map from domain variables to decision diagram variables.
 114         /// </summary>
 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;
 118
 119         /// <summary>
 120         /// Translates a domain constraint term to an N-ary DD vertex.
 121         /// </summary>
 122         internal override Vertex TranslateTermToVertex(TermExpr<DomainConstraint<T_Variable, T_Element>> term)
 123         {
 124             var range = term.Identifier.Range;
 125             var domainVariable = term.Identifier.Variable;
 126             var domain = domainVariable.Domain;
 127
 128             if (range.All(element => !domain.Contains(element)))
 129             {
 130                 // trivially false
 131                 return Vertex.Zero;
 132             }
 133
 134             if (domain.All(element => range.Contains(element)))
 135             {
 136                 // trivially true
 137                 return Vertex.One;
 138             }
 139
 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();
 142
 143             // see if we know this variable
 144             int robddVariable;
 145             if (!_domainVariableToRobddVariableMap.TryGetValue(domainVariable, out robddVariable))
 146             {
 147                 robddVariable = Solver.CreateVariable();
 148                 _domainVariableToRobddVariableMap[domainVariable] = robddVariable;
 149             }
 150
 151             // create a new vertex with the given assignments
 152             return Solver.CreateLeafVertex(robddVariable, children);
 153         }
 154
 155         internal override IEnumerable<LiteralVertexPair<DomainConstraint<T_Variable, T_Element>>> GetSuccessors(Vertex vertex)
 156         {
 157             InitializeInverseMap();
 158             var domainVariable = _inverseMap[vertex.Variable];
 159
 160             // since vertex children are ordinally aligned with domain, handle domain as array
 161             var domain = domainVariable.Domain.ToArray();
 162
 163             // foreach unique successor vertex, build up range
 164             Dictionary<Vertex, Set<T_Element>> vertexToRange = new Dictionary<Vertex, Set<T_Element>>();
 165
 166             for (int i = 0; i < vertex.Children.Length; i++)
 167             {
 168                 Vertex successorVertex = vertex.Children[i];
 169                 Set<T_Element> range;
 170                 if (!vertexToRange.TryGetValue(successorVertex, out range))
 171                 {
 172                     range = new Set<T_Element>(domainVariable.Domain.Comparer);
 173                     vertexToRange.Add(successorVertex, range);
 174                 }
 175                 range.Add(domain[i]);
 176             }
 177
 178             foreach (var vertexRange in vertexToRange)
 179             {
 180                 var successorVertex = vertexRange.Key;
 181                 var range = vertexRange.Value;
 182
 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);
 187
 188                 yield return new LiteralVertexPair<DomainConstraint<T_Variable, T_Element>>(successorVertex, literal);
 189             }
 190         }
 191
 192         private void InitializeInverseMap()
 193         {
 194             if (null == _inverseMap)
 195             {
 196                 _inverseMap = _domainVariableToRobddVariableMap.ToDictionary(kvp => kvp.Value, kvp => kvp.Key);
 197             }
 198         }
 199     }
 200 }