@@ -41,53 +41,38 @@ def cylinder_notify(self, cylinder, assignment):
41
41
print "Cylinder:\n " , cylinder
42
42
pass
43
43
44
+
45
+ # Get all the reductums (including the polynomial itself), but not the constant
46
+ def get_reductums (f , x ):
47
+ R = []
48
+ while f .var () == x :
49
+ R .append (f )
50
+ f = f .reductum ()
51
+ return R
52
+
53
+ # Polynomials with sign conditions are considered a conjunction
54
+ CONJUNCTIVE = 0
55
+ # Polynomials with sign conditions are considered a disjunction
56
+ DISJUNCTIVE = 1
44
57
45
58
# Do cylindrical algebraic decomposition (CAD)
46
59
class CAD :
47
-
48
- # Map from variables to polynomials
49
- projection_map = {}
50
-
51
- # Signs of relevant polynomials, mapping top variables to polynomials (for lifting)
52
- sign_condition_map = {}
53
-
54
- # Set of variables we're working with
55
- variables = []
56
-
57
- # Notification
58
- cylinder_notify = CylinderNotify ()
59
-
60
- # Polynomials with sign conditions are considered a conjunction
61
- CONJUCTIVE = 0
62
- # Polynomials with sign conditions are considered a disjunction
63
- DISJUNCTIVE = 1
64
-
65
- # Type of CAD
66
- type = CONJUCTIVE
67
-
60
+
68
61
# Initialize
69
- def __init__ (self , variable_list ):
70
- # Set the variable order
71
- polypy .variable_order .set (variable_list )
72
- # Map from variables to sets of polynomials
62
+ def __init__ (self , variable_list , type = CONJUNCTIVE ):
63
+ # Init variables
73
64
self .projection_map = {}
74
65
self .sign_condition_map = {}
66
+ self .variables = variable_list
67
+ self .cylinder_notify = CylinderNotify ()
68
+ self .type = type
69
+ # Initialize the maps
75
70
for x in variable_list :
76
71
self .projection_map [x ] = set ()
77
72
self .sign_condition_map [x ] = set ()
78
-
79
- # Variables
80
- self .variables = variable_list
81
-
82
- # Get all the reductums (including the polynomial itself), but not the constant
83
- @staticmethod
84
- def get_reductums (f , x ):
85
- R = []
86
- while f .var () == x :
87
- R .append (f )
88
- f = f .reductum ()
89
- return R
90
-
73
+ # Set the variable order
74
+ polypy .variable_order .set (variable_list )
75
+
91
76
# Add a polynomial to CAD
92
77
def add_polynomial (self , f , sign_condition = None ):
93
78
# Factor the polynomial
@@ -104,7 +89,7 @@ def add_polynomial(self, f, sign_condition = None):
104
89
105
90
# Check if the assignment respects the polynomials with top variable x
106
91
def check_assignment (self , x , assignment ):
107
- if self .type == CAD . CONJUCTIVE :
92
+ if self .type == CONJUNCTIVE :
108
93
for p , sgn_condition in self .sign_condition_map [x ]:
109
94
if not p .sgn_check (assignment , sgn_condition ):
110
95
return False
@@ -121,29 +106,26 @@ def add_polynomials(self, polynomials):
121
106
self .add_polynomial (f )
122
107
123
108
# Project. Go down the variable stack and project:
124
- # [1] coeff(f) for f in poly[x]
125
- # [2] psc(g, g') for f in poly[x], g in R(f, x)
126
- # [3] psc(g1, g2) for f1, f2 in poly[x], g1 in R(f1, x), g2 in R(f2, x)
127
109
def project (self ):
128
110
for x in reversed (self .variables ):
129
111
# Project variable x
130
112
x_poly_set = self .projection_map [x ]
131
113
# [1] coeff(f) for f in poly[x]
132
- for f in self . projection_map [ x ] :
114
+ for f in x_poly_set :
133
115
self .add_polynomials (f .coefficients ())
134
116
# [2] psc(g, g') for f in poly[x], g in R(f, x)
135
- for f in self . projection_map [ x ] :
136
- for g in CAD . get_reductums (f , x ):
117
+ for f in x_poly_set :
118
+ for g in get_reductums (f , x ):
137
119
g_d = f .derivative ()
138
120
if (g_d .var () == x ):
139
121
self .add_polynomials (g .psc (g_d ))
140
122
# [3] psc(g1, g2) for f1, f2 in poly[x], g1 in R(f1, x), g2 in R(f2, x)
141
- for (f1 , f2 ) in itertools .combinations (self . projection_map [ x ] , 2 ):
142
- f1_R = CAD . get_reductums (f1 , x )
143
- f2_R = CAD . get_reductums (f2 , x )
123
+ for (f1 , f2 ) in itertools .combinations (x_poly_set , 2 ):
124
+ f1_R = get_reductums (f1 , x )
125
+ f2_R = get_reductums (f2 , x )
144
126
for (g1 , g2 ) in itertools .product (f1_R , f2_R ):
145
- self .add_polynomials (g1 .psc (g2 ))
146
-
127
+ self .add_polynomial (g1 .psc (g2 ))
128
+
147
129
# Lift the first variable, update the assignment and lift recursively
148
130
def lift_first_var (self , variables , assignment , cylinder ):
149
131
# We've tried all variables, this assignment checks out
@@ -190,7 +172,12 @@ def lift(self):
190
172
assignment = polypy .Assignment ()
191
173
cylinder = Cylinder ()
192
174
self .lift_first_var (self .variables , assignment , cylinder )
193
-
175
+
176
+ # Run the CAD construction
177
+ def run (self ):
178
+ self .project ()
179
+ self .lift ()
180
+
194
181
# Print internal state
195
182
def print_state (self ):
196
183
print "Variables:" , self .variables
@@ -208,7 +195,5 @@ def print_state(self):
208
195
# Setup CAD
209
196
cad = CAD ([x , y ])
210
197
cad .add_polynomial (x ** 2 + y ** 2 - 1 , polypy .SGN_GE_0 )
211
- # Project
212
- cad .project ()
213
- # Lift
214
- cad .lift ()
198
+ # Run CAD
199
+ cad .run ()
0 commit comments