Code:
/ Dotnetfx_Vista_SP2 / Dotnetfx_Vista_SP2 / 8.0.50727.4016 / DEVDIV / depot / DevDiv / releases / Orcas / QFE / ndp / fx / src / DataEntity / System / Data / Common / Utils / Boolean / Converter.cs / 1 / Converter.cs
//---------------------------------------------------------------------- //// Copyright (c) Microsoft Corporation. All rights reserved. // // // @owner [....] // @backupOwner [....] //--------------------------------------------------------------------- using System; using System.Collections.Generic; using System.Text; using System.Diagnostics; using System.Collections.ObjectModel; using System.Globalization; using System.Linq; namespace System.Data.Common.Utils.Boolean { ////// Handles conversion of expressions to different forms (decision diagram, etc) /// internal sealed class Converter{ private readonly Vertex _vertex; private readonly ConversionContext _context; private DnfSentence _dnf; private CnfSentence _cnf; internal Converter(BoolExpr expr, ConversionContext context) { _context = context ?? IdentifierService .Instance.CreateConversionContext(); _vertex = ToDecisionDiagramConverter .TranslateToRobdd(expr, _context); } internal Vertex Vertex { get { return _vertex; } } internal DnfSentence Dnf { get { InitializeNormalForms(); return _dnf; } } internal CnfSentence Cnf { get { InitializeNormalForms(); return _cnf; } } /// /// Converts the decision diagram (Vertex) wrapped by this converter and translates it into DNF /// and CNF forms. I'll first explain the strategy with respect to DNF, and then explain how CNF /// is achieved in parallel. A DNF sentence representing the expression is simply a disjunction /// of every rooted path through the decision diagram ending in one. For instance, given the /// following decision diagram: /// /// A /// 0/ \1 /// B C /// 0/ \1 0/ \1 /// One Zero One /// /// the following paths evaluate to 'One' /// /// !A, !B /// A, C /// /// and the corresponding DNF is (!A.!B) + (A.C) /// /// It is easy to compute CNF from the DNF of the negation, e.g.: /// /// !((A.B) + (C.D)) iff. (!A+!B) . (!C+!D) /// /// To compute the CNF form in parallel, we negate the expression (by swapping One and Zero sinks) /// and collect negation of the literals along the path. In the above example, the following paths /// evaluate to 'Zero': /// /// !A, B /// A, !C /// /// and the CNF (which takes the negation of all literals in the path) is (!A+B) . (A+!C) /// private void InitializeNormalForms() { if (null == _cnf) { // short-circuit if the root is true/false if (_vertex.IsOne()) { // And() -> True _cnf = new CnfSentence(Set >.Empty); // Or(And()) -> True var emptyClause = new DnfClause (Set >.Empty); var emptyClauseSet = new Set >(); emptyClauseSet.Add(emptyClause); _dnf = new DnfSentence (emptyClauseSet.MakeReadOnly()); } else if (_vertex.IsZero()) { // And(Or()) -> False var emptyClause = new CnfClause (Set >.Empty); var emptyClauseSet = new Set >(); emptyClauseSet.Add(emptyClause); _cnf = new CnfSentence (emptyClauseSet.MakeReadOnly()); // Or() -> False _dnf = new DnfSentence (Set >.Empty); } else { // construct clauses by walking the tree and constructing a clause for each sink Set > dnfClauses = new Set >(); Set > cnfClauses = new Set >(); Set > path = new Set >(); FindAllPaths(_vertex, cnfClauses, dnfClauses, path); _cnf = new CnfSentence (cnfClauses.MakeReadOnly()); _dnf = new DnfSentence (dnfClauses.MakeReadOnly()); } } } private void FindAllPaths(Vertex vertex, Set > cnfClauses, Set > dnfClauses, Set > path) { if (vertex.IsOne()) { // create DNF clause var clause = new DnfClause (path); dnfClauses.Add(clause); } else if (vertex.IsZero()) { // create CNF clause var clause = new CnfClause (new Set >(path.Select(l => l.MakeNegated()))); cnfClauses.Add(clause); } else { // keep on walking... foreach (var successor in _context.GetSuccessors(vertex)) { path.Add(successor.Literal); FindAllPaths(successor.Vertex, cnfClauses, dnfClauses, path); path.Remove(successor.Literal); } } } } } // File provided for Reference Use Only by Microsoft Corporation (c) 2007. //---------------------------------------------------------------------- // // Copyright (c) Microsoft Corporation. All rights reserved. // // // @owner [....] // @backupOwner [....] //--------------------------------------------------------------------- using System; using System.Collections.Generic; using System.Text; using System.Diagnostics; using System.Collections.ObjectModel; using System.Globalization; using System.Linq; namespace System.Data.Common.Utils.Boolean { ////// Handles conversion of expressions to different forms (decision diagram, etc) /// internal sealed class Converter{ private readonly Vertex _vertex; private readonly ConversionContext _context; private DnfSentence _dnf; private CnfSentence _cnf; internal Converter(BoolExpr expr, ConversionContext context) { _context = context ?? IdentifierService .Instance.CreateConversionContext(); _vertex = ToDecisionDiagramConverter .TranslateToRobdd(expr, _context); } internal Vertex Vertex { get { return _vertex; } } internal DnfSentence Dnf { get { InitializeNormalForms(); return _dnf; } } internal CnfSentence Cnf { get { InitializeNormalForms(); return _cnf; } } /// /// Converts the decision diagram (Vertex) wrapped by this converter and translates it into DNF /// and CNF forms. I'll first explain the strategy with respect to DNF, and then explain how CNF /// is achieved in parallel. A DNF sentence representing the expression is simply a disjunction /// of every rooted path through the decision diagram ending in one. For instance, given the /// following decision diagram: /// /// A /// 0/ \1 /// B C /// 0/ \1 0/ \1 /// One Zero One /// /// the following paths evaluate to 'One' /// /// !A, !B /// A, C /// /// and the corresponding DNF is (!A.!B) + (A.C) /// /// It is easy to compute CNF from the DNF of the negation, e.g.: /// /// !((A.B) + (C.D)) iff. (!A+!B) . (!C+!D) /// /// To compute the CNF form in parallel, we negate the expression (by swapping One and Zero sinks) /// and collect negation of the literals along the path. In the above example, the following paths /// evaluate to 'Zero': /// /// !A, B /// A, !C /// /// and the CNF (which takes the negation of all literals in the path) is (!A+B) . (A+!C) /// private void InitializeNormalForms() { if (null == _cnf) { // short-circuit if the root is true/false if (_vertex.IsOne()) { // And() -> True _cnf = new CnfSentence(Set >.Empty); // Or(And()) -> True var emptyClause = new DnfClause (Set >.Empty); var emptyClauseSet = new Set >(); emptyClauseSet.Add(emptyClause); _dnf = new DnfSentence (emptyClauseSet.MakeReadOnly()); } else if (_vertex.IsZero()) { // And(Or()) -> False var emptyClause = new CnfClause (Set >.Empty); var emptyClauseSet = new Set >(); emptyClauseSet.Add(emptyClause); _cnf = new CnfSentence (emptyClauseSet.MakeReadOnly()); // Or() -> False _dnf = new DnfSentence (Set >.Empty); } else { // construct clauses by walking the tree and constructing a clause for each sink Set > dnfClauses = new Set >(); Set > cnfClauses = new Set >(); Set > path = new Set >(); FindAllPaths(_vertex, cnfClauses, dnfClauses, path); _cnf = new CnfSentence (cnfClauses.MakeReadOnly()); _dnf = new DnfSentence (dnfClauses.MakeReadOnly()); } } } private void FindAllPaths(Vertex vertex, Set > cnfClauses, Set > dnfClauses, Set > path) { if (vertex.IsOne()) { // create DNF clause var clause = new DnfClause (path); dnfClauses.Add(clause); } else if (vertex.IsZero()) { // create CNF clause var clause = new CnfClause (new Set >(path.Select(l => l.MakeNegated()))); cnfClauses.Add(clause); } else { // keep on walking... foreach (var successor in _context.GetSuccessors(vertex)) { path.Add(successor.Literal); FindAllPaths(successor.Vertex, cnfClauses, dnfClauses, path); path.Remove(successor.Literal); } } } } } // File provided for Reference Use Only by Microsoft Corporation (c) 2007.
Link Menu
This book is available now!
Buy at Amazon US or
Buy at Amazon UK
- ReflectionUtil.cs
- SQLUtility.cs
- TextEffectCollection.cs
- IIS7WorkerRequest.cs
- PropertyEmitter.cs
- WinEventTracker.cs
- StrongNameUtility.cs
- ListDesigner.cs
- WorkflowQueuingService.cs
- PropertyValueChangedEvent.cs
- CallbackHandler.cs
- SqlMethodCallConverter.cs
- StreamGeometry.cs
- BooleanFunctions.cs
- TreeNodeStyleCollection.cs
- HostingEnvironment.cs
- UnmanagedMemoryStream.cs
- EdmScalarPropertyAttribute.cs
- TableLayoutColumnStyleCollection.cs
- ResourceBinder.cs
- ListViewGroupItemCollection.cs
- MethodRental.cs
- SqlGatherConsumedAliases.cs
- ConfigurationException.cs
- TextBoxAutoCompleteSourceConverter.cs
- CompensatableTransactionScopeActivityDesigner.cs
- JsonQueryStringConverter.cs
- PrintPreviewDialog.cs
- Choices.cs
- Stylesheet.cs
- HttpCookiesSection.cs
- Line.cs
- CacheMemory.cs
- LassoSelectionBehavior.cs
- DefinitionBase.cs
- ChangePasswordAutoFormat.cs
- ObjectListItemCollection.cs
- StylusEditingBehavior.cs
- ClassicBorderDecorator.cs
- SafeFileMapViewHandle.cs
- BulletDecorator.cs
- WindowHideOrCloseTracker.cs
- EncoderFallback.cs
- CellIdBoolean.cs
- CounterSet.cs
- FloaterBaseParaClient.cs
- MethodToken.cs
- DataReceivedEventArgs.cs
- odbcmetadatacollectionnames.cs
- basenumberconverter.cs
- AsyncPostBackErrorEventArgs.cs
- SemaphoreFullException.cs
- PropertyManager.cs
- DecodeHelper.cs
- ImageCodecInfo.cs
- SubstitutionList.cs
- GPStream.cs
- AddInController.cs
- log.cs
- ActivityCodeDomReferenceService.cs
- WindowPattern.cs
- ReliableChannelBinder.cs
- XPathSelectionIterator.cs
- ResourceIDHelper.cs
- FormViewRow.cs
- Deserializer.cs
- InternalControlCollection.cs
- NotifyInputEventArgs.cs
- DependencyProperty.cs
- AuthorizationContext.cs
- PageHandlerFactory.cs
- Bookmark.cs
- PenLineCapValidation.cs
- DataGridViewSelectedColumnCollection.cs
- OleDbCommand.cs
- SafeLibraryHandle.cs
- SafeNativeMethodsCLR.cs
- SHA512.cs
- BindableTemplateBuilder.cs
- EventLogPermission.cs
- WebHttpBindingCollectionElement.cs
- MetadataItemEmitter.cs
- CatalogUtil.cs
- TableDetailsRow.cs
- DefaultParameterValueAttribute.cs
- WindowCollection.cs
- _LocalDataStoreMgr.cs
- IPGlobalProperties.cs
- FieldBuilder.cs
- MethodMessage.cs
- unitconverter.cs
- LogReserveAndAppendState.cs
- ConfigXmlCDataSection.cs
- SqlServices.cs
- PropertyDescriptors.cs
- CacheMode.cs
- ExtendedPropertyDescriptor.cs
- CrossContextChannel.cs
- DrawToolTipEventArgs.cs
- TitleStyle.cs