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

   1 //---------------------------------------------------------------------
   2 // <copyright file="Converter.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.Text;
  13 using System.Diagnostics;
  14 using System.Collections.ObjectModel;
  15 using System.Globalization;
  16 using System.Linq;
  17
  18 namespace System.Data.Common.Utils.Boolean
  19 {
  20
  21     /// <summary>
  22     /// Handles conversion of expressions to different forms (decision diagram, etc)
  23     /// </summary>
  24     internal sealed class Converter<T_Identifier>
  25     {
  26         private readonly Vertex _vertex;
  27         private readonly ConversionContext<T_Identifier> _context;
  28         private DnfSentence<T_Identifier> _dnf;
  29         private CnfSentence<T_Identifier> _cnf;
  30
  31         internal Converter(BoolExpr<T_Identifier> expr, ConversionContext<T_Identifier> context)
  32         {
  33             _context = context ?? IdentifierService<T_Identifier>.Instance.CreateConversionContext();
  34             _vertex = ToDecisionDiagramConverter<T_Identifier>.TranslateToRobdd(expr, _context);
  35         }
  36
  37         internal Vertex Vertex
  38         {
  39             get { return _vertex; }
  40         }
  41
  42         internal DnfSentence<T_Identifier> Dnf
  43         {
  44             get
  45             {
  46                 InitializeNormalForms();
  47                 return _dnf;
  48             }
  49         }
  50
  51         internal CnfSentence<T_Identifier> Cnf
  52         {
  53             get
  54             {
  55                 InitializeNormalForms();
  56                 return _cnf;
  57             }
  58         }
  59
  60         /// <summary>
  61         /// Converts the decision diagram (Vertex) wrapped by this converter and translates it into DNF
  62         /// and CNF forms. I'll first explain the strategy with respect to DNF, and then explain how CNF
  63         /// is achieved in parallel. A DNF sentence representing the expression is simply a disjunction
  64         /// of every rooted path through the decision diagram ending in one. For instance, given the
  65         /// following decision diagram:
  66         ///
  67         ///                         A
  68         ///                       0/ \1
  69         ///                      B     C
  70         ///                    0/ \1 0/ \1
  71         ///                 One   Zero   One
  72         ///
  73         /// the following paths evaluate to 'One'
  74         ///
  75         ///                 !A, !B
  76         ///                 A, C
  77         ///
  78         /// and the corresponding DNF is (!A.!B) + (A.C)
  79         ///
  80         /// It is easy to compute CNF from the DNF of the negation, e.g.:
  81         ///
  82         ///     !((A.B) + (C.D)) iff. (!A+!B) . (!C+!D)
  83         ///
  84         /// To compute the CNF form in parallel, we negate the expression (by swapping One and Zero sinks)
  85         /// and collect negation of the literals along the path. In the above example, the following paths
  86         /// evaluate to 'Zero':
  87         ///
  88         ///                 !A, B
  89         ///                 A, !C
  90         ///
  91         /// and the CNF (which takes the negation of all literals in the path) is (!A+B) . (A+!C)
  92         /// </summary>
  93         private void InitializeNormalForms()
  94         {
  95             if (null == _cnf)
  96             {
  97                 // short-circuit if the root is true/false
  98                 if (_vertex.IsOne())
  99                 {
 100                     // And() -> True
 101                     _cnf = new CnfSentence<T_Identifier>(Set<CnfClause<T_Identifier>>.Empty);
 102                     // Or(And()) -> True
 103                     var emptyClause = new DnfClause<T_Identifier>(Set<Literal<T_Identifier>>.Empty);
 104                     var emptyClauseSet = new Set<DnfClause<T_Identifier>>();
 105                     emptyClauseSet.Add(emptyClause);
 106                     _dnf = new DnfSentence<T_Identifier>(emptyClauseSet.MakeReadOnly());
 107                 }
 108                 else if (_vertex.IsZero())
 109                 {
 110                     // And(Or()) -> False
 111                     var emptyClause = new CnfClause<T_Identifier>(Set<Literal<T_Identifier>>.Empty);
 112                     var emptyClauseSet = new Set<CnfClause<T_Identifier>>();
 113                     emptyClauseSet.Add(emptyClause);
 114                     _cnf = new CnfSentence<T_Identifier>(emptyClauseSet.MakeReadOnly());
 115                     // Or() -> False
 116                     _dnf = new DnfSentence<T_Identifier>(Set<DnfClause<T_Identifier>>.Empty);
 117                 }
 118                 else
 119                 {
 120                     // construct clauses by walking the tree and constructing a clause for each sink
 121                     Set<DnfClause<T_Identifier>> dnfClauses = new Set<DnfClause<T_Identifier>>();
 122                     Set<CnfClause<T_Identifier>> cnfClauses = new Set<CnfClause<T_Identifier>>();
 123                     Set<Literal<T_Identifier>> path = new Set<Literal<T_Identifier>>();
 124
 125                     FindAllPaths(_vertex, cnfClauses, dnfClauses, path);
 126
 127                     _cnf = new CnfSentence<T_Identifier>(cnfClauses.MakeReadOnly());
 128                     _dnf = new DnfSentence<T_Identifier>(dnfClauses.MakeReadOnly());
 129                 }
 130             }
 131         }
 132
 133         private void FindAllPaths(Vertex vertex, Set<CnfClause<T_Identifier>> cnfClauses, Set<DnfClause<T_Identifier>> dnfClauses,
 134             Set<Literal<T_Identifier>> path)
 135         {
 136             if (vertex.IsOne())
 137             {
 138                 // create DNF clause
 139                 var clause = new DnfClause<T_Identifier>(path);
 140                 dnfClauses.Add(clause);
 141             }
 142             else if (vertex.IsZero())
 143             {
 144                 // create CNF clause
 145                 var clause = new CnfClause<T_Identifier>(new Set<Literal<T_Identifier>>(path.Select(l => l.MakeNegated())));
 146                 cnfClauses.Add(clause);
 147             }
 148             else
 149             {
 150                 // keep on walking...
 151                 foreach (var successor in _context.GetSuccessors(vertex))
 152                 {
 153                     path.Add(successor.Literal);
 154                     FindAllPaths(successor.Vertex, cnfClauses, dnfClauses, path);
 155                     path.Remove(successor.Literal);
 156                 }
 157             }
 158         }
 159     }
 160 }