-
Notifications
You must be signed in to change notification settings - Fork 0
/
stringcons.py
94 lines (74 loc) · 3.1 KB
/
stringcons.py
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
"""Functions for analysing the satisfiability of string constraints"""
from collections import defaultdict
from itertools import ifilter
def satisfiable(pos_cons, neg_cons):
"""A function for analysing constraints of the form e.g.
[a="v1"][a|="v2"]:not([a~="v3"]):not([a$="v4"])"
:param pos_cons:
a Set() of pairs (op, v) giving positive constraints on the attribute a,
where op is a String from "=", "|=", "~=", &c. and v is a String giving the
RHS.
:param neg_cons:
a Set() of pairs (op, v) giving negative constraints (appearing in
:not()) on the attribute a, where op is a String from "=", "|=", "~=",
&c. and v is a String giving the RHS.
:returns:
True if the constraints are satisfiable are there are an infinite number
of possible solutions.
False if there are no solutions.
A String if there is a unique solution.
"""
if len(pos_cons) + len(neg_cons) > 1:
# pos/negmap[op] = set of values v such that [a op v]
posmap = defaultdict(set)
for (op, v) in pos_cons:
posmap[op].add(v)
negmap = defaultdict(set)
for (op, v) in neg_cons:
negmap[op].add(v)
# Catch basic case of lots of ~= from class constraints
# Satisfiable as long as we don't have a ~= x and :not(a ~= x)
if ((len(negmap) == 0 or
(len(negmap) == 1 and next(iter(negmap)) == "~=")) and
(len(posmap) == 0 or
(len(posmap) == 1 and next(iter(posmap)) == "~="))):
return not any(v in posmap["~="] for v in negmap["~="])
# Catch igloo case of two equality constraints
# a = x & a = y with x != y
if (len(posmap) == 1 and
next(iter(posmap)) == "=" and
len(posmap["="]) > 1):
return False
# Catch reveal.css constraints
# a = x and :not(a = y)
if (len(posmap) == 1 and
next(iter(posmap)) == "=" and
len(negmap) == 1 and
next(iter(negmap)) == "="):
return not any(v in posmap["="] for v in negmap["="])
# Catch reveal.css constraints
# a exists (by any operator) and :not(a)
if (len(posmap) > 0 and
len(negmap) == 1 and
next(iter(negmap)) == "exists"):
return False
# Catch a test case constraint
# a *= b and :not(a = d)
if (len(posmap) == 1 and
next(iter(posmap)) == "*=" and
len(posmap["*="]) == 1 and
len(negmap) == 1 and
next(iter(negmap)) == "=" and
len(negmap["="]) == 1):
return True
# Catch only positive substring guards (*= or ~=) and at most one ^= and $=
if (len(negmap) == 0 and
len(posmap["^="]) <= 1 and
len(posmap["$="]) <= 1 and
len(posmap["|="]) == 0 and
len(posmap["="]) == 0):
return True
print "WARNING: String Constraints Unknown, assuming True!"
print "Pos cons: ", pos_cons
print "Neg cons: ", neg_cons
return True # TODO