1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
//---------------------------------------------------------------------
// <copyright file="Sentence.cs" company="Microsoft">
// Copyright (c) Microsoft Corporation. All rights reserved.
// </copyright>
//
// @owner [....]
// @backupOwner [....]
//---------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Text;
using System.Globalization;
using System.Collections.ObjectModel;
using System.Diagnostics;
using System.Linq;
namespace System.Data.Common.Utils.Boolean
{
/// <summary>
/// Abstract base class for nodes in normal form expressions, e.g. Conjunctive Normal Form
/// sentences.
/// </summary>
/// <typeparam name="T_Identifier">Type of expression leaf term identifiers.</typeparam>
internal abstract class NormalFormNode<T_Identifier>
{
private readonly BoolExpr<T_Identifier> _expr;
/// <summary>
/// Initialize a new normal form node representing the given expression. Caller must
/// ensure the expression is logically equivalent to the node.
/// </summary>
/// <param name="expr">Expression logically equivalent to this node.</param>
protected NormalFormNode(BoolExpr<T_Identifier> expr) { _expr = expr.Simplify(); }
/// <summary>
/// Gets an expression that is logically equivalent to this node.
/// </summary>
internal BoolExpr<T_Identifier> Expr { get { return _expr; } }
/// <summary>
/// Utility method for delegation that return the expression corresponding to a given
/// normal form node.
/// </summary>
/// <typeparam name="T_NormalFormNode">Type of node</typeparam>
/// <param name="node">Node to examine.</param>
/// <returns>Equivalent Boolean expression for the given node.</returns>
protected static BoolExpr<T_Identifier> ExprSelector<T_NormalFormNode>(T_NormalFormNode node)
where T_NormalFormNode : NormalFormNode<T_Identifier>
{
return node._expr;
}
}
/// <summary>
/// Abstract base class for normal form sentences (CNF and DNF)
/// </summary>
/// <typeparam name="T_Identifier">Type of expression leaf term identifiers.</typeparam>
/// <typeparam name="T_Clause">Type of clauses in the sentence.</typeparam>
internal abstract class Sentence<T_Identifier, T_Clause> : NormalFormNode<T_Identifier>
where T_Clause : Clause<T_Identifier>, IEquatable<T_Clause>
{
private readonly Set<T_Clause> _clauses;
/// <summary>
/// Initialize a sentence given the appropriate sentence clauses. Produces
/// an equivalent expression by composing the clause expressions using
/// the given tree type.
/// </summary>
/// <param name="clauses">Sentence clauses</param>
/// <param name="treeType">Tree type for sentence (and generated expression)</param>
protected Sentence(Set<T_Clause> clauses, ExprType treeType)
: base(ConvertClausesToExpr(clauses, treeType))
{
_clauses = clauses.AsReadOnly();
}
// Produces an expression equivalent to the given clauses by composing the clause
// expressions using the given tree type.
private static BoolExpr<T_Identifier> ConvertClausesToExpr(Set<T_Clause> clauses, ExprType treeType)
{
bool isAnd = ExprType.And == treeType;
Debug.Assert(isAnd || ExprType.Or == treeType);
IEnumerable<BoolExpr<T_Identifier>> clauseExpressions =
clauses.Select(new Func<T_Clause, BoolExpr<T_Identifier>>(ExprSelector));
if (isAnd)
{
return new AndExpr<T_Identifier>(clauseExpressions);
}
else
{
return new OrExpr<T_Identifier>(clauseExpressions);
}
}
public override string ToString()
{
StringBuilder builder = new StringBuilder();
builder.Append("Sentence{");
builder.Append(_clauses);
return builder.Append("}").ToString();
}
}
/// <summary>
/// Represents a sentence in disjunctive normal form, e.g.:
///
/// Clause1 + Clause2 . ...
///
/// Where each DNF clause is of the form:
///
/// Literal1 . Literal2 . ...
///
/// Each literal is of the form:
///
/// Term
///
/// or
///
/// !Term
/// </summary>
/// <typeparam name="T_Identifier">Type of expression leaf term identifiers.</typeparam>
internal sealed class DnfSentence<T_Identifier> : Sentence<T_Identifier, DnfClause<T_Identifier>>
{
// Initializes a new DNF sentence given its clauses.
internal DnfSentence(Set<DnfClause<T_Identifier>> clauses)
: base(clauses, ExprType.Or)
{
}
}
/// <summary>
/// Represents a sentence in conjunctive normal form, e.g.:
///
/// Clause1 . Clause2 . ...
///
/// Where each DNF clause is of the form:
///
/// Literal1 + Literal2 + ...
///
/// Each literal is of the form:
///
/// Term
///
/// or
///
/// !Term
/// </summary>
/// <typeparam name="T_Identifier">Type of expression leaf term identifiers.</typeparam>
internal sealed class CnfSentence<T_Identifier> : Sentence<T_Identifier, CnfClause<T_Identifier>>
{
// Initializes a new CNF sentence given its clauses.
internal CnfSentence(Set<CnfClause<T_Identifier>> clauses)
: base(clauses, ExprType.And)
{
}
}
}
|
