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

   1 //---------------------------------------------------------------------
   2 // <copyright file="BoolExpr.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.Globalization;
  14 using System.Collections.ObjectModel;
  15 using System.Diagnostics;
  16 using System.Linq;
  17
  18 namespace System.Data.Common.Utils.Boolean
  19 {
  20     /// <summary>
  21     /// Base type for Boolean expressions. Boolean expressions are immutable,
  22     /// and value-comparable using Equals. Services include local simplification
  23     /// and normalization to Conjunctive and Disjunctive Normal Forms.
  24     /// </summary>
  25     /// <remarks>
  26     /// Comments use the following notation convention:
  27     ///
  28     ///     "A . B" means "A and B"
  29     ///     "A + B" means "A or B"
  30     ///     "!A" means "not A"
  31     /// </remarks>
  32     /// <typeparam name="T_Identifier">The type of leaf term identifiers in this expression.</typeparam>
  33     internal abstract partial class BoolExpr<T_Identifier> : IEquatable<BoolExpr<T_Identifier>>
  34     {
  35         /// <summary>
  36         /// Gets an enumeration value indicating the type of the expression node.
  37         /// </summary>
  38         internal abstract ExprType ExprType { get; }
  39
  40         /// <summary>
  41         /// Standard accept method invoking the appropriate method overload
  42         /// in the given visitor.
  43         /// </summary>
  44         /// <typeparam name="T_Return">T_Return is the return type for the visitor.</typeparam>
  45         /// <param name="visitor">Visitor implementation.</param>
  46         /// <returns>Value computed for this node.</returns>
  47         internal abstract T_Return Accept<T_Return>(Visitor<T_Identifier, T_Return> visitor);
  48
  49         /// <summary>
  50         /// Invokes the Simplifier visitor on this expression tree.
  51         /// Simplifications are purely local (see Simplifier class
  52         /// for details).
  53         /// </summary>
  54         internal BoolExpr<T_Identifier> Simplify()
  55         {
  56             return IdentifierService<T_Identifier>.Instance.LocalSimplify(this);
  57         }
  58
  59         /// <summary>
  60         /// Expensive simplification that considers various permutations of the
  61         /// expression (including Decision Diagram, DNF, and CNF translations)
  62         /// </summary>
  63         internal BoolExpr<T_Identifier> ExpensiveSimplify(out Converter<T_Identifier> converter)
  64         {
  65             var context = IdentifierService<T_Identifier>.Instance.CreateConversionContext();
  66             converter = new Converter<T_Identifier>(this, context);
  67
  68             // Check for valid/unsat constraints
  69             if (converter.Vertex.IsOne())
  70             {
  71                 return TrueExpr<T_Identifier>.Value;
  72             }
  73             if (converter.Vertex.IsZero())
  74             {
  75                 return FalseExpr<T_Identifier>.Value;
  76             }
  77
  78             // Pick solution from the (unmodified) expression, its CNF and its DNF
  79             return ChooseCandidate(this, converter.Cnf.Expr, converter.Dnf.Expr);
  80         }
  81
  82         private static BoolExpr<T_Identifier> ChooseCandidate(params BoolExpr<T_Identifier>[] candidates)
  83         {
  84             Debug.Assert(null != candidates && 1 < candidates.Length, "must be at least one to pick");
  85
  86             int resultUniqueTermCount = default(int);
  87             int resultTermCount = default(int);
  88             BoolExpr<T_Identifier> result = null;
  89
  90             foreach (var candidate in candidates)
  91             {
  92                 // first do basic simplification
  93                 var simplifiedCandidate = candidate.Simplify();
  94
  95                 // determine "interesting" properties of the expression
  96                 int candidateUniqueTermCount = simplifiedCandidate.GetTerms().Distinct().Count();
  97                 int candidateTermCount = simplifiedCandidate.CountTerms();
  98
  99                 // see if it's better than the current result best result
 100                 if (null == result || // bootstrap
 101                     candidateUniqueTermCount < resultUniqueTermCount || // check if the candidate improves on # of terms
 102                     (candidateUniqueTermCount == resultUniqueTermCount && // in case of tie, choose based on total
 103                      candidateTermCount < resultTermCount))
 104                 {
 105                     result = simplifiedCandidate;
 106                     resultUniqueTermCount = candidateUniqueTermCount;
 107                     resultTermCount = candidateTermCount;
 108                 }
 109             }
 110
 111             return result;
 112         }
 113
 114         /// <summary>
 115         /// Returns all term expressions below this node.
 116         /// </summary>
 117         internal List<TermExpr<T_Identifier>> GetTerms()
 118         {
 119             return LeafVisitor<T_Identifier>.GetTerms(this);
 120         }
 121
 122         /// <summary>
 123         /// Counts terms in this expression.
 124         /// </summary>
 125         internal int CountTerms()
 126         {
 127             return TermCounter<T_Identifier>.CountTerms(this);
 128         }
 129
 130         /// <summary>
 131         /// Implicit cast from a value of type T to a TermExpr where
 132         /// TermExpr.Value is set to the given value.
 133         /// </summary>
 134         /// <param name="value">Value to wrap in term expression</param>
 135         /// <returns>Term expression</returns>
 136         public static implicit operator BoolExpr<T_Identifier>(T_Identifier value)
 137         {
 138             return new TermExpr<T_Identifier>(value);
 139         }
 140
 141         /// <summary>
 142         /// Creates the negation of the current element.
 143         /// </summary>
 144         internal virtual BoolExpr<T_Identifier> MakeNegated()
 145         {
 146             return new NotExpr<T_Identifier>(this);
 147         }
 148
 149         public override string ToString()
 150         {
 151             return ExprType.ToString();
 152         }
 153
 154         public bool Equals(BoolExpr<T_Identifier> other)
 155         {
 156             return null != other && ExprType == other.ExprType &&
 157                 EquivalentTypeEquals(other);
 158         }
 159
 160         protected abstract bool EquivalentTypeEquals(BoolExpr<T_Identifier> other);
 161     }
 162
 163     /// <summary>
 164     /// Boolean expression that evaluates to true.
 165     /// </summary>
 166     /// <typeparam name="T_Identifier">The type of leaf term identifiers in this expression.</typeparam>
 167     internal sealed class TrueExpr<T_Identifier> : BoolExpr<T_Identifier>
 168     {
 169         private static readonly TrueExpr<T_Identifier> s_value = new TrueExpr<T_Identifier>();
 170
 171         // private constructor so that we control existence of True instance
 172         private TrueExpr()
 173             : base()
 174         {
 175         }
 176
 177         /// <summary>
 178         /// Gets the one instance of TrueExpr
 179         /// </summary>
 180         internal static TrueExpr<T_Identifier> Value { get { return s_value; } }
 181
 182         internal override ExprType ExprType { get { return ExprType.True; } }
 183
 184         internal override T_Return Accept<T_Return>(Visitor<T_Identifier, T_Return> visitor)
 185         {
 186             return visitor.VisitTrue(this);
 187         }
 188
 189         internal override BoolExpr<T_Identifier> MakeNegated()
 190         {
 191             return FalseExpr<T_Identifier>.Value;
 192         }
 193
 194         protected override bool EquivalentTypeEquals(BoolExpr<T_Identifier> other)
 195         {
 196             return object.ReferenceEquals(this, other);
 197         }
 198     }
 199
 200     /// <summary>
 201     /// Boolean expression that evaluates to false.
 202     /// </summary>
 203     /// <typeparam name="T_Identifier">The type of leaf term identifiers in this expression.</typeparam>
 204     internal sealed class FalseExpr<T_Identifier> : BoolExpr<T_Identifier>
 205     {
 206         private static readonly FalseExpr<T_Identifier> s_value = new FalseExpr<T_Identifier>();
 207
 208         // private constructor so that we control existence of False instance
 209         private FalseExpr()
 210             : base()
 211         {
 212         }
 213
 214         /// <summary>
 215         /// Gets the one instance of FalseExpr
 216         /// </summary>
 217         internal static FalseExpr<T_Identifier> Value { get { return s_value; } }
 218
 219         internal override ExprType ExprType { get { return ExprType.False; } }
 220
 221         internal override T_Return Accept<T_Return>(Visitor<T_Identifier, T_Return> visitor)
 222         {
 223             return visitor.VisitFalse(this);
 224         }
 225
 226         internal override BoolExpr<T_Identifier> MakeNegated()
 227         {
 228             return TrueExpr<T_Identifier>.Value;
 229         }
 230
 231         protected override bool EquivalentTypeEquals(BoolExpr<T_Identifier> other)
 232         {
 233             return object.ReferenceEquals(this, other);
 234         }
 235     }
 236
 237     /// <summary>
 238     /// A term is a leaf node in a Boolean expression. Its value (T/F) is undefined.
 239     /// </summary>
 240     /// <typeparam name="T_Identifier">The type of leaf term identifiers in this expression.</typeparam>
 241     internal sealed class TermExpr<T_Identifier> : BoolExpr<T_Identifier>, IEquatable<TermExpr<T_Identifier>>
 242     {
 243         private readonly T_Identifier _identifier;
 244         private readonly IEqualityComparer<T_Identifier> _comparer;
 245
 246         /// <summary>
 247         /// Construct a term.
 248         /// </summary>
 249         /// <param name="comparer">Value comparer to use when comparing two
 250         /// term expressions.</param>
 251         /// <param name="identifier">Identifier/tag for this term.</param>
 252         internal TermExpr(IEqualityComparer<T_Identifier> comparer, T_Identifier identifier)
 253             : base()
 254         {
 255             Debug.Assert(null != (object)identifier);
 256             _identifier = identifier;
 257             if (null == comparer) { _comparer = EqualityComparer<T_Identifier>.Default; }
 258             else { _comparer = comparer; }
 259         }
 260         internal TermExpr(T_Identifier identifier) : this(null, identifier) { }
 261
 262         /// <summary>
 263         /// Gets identifier for this term. This value is used to determine whether
 264         /// two terms as equivalent.
 265         /// </summary>
 266         internal T_Identifier Identifier { get { return _identifier; } }
 267
 268         internal override ExprType ExprType { get { return ExprType.Term; } }
 269
 270         public override bool Equals(object obj)
 271         {
 272             Debug.Fail("use only typed equals");
 273             return this.Equals(obj as TermExpr<T_Identifier>);
 274         }
 275
 276         public bool Equals(TermExpr<T_Identifier> other)
 277         {
 278             return _comparer.Equals(_identifier, other._identifier);
 279         }
 280
 281         protected override bool EquivalentTypeEquals(BoolExpr<T_Identifier> other)
 282         {
 283             return _comparer.Equals(_identifier, ((TermExpr<T_Identifier>)other)._identifier);
 284         }
 285
 286         public override int GetHashCode()
 287         {
 288             return _comparer.GetHashCode(_identifier);
 289         }
 290
 291         public override string ToString()
 292         {
 293             return StringUtil.FormatInvariant("{0}", _identifier);
 294         }
 295
 296         internal override T_Return Accept<T_Return>(Visitor<T_Identifier, T_Return> visitor)
 297         {
 298             return visitor.VisitTerm(this);
 299         }
 300
 301         internal override BoolExpr<T_Identifier> MakeNegated()
 302         {
 303             Literal<T_Identifier> literal = new Literal<T_Identifier>(this, true);
 304             // leverage normalization code if it exists
 305             Literal<T_Identifier> negatedLiteral = literal.MakeNegated();
 306             if (negatedLiteral.IsTermPositive)
 307             {
 308                 return negatedLiteral.Term;
 309             }
 310             else
 311             {
 312                 return new NotExpr<T_Identifier>(negatedLiteral.Term);
 313             }
 314         }
 315     }
 316
 317     /// <summary>
 318     /// Abstract base class for tree expressions (unary as in Not, n-ary
 319     /// as in And or Or). Duplicate elements are trimmed at construction
 320     /// time (algorithms applied to these trees rely on the assumption
 321     /// of uniform children).
 322     /// </summary>
 323     /// <typeparam name="T_Identifier">The type of leaf term identifiers in this expression.</typeparam>
 324     internal abstract class TreeExpr<T_Identifier> : BoolExpr<T_Identifier>
 325     {
 326         private readonly Set<BoolExpr<T_Identifier>> _children;
 327         private readonly int _hashCode;
 328
 329         /// <summary>
 330         /// Initialize a new tree expression with the given children.
 331         /// </summary>
 332         /// <param name="children">Child expressions</param>
 333         protected TreeExpr(IEnumerable<BoolExpr<T_Identifier>> children)
 334             : base()
 335         {
 336             Debug.Assert(null != children);
 337             _children = new Set<BoolExpr<T_Identifier>>(children);
 338             _children.MakeReadOnly();
 339             _hashCode = _children.GetElementsHashCode();
 340         }
 341
 342         /// <summary>
 343         /// Gets the children of this expression node.
 344         /// </summary>
 345         internal Set<BoolExpr<T_Identifier>> Children { get { return _children; } }
 346
 347         public override bool Equals(object obj)
 348         {
 349             Debug.Fail("use only typed Equals");
 350             return base.Equals(obj as BoolExpr<T_Identifier>);
 351         }
 352
 353         public override int GetHashCode()
 354         {
 355             return _hashCode;
 356         }
 357
 358         public override string ToString()
 359         {
 360             return StringUtil.FormatInvariant("{0}({1})", ExprType, _children);
 361         }
 362
 363         protected override bool EquivalentTypeEquals(BoolExpr<T_Identifier> other)
 364         {
 365             return ((TreeExpr<T_Identifier>)other).Children.SetEquals(Children);
 366         }
 367     }
 368
 369     /// <summary>
 370     /// A tree expression that evaluates to true iff. none of its children
 371     /// evaluate to false.
 372     /// </summary>
 373     /// <remarks>
 374     /// An And expression with no children is equivalent to True (this is an
 375     /// operational convenience because we assume an implicit True is along
 376     /// for the ride in every And expression)
 377     ///
 378     ///     A . True iff. A
 379     /// </remarks>
 380     /// <typeparam name="T_Identifier">The type of leaf term identifiers in this expression.</typeparam>
 381     internal class AndExpr<T_Identifier> : TreeExpr<T_Identifier>
 382     {
 383         /// <summary>
 384         /// Initialize a new And expression with the given children.
 385         /// </summary>
 386         /// <param name="children">Child expressions</param>
 387         internal AndExpr(params BoolExpr<T_Identifier>[] children)
 388             : this((IEnumerable<BoolExpr<T_Identifier>>)children)
 389         {
 390         }
 391
 392         /// <summary>
 393         /// Initialize a new And expression with the given children.
 394         /// </summary>
 395         /// <param name="children">Child expressions</param>
 396         internal AndExpr(IEnumerable<BoolExpr<T_Identifier>> children)
 397             : base(children)
 398         {
 399         }
 400
 401         internal override ExprType ExprType { get { return ExprType.And; } }
 402
 403         internal override T_Return Accept<T_Return>(Visitor<T_Identifier, T_Return> visitor)
 404         {
 405             return visitor.VisitAnd(this);
 406         }
 407     }
 408
 409     /// <summary>
 410     /// A tree expression that evaluates to true iff. any of its children
 411     /// evaluates to true.
 412     /// </summary>
 413     /// <remarks>
 414     /// An Or expression with no children is equivalent to False (this is an
 415     /// operational convenience because we assume an implicit False is along
 416     /// for the ride in every Or expression)
 417     ///
 418     ///     A + False iff. A
 419     /// </remarks>
 420     /// <typeparam name="T_Identifier">The type of leaf term identifiers in this expression.</typeparam>
 421     internal class OrExpr<T_Identifier> : TreeExpr<T_Identifier>
 422     {
 423         /// <summary>
 424         /// Initialize a new Or expression with the given children.
 425         /// </summary>
 426         /// <param name="children">Child expressions</param>
 427         internal OrExpr(params BoolExpr<T_Identifier>[] children)
 428             : this((IEnumerable<BoolExpr<T_Identifier>>)children)
 429         {
 430         }
 431
 432         /// <summary>
 433         /// Initialize a new Or expression with the given children.
 434         /// </summary>
 435         /// <param name="children">Child expressions</param>
 436         internal OrExpr(IEnumerable<BoolExpr<T_Identifier>> children)
 437             : base(children)
 438         {
 439         }
 440
 441         internal override ExprType ExprType { get { return ExprType.Or; } }
 442
 443         internal override T_Return Accept<T_Return>(Visitor<T_Identifier, T_Return> visitor)
 444         {
 445             return visitor.VisitOr(this);
 446         }
 447     }
 448
 449     /// <summary>
 450     /// A tree expression that evaluates to true iff. its (single) child evaluates to false.
 451     /// </summary>
 452     /// <typeparam name="T_Identifier">The type of leaf term identifiers in this expression.</typeparam>
 453     internal sealed class NotExpr<T_Identifier> : TreeExpr<T_Identifier>
 454     {
 455         /// <summary>
 456         /// Initialize a new Not expression with the given child.
 457         /// </summary>
 458         /// <param name="child"></param>
 459         internal NotExpr(BoolExpr<T_Identifier> child)
 460             : base(new BoolExpr<T_Identifier>[] { child })
 461         {
 462         }
 463
 464         internal override ExprType ExprType { get { return ExprType.Not; } }
 465
 466         internal BoolExpr<T_Identifier> Child { get { return Children.First(); } }
 467
 468         internal override T_Return Accept<T_Return>(Visitor<T_Identifier, T_Return> visitor)
 469         {
 470             return visitor.VisitNot(this);
 471         }
 472
 473         public override string ToString()
 474         {
 475             return String.Format(CultureInfo.InvariantCulture, "!{0}", Child);
 476         }
 477
 478         internal override BoolExpr<T_Identifier> MakeNegated()
 479         {
 480             return this.Child;
 481         }
 482     }
 483
 484     /// <summary>
 485     /// Enumeration of Boolean expression node types.
 486     /// </summary>
 487     internal enum ExprType
 488     {
 489         And, Not, Or, Term, True, False,
 490     }
 491 }