9{
10
11 for (const auto &s : statements) {
12 if (is_a<Contains>(*s)) {
13 const Contains &contains = down_cast<const Contains &>(*s);
14 const auto expr = contains.get_expr();
15 const auto set = contains.get_set();
16 if (is_a<Symbol>(*expr)) {
17 if (is_a<Complexes>(*set)) {
18 complex_symbols_.
insert(expr);
19 } else if (is_a<Reals>(*set)) {
20 complex_symbols_.
insert(expr);
21 real_symbols_.
insert(expr);
22 } else if (is_a<Rationals>(*set)) {
23 complex_symbols_.
insert(expr);
24 real_symbols_.
insert(expr);
25 rational_symbols_.
insert(expr);
26 } else if (is_a<Integers>(*set)) {
27 complex_symbols_.
insert(expr);
28 real_symbols_.
insert(expr);
29 rational_symbols_.
insert(expr);
30 integer_symbols_.
insert(expr);
31 }
32 }
33 } else if (is_a<LessThan>(*s)) {
34 const LessThan &less_than = down_cast<const LessThan &>(*s);
35 const auto &arg1 = less_than.get_arg1();
36 const auto &arg2 = less_than.get_arg2();
38 real_symbols_.
insert(arg2);
39 if (down_cast<const Number &>(*arg1).is_positive()) {
40 set_map(nonnegative_, arg2, true);
41 set_map(positive_, arg2, true);
42 set_map(negative_, arg2, false);
43 set_map(nonpositive_, arg2, false);
44 set_map(nonzero_, arg2, true);
45 set_map(zero_, arg2, false);
46 } else if (down_cast<const Number &>(*arg1).is_zero()) {
47 set_map(nonnegative_, arg2, true);
48 set_map(negative_, arg2, false);
49 }
50 }
else if (is_a<Symbol>(*arg1) and
is_a_Number(*arg2)) {
51 real_symbols_.
insert(arg1);
52 if (down_cast<const Number &>(*arg2).is_negative()) {
53 set_map(nonnegative_, arg1, false);
54 set_map(positive_, arg1, false);
55 set_map(negative_, arg1, true);
56 set_map(nonpositive_, arg1, true);
57 set_map(nonzero_, arg1, true);
58 set_map(zero_, arg1, false);
59 } else if (down_cast<const Number &>(*arg2).is_zero()) {
60 set_map(nonpositive_, arg1, true);
61 set_map(positive_, arg1, false);
62 }
63 }
64 } else if (is_a<StrictLessThan>(*s)) {
65 const StrictLessThan &strictly_less_than
66 = down_cast<const StrictLessThan &>(*s);
67 const auto arg1 = strictly_less_than.get_arg1();
68 const auto arg2 = strictly_less_than.get_arg2();
70 real_symbols_.
insert(arg2);
71 if (not down_cast<const Number &>(*arg1).is_negative()) {
72 set_map(nonnegative_, arg2, true);
73 set_map(positive_, arg2, true);
74 set_map(negative_, arg2, false);
75 set_map(nonpositive_, arg2, false);
76 set_map(nonzero_, arg2, true);
77 set_map(zero_, arg2, false);
78 }
79 }
else if (is_a<Symbol>(*arg1) and
is_a_Number(*arg2)) {
80 real_symbols_.
insert(arg1);
81 if (not down_cast<const Number &>(*arg2).is_positive()) {
82 set_map(nonnegative_, arg1, false);
83 set_map(positive_, arg1, false);
84 set_map(negative_, arg1, true);
85 set_map(nonpositive_, arg1, true);
86 set_map(nonzero_, arg1, true);
87 set_map(zero_, arg1, false);
88 }
89 }
90 } else if (is_a<Equality>(*s)) {
91 const Equality &equals = down_cast<const Equality &>(*s);
92 const auto arg1 = equals.get_arg1();
93 const auto arg2 = equals.get_arg2();
95 complex_symbols_.
insert(arg2);
96 if (down_cast<const Number &>(*arg1).is_zero()) {
97 set_map(zero_, arg2, true);
98 real_symbols_.
insert(arg2);
99 rational_symbols_.
insert(arg2);
100 integer_symbols_.
insert(arg2);
101 set_map(positive_, arg2, false);
102 set_map(negative_, arg2, false);
103 set_map(nonpositive_, arg2, true);
104 set_map(nonnegative_, arg2, true);
105 set_map(nonzero_, arg2, false);
106 } else {
107 set_map(zero_, arg2, false);
108 set_map(nonzero_, arg2, true);
109 }
110 }
111 } else if (is_a<Unequality>(*s)) {
112 const Unequality &uneq = down_cast<const Unequality &>(*s);
113 const auto arg1 = uneq.get_arg1();
114 const auto arg2 = uneq.get_arg2();
116 if (down_cast<const Number &>(*arg1).is_zero()) {
117 set_map(zero_, arg2, false);
118 set_map(nonzero_, arg2, true);
119 }
120 }
121 }
122 }
123}
bool is_a_Number(const Basic &b)