assumptions.cpp
1 #include <symengine/logic.h>
2 #include <symengine/assumptions.h>
3 #include <symengine/number.h>
4 
5 namespace SymEngine
6 {
7 
8 Assumptions::Assumptions(const set_basic &statements)
9 {
10  // Convert a set of statements into a faster and easier internal form
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<Reals>(*set)) {
18  complex_symbols_.insert(expr);
19  real_symbols_.insert(expr);
20  } else if (is_a<Rationals>(*set)) {
21  complex_symbols_.insert(expr);
22  real_symbols_.insert(expr);
23  rational_symbols_.insert(expr);
24  } else if (is_a<Integers>(*set)) {
25  complex_symbols_.insert(expr);
26  real_symbols_.insert(expr);
27  rational_symbols_.insert(expr);
28  integer_symbols_.insert(expr);
29  }
30  }
31  } else if (is_a<LessThan>(*s)) {
32  const LessThan &less_than = down_cast<const LessThan &>(*s);
33  const auto &arg1 = less_than.get_arg1();
34  const auto &arg2 = less_than.get_arg2();
35  if (is_a<Symbol>(*arg2) and is_a_Number(*arg1)) {
36  real_symbols_.insert(arg2);
37  if (down_cast<const Number &>(*arg1).is_positive()) {
38  set_map(nonnegative_, arg2, true);
39  set_map(positive_, arg2, true);
40  set_map(negative_, arg2, false);
41  set_map(nonpositive_, arg2, false);
42  set_map(nonzero_, arg2, true);
43  set_map(zero_, arg2, false);
44  } else if (down_cast<const Number &>(*arg1).is_zero()) {
45  set_map(nonnegative_, arg2, true);
46  set_map(negative_, arg2, false);
47  }
48  } else if (is_a<Symbol>(*arg1) and is_a_Number(*arg2)) {
49  real_symbols_.insert(arg1);
50  if (down_cast<const Number &>(*arg2).is_negative()) {
51  set_map(nonnegative_, arg1, false);
52  set_map(positive_, arg1, false);
53  set_map(negative_, arg1, true);
54  set_map(nonpositive_, arg1, true);
55  set_map(nonzero_, arg1, true);
56  set_map(zero_, arg1, false);
57  } else if (down_cast<const Number &>(*arg2).is_zero()) {
58  set_map(nonpositive_, arg1, true);
59  set_map(positive_, arg1, false);
60  }
61  }
62  } else if (is_a<StrictLessThan>(*s)) {
63  const StrictLessThan &strictly_less_than
64  = down_cast<const StrictLessThan &>(*s);
65  const auto arg1 = strictly_less_than.get_arg1();
66  const auto arg2 = strictly_less_than.get_arg2();
67  if (is_a<Symbol>(*arg2) and is_a_Number(*arg1)) {
68  real_symbols_.insert(arg2);
69  if (not down_cast<const Number &>(*arg1).is_negative()) {
70  set_map(nonnegative_, arg2, true);
71  set_map(positive_, arg2, true);
72  set_map(negative_, arg2, false);
73  set_map(nonpositive_, arg2, false);
74  set_map(nonzero_, arg2, true);
75  set_map(zero_, arg2, false);
76  }
77  } else if (is_a<Symbol>(*arg1) and is_a_Number(*arg2)) {
78  real_symbols_.insert(arg1);
79  if (not down_cast<const Number &>(*arg2).is_positive()) {
80  set_map(nonnegative_, arg1, false);
81  set_map(positive_, arg1, false);
82  set_map(negative_, arg1, true);
83  set_map(nonpositive_, arg1, true);
84  set_map(nonzero_, arg1, true);
85  set_map(zero_, arg1, false);
86  }
87  }
88  } else if (is_a<Equality>(*s)) {
89  const Equality &equals = down_cast<const Equality &>(*s);
90  const auto arg1 = equals.get_arg1();
91  const auto arg2 = equals.get_arg2();
92  if (is_a_Number(*arg1) and is_a<Symbol>(*arg2)) {
93  complex_symbols_.insert(arg2);
94  if (down_cast<const Number &>(*arg1).is_zero()) {
95  set_map(zero_, arg2, true);
96  real_symbols_.insert(arg2);
97  rational_symbols_.insert(arg2);
98  integer_symbols_.insert(arg2);
99  set_map(positive_, arg2, false);
100  set_map(negative_, arg2, false);
101  set_map(nonpositive_, arg2, true);
102  set_map(nonnegative_, arg2, true);
103  set_map(nonzero_, arg2, false);
104  } else {
105  set_map(zero_, arg2, false);
106  set_map(nonzero_, arg2, true);
107  }
108  }
109  } else if (is_a<Unequality>(*s)) {
110  const Unequality &uneq = down_cast<const Unequality &>(*s);
111  const auto arg1 = uneq.get_arg1();
112  const auto arg2 = uneq.get_arg2();
113  if (is_a_Number(*arg1) and is_a<Symbol>(*arg2)) {
114  if (down_cast<const Number &>(*arg1).is_zero()) {
115  set_map(zero_, arg2, false);
116  set_map(nonzero_, arg2, true);
117  }
118  }
119  }
120  }
121 }
122 
123 void Assumptions::set_map(umap_basic_bool &map, const RCP<const Basic> &symbol,
124  bool value)
125 {
126  // Set element in map to true or false. Check for consistency within map
127  tribool old_value = from_map(map, symbol);
128  if ((is_true(old_value) and not value) or (is_false(old_value) and value)) {
129  throw SymEngineException("Symbol " + symbol->__str__()
130  + " have inconsistent positive/negativeness");
131  }
132  map[symbol] = value;
133 }
134 
135 tribool Assumptions::from_map(const umap_basic_bool &map,
136  const RCP<const Basic> &symbol) const
137 {
138  auto it = map.find(symbol);
139  if (it != map.end()) {
140  return (tribool)((*it).second);
141  } else {
142  return tribool::indeterminate;
143  }
144 }
145 
146 tribool Assumptions::is_complex(const RCP<const Basic> &symbol) const
147 {
148  bool cmplx = complex_symbols_.find(symbol) != complex_symbols_.end();
149  return cmplx ? tribool::tritrue : tribool::indeterminate;
150 }
151 
152 tribool Assumptions::is_real(const RCP<const Basic> &symbol) const
153 {
154  bool real = real_symbols_.find(symbol) != real_symbols_.end();
155  return real ? tribool::tritrue : tribool::indeterminate;
156 }
157 
158 tribool Assumptions::is_rational(const RCP<const Basic> &symbol) const
159 {
160  bool rational = rational_symbols_.find(symbol) != rational_symbols_.end();
161  return rational ? tribool::tritrue : tribool::indeterminate;
162 }
163 
164 tribool Assumptions::is_integer(const RCP<const Basic> &symbol) const
165 {
166  bool integer = integer_symbols_.find(symbol) != integer_symbols_.end();
167  return integer ? tribool::tritrue : tribool::indeterminate;
168 }
169 
170 tribool Assumptions::is_positive(const RCP<const Basic> &symbol) const
171 {
172  return from_map(positive_, symbol);
173 }
174 
175 tribool Assumptions::is_nonnegative(const RCP<const Basic> &symbol) const
176 {
177  return from_map(nonnegative_, symbol);
178 }
179 
180 tribool Assumptions::is_negative(const RCP<const Basic> &symbol) const
181 {
182  return from_map(negative_, symbol);
183 }
184 
185 tribool Assumptions::is_nonpositive(const RCP<const Basic> &symbol) const
186 {
187  return from_map(nonpositive_, symbol);
188 }
189 
190 tribool Assumptions::is_nonzero(const RCP<const Basic> &symbol) const
191 {
192  return from_map(nonzero_, symbol);
193 }
194 
195 tribool Assumptions::is_zero(const RCP<const Basic> &symbol) const
196 {
197  return from_map(zero_, symbol);
198 }
199 
200 } // namespace SymEngine
T end(T... args)
T find(T... args)
T insert(T... args)
Main namespace for SymEngine package.
Definition: add.cpp:19
bool is_a_Number(const Basic &b)
Definition: number.h:130
std::enable_if< std::is_integral< T >::value, RCP< const Integer > >::type integer(T i)
Definition: integer.h:200
RCP< const Symbol > symbol(const std::string &name)
inline version to return Symbol
Definition: symbol.h:82
RCP< const Number > rational(long n, long d)
convenience creator from two longs
Definition: rational.h:328