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
|
//---------------------------------------------------------------------
// <copyright file="Clause.cs" company="Microsoft">
// Copyright (c) Microsoft Corporation. All rights reserved.
// </copyright>
//
// @owner Microsoft
// @backupOwner Microsoft
//---------------------------------------------------------------------
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>
/// Base class for clauses, which are (constrained) combinations of literals.
/// </summary>
/// <typeparam name="T_Identifier">Type of normal form literal.</typeparam>
internal abstract class Clause<T_Identifier> : NormalFormNode<T_Identifier>
{
private readonly Set<Literal<T_Identifier>> _literals;
private readonly int _hashCode;
/// <summary>
/// Initialize a new clause.
/// </summary>
/// <param name="literals">Literals contained in the clause.</param>
/// <param name="treeType">Type of expression tree to produce from literals.</param>
protected Clause(Set<Literal<T_Identifier>> literals, ExprType treeType)
: base(ConvertLiteralsToExpr(literals, treeType))
{
_literals = literals.AsReadOnly();
_hashCode = _literals.GetElementsHashCode();
}
/// <summary>
/// Gets the literals contained in this clause.
/// </summary>
internal Set<Literal<T_Identifier>> Literals
{
get { return _literals; }
}
// Given a collection of literals and a tree type, returns an expression of the given type.
private static BoolExpr<T_Identifier> ConvertLiteralsToExpr(Set<Literal<T_Identifier>> literals, ExprType treeType)
{
bool isAnd = ExprType.And == treeType;
Debug.Assert(isAnd || ExprType.Or == treeType);
IEnumerable<BoolExpr<T_Identifier>> literalExpressions = literals.Select(
new Func<Literal<T_Identifier>, BoolExpr<T_Identifier>>(ConvertLiteralToExpression));
if (isAnd)
{
return new AndExpr<T_Identifier>(literalExpressions);
}
else
{
return new OrExpr<T_Identifier>(literalExpressions);
}
}
// Given a literal, returns its logical equivalent expression.
private static BoolExpr<T_Identifier> ConvertLiteralToExpression(Literal<T_Identifier> literal)
{
return literal.Expr;
}
public override string ToString()
{
StringBuilder builder = new StringBuilder();
builder.Append("Clause{");
builder.Append(_literals);
return builder.Append("}").ToString();
}
public override int GetHashCode()
{
return _hashCode;
}
public override bool Equals(object obj)
{
Debug.Fail("call typed Equals");
return base.Equals(obj);
}
}
/// <summary>
/// A DNF clause is of the form:
///
/// Literal1 . Literal2 . ...
///
/// Each literal is of the form:
///
/// Term
///
/// or
///
/// !Term
/// </summary>
/// <typeparam name="T_Identifier">Type of normal form literal.</typeparam>
internal sealed class DnfClause<T_Identifier> : Clause<T_Identifier>,
IEquatable<DnfClause<T_Identifier>>
{
/// <summary>
/// Initialize a DNF clause.
/// </summary>
/// <param name="literals">Literals in clause.</param>
internal DnfClause(Set<Literal<T_Identifier>> literals)
: base(literals, ExprType.And)
{
}
public bool Equals(DnfClause<T_Identifier> other)
{
return null != other &&
other.Literals.SetEquals(Literals);
}
}
/// <summary>
/// A CNF clause is of the form:
///
/// Literal1 + Literal2 . ...
///
/// Each literal is of the form:
///
/// Term
///
/// or
///
/// !Term
/// </summary>
/// <typeparam name="T_Identifier">Type of normal form literal.</typeparam>
internal sealed class CnfClause<T_Identifier> : Clause<T_Identifier>,
IEquatable<CnfClause<T_Identifier>>
{
/// <summary>
/// Initialize a CNF clause.
/// </summary>
/// <param name="literals">Literals in clause.</param>
internal CnfClause(Set<Literal<T_Identifier>> literals)
: base(literals, ExprType.Or)
{
}
public bool Equals(CnfClause<T_Identifier> other)
{
return null != other &&
other.Literals.SetEquals(Literals);
}
}
}
|
