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
|
//---------------------------------------------------------------------
// <copyright file="KnowledgeBase.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;
namespace System.Data.Common.Utils.Boolean
{
/// <summary>
/// Data structure supporting storage of facts and proof (resolution) of queries given
/// those facts.
///
/// For instance, we may know the following facts:
///
/// A --> B
/// A
///
/// Given these facts, the knowledge base can prove the query:
///
/// B
///
/// through resolution.
/// </summary>
/// <typeparam name="T_Identifier">Type of leaf term identifiers in fact expressions.</typeparam>
internal class KnowledgeBase<T_Identifier>
{
private readonly List<BoolExpr<T_Identifier>> _facts;
private Vertex _knowledge;
private readonly ConversionContext<T_Identifier> _context;
/// <summary>
/// Initialize a new knowledge base.
/// </summary>
internal KnowledgeBase()
{
_facts = new List<BoolExpr<T_Identifier>>();
_knowledge = Vertex.One; // we know '1', but nothing else at present
_context = IdentifierService<T_Identifier>.Instance.CreateConversionContext();
}
/// <summary>
/// Adds all facts from another knowledge base
/// </summary>
/// <param name="kb">The other knowledge base</param>
internal void AddKnowledgeBase(KnowledgeBase<T_Identifier> kb)
{
foreach (BoolExpr<T_Identifier> fact in kb._facts)
{
AddFact(fact);
}
}
/// <summary>
/// Adds the given fact to this KB.
/// </summary>
/// <param name="fact">Simple fact.</param>
internal virtual void AddFact(BoolExpr<T_Identifier> fact)
{
_facts.Add(fact);
Converter<T_Identifier> converter = new Converter<T_Identifier>(fact, _context);
Vertex factVertex = converter.Vertex;
_knowledge = _context.Solver.And(_knowledge, factVertex);
}
/// <summary>
/// Adds the given implication to this KB, where implication is of the form:
///
/// condition --> implies
/// </summary>
/// <param name="condition">Condition</param>
/// <param name="implies">Entailed expression</param>
internal void AddImplication(BoolExpr<T_Identifier> condition, BoolExpr<T_Identifier> implies)
{
AddFact(new Implication(condition, implies));
}
/// <summary>
/// Adds an equivalence to this KB, of the form:
///
/// left iff. right
/// </summary>
/// <param name="left">Left operand</param>
/// <param name="right">Right operand</param>
internal void AddEquivalence(BoolExpr<T_Identifier> left, BoolExpr<T_Identifier> right)
{
AddFact(new Equivalence(left, right));
}
public override string ToString()
{
StringBuilder builder = new StringBuilder();
builder.AppendLine("Facts:");
foreach (BoolExpr<T_Identifier> fact in _facts)
{
builder.Append("\t").AppendLine(fact.ToString());
}
return builder.ToString();
}
// Private class improving debugging output for implication facts
// (fact appears as A --> B rather than !A + B)
private class Implication : OrExpr<T_Identifier>
{
BoolExpr<T_Identifier> _condition;
BoolExpr<T_Identifier> _implies;
// (condition --> implies) iff. (!condition OR implies)
internal Implication(BoolExpr<T_Identifier> condition, BoolExpr<T_Identifier> implies)
: base(condition.MakeNegated(), implies)
{
_condition = condition;
_implies = implies;
}
public override string ToString()
{
return StringUtil.FormatInvariant("{0} --> {1}", _condition, _implies);
}
}
// Private class improving debugging output for equivalence facts
// (fact appears as A <--> B rather than (!A + B) . (A + !B))
private class Equivalence : AndExpr<T_Identifier>
{
BoolExpr<T_Identifier> _left;
BoolExpr<T_Identifier> _right;
// (left iff. right) iff. (left --> right AND right --> left)
internal Equivalence(BoolExpr<T_Identifier> left, BoolExpr<T_Identifier> right)
: base(new Implication(left, right), new Implication(right, left))
{
_left = left;
_right = right;
}
public override string ToString()
{
return StringUtil.FormatInvariant("{0} <--> {1}", _left, _right);
}
}
}
}
|
