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
|
from typing import TypeVar, Any, List, Tuple, Dict, Set
from itertools import product
from pprint import pprint
# do we have numpy here?
import numpy as np
from .sets_representation import SolFiniteSetRepresentation
from .posets_product import MyFinitePosetProduct
from .posets_sum import MyFinitePosetDisjointUnion
import act4e_interfaces as I
X = TypeVar("X")
class MyFinitePoset(I.FinitePoset[X]):
_carrier: I.FiniteSet[X]
_values: List[Tuple[X,X]]
# Implementation using adjacency and reachability matrix
_adjacency: np.ndarray
_paths: np.ndarray
def __init__(self, carrier: I.FiniteSet[X], values: List[Tuple[X,X]]):
self._carrier = carrier
self._values = values
self._paths = np.eye(carrier.size(), dtype=bool)
if self._values:
self._compute_paths_naive()
# self._compute_paths_fast()
def _compute_paths_naive(self):
# Create adjancency matrix. Because poset can be represented as a hasse
# diagram, which is the same as a directed graph we can create an
# adjacency matrix for the graph of the relation. In particular when
# the graph is acyclic the adjancency matrix is nilpotent. Even if the
# graph contains cycles we can still precompute a reachability matrix
# and check in O(1) whether there is a relation between two elements
n = self._carrier.size()
# We use booleans to avoid overflow, we do not care how long the path
# is, only whether it exists or not
self._adjacency = np.zeros((n, n), dtype=bool)
# Build adjacency matrix
for a, b in self._values:
ia = self._carrier.elements().index(a)
ib = self._carrier.elements().index(b)
self._adjacency[ia][ib] = True
# Compute the reachability matrix, i.e. a power series of the adjacency
# matrix if the adjacency matrix is nilpotent the power series is
# finite, otherwise it is not, but this is not a problem since we can
# upper bound the number of terms needed in this case with the number
# of nodes
self._paths = np.eye(n, dtype=bool)
adjpow = np.eye(n, dtype=bool)
for _ in range(n):
# compute the p-th power of the adjacency matrix and add it to the
# series.
adjpow = (adjpow @ self._adjacency > 0)
self._paths = np.logical_or(self._paths, adjpow)
# if the graph is acylic we stop earlier
if np.allclose(adjpow, 0):
break
# if not np.allclose(adjpow, 0):
# print(f"Adjacency matrix may not be nilpotent! Ran for {_} "
# + "iterations and there are nonzero entries, "
# + f"the graph ({n} nodes) may contain cycles")
# print(f"Computed path matrix for poset with elements {self._carrier.elements()}:")
# print(self._paths.astype(int))
def carrier(self) -> I.FiniteSet[X]:
return self._carrier
def holds(self, a: X, b: X) -> bool:
# a is smaller than b, means that there is a path in the graph from a to b
if self._has_path(a, b):
return True
return False
def _cmp(self, a: X, b: X) -> bool:
assert self._carrier.contains(a)
assert self._carrier.contains(b)
# a is both smaller and bigger than b
# i.e. they are equivalent
if self._has_path(a, b) and self._has_path(b, a):
return 0
# a is smaller than b
if self._has_path(a, b):
return 1
# b is smaller than a, or
# a is bigger than b
if self._has_path(b, a):
return -1
# else not comparable
raise RuntimeError(f"Cannot compare {a} with {b}.")
def _has_path(self, a: X, b: X) -> bool:
ia = self._carrier.elements().index(a)
ib = self._carrier.elements().index(b)
# if self._paths[ia][ib] > 0:
# print(f"The path from {a = } to {b = } has length {self._paths[ia][ib]}")
return self._paths[ia][ib] > 0
class SolFinitePosetRepresentation(I.FinitePosetRepresentation):
def load(self, h: I.IOHelper, s: I.FinitePoset_desc) -> I.FinitePoset[Any]:
if "poset_product" in s.keys():
posets = [self.load(h, p) for p in s["poset_product"]]
return MyFinitePosetProduct(posets)
if "poset_sum" in s.keys():
posets = [self.load(h, p) for p in s["poset_sum"]]
return MyFinitePosetDisjointUnion(posets)
if not all(k in s.keys() for k in ["carrier", "hasse"]):
raise I.InvalidFormat()
fsr = SolFiniteSetRepresentation()
X = fsr.load(h, s["carrier"])
return MyFinitePoset(X, s["hasse"])
def save(self, h: I.IOHelper, p: I.FinitePoset[Any]) -> I.FinitePoset_desc:
fsr = SolFiniteSetRepresentation()
d = {"carrier": fsr.save(h, p.carrier()),
"hasse": []}
for a in p.carrier().elements():
for b in p.carrier().elements():
if p.holds(a, b):
d["hasse"].append([a, b])
return d
|
