Loading...
Searching...
No Matches
assumptions.cpp
1#include <symengine/logic.h>
2#include <symengine/assumptions.h>
3#include <symengine/number.h>
4
5namespace SymEngine
6{
7
8Assumptions::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<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();
37 if (is_a<Symbol>(*arg2) and is_a_Number(*arg1)) {
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();
69 if (is_a<Symbol>(*arg2) and is_a_Number(*arg1)) {
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();
94 if (is_a_Number(*arg1) and is_a<Symbol>(*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();
115 if (is_a_Number(*arg1) and is_a<Symbol>(*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}
124
125void Assumptions::set_map(umap_basic_bool &map, const RCP<const Basic> &symbol,
126 bool value)
127{
128 // Set element in map to true or false. Check for consistency within map
129 tribool old_value = from_map(map, symbol);
130 if ((is_true(old_value) and not value) or (is_false(old_value) and value)) {
131 throw SymEngineException("Symbol " + symbol->__str__()
132 + " have inconsistent positive/negativeness");
133 }
134 map[symbol] = value;
135}
136
137tribool Assumptions::from_map(const umap_basic_bool &map,
138 const RCP<const Basic> &symbol) const
139{
140 auto it = map.find(symbol);
141 if (it != map.end()) {
142 return (tribool)((*it).second);
143 } else {
144 return tribool::indeterminate;
145 }
146}
147
148tribool Assumptions::is_complex(const RCP<const Basic> &symbol) const
149{
150 bool cmplx = complex_symbols_.find(symbol) != complex_symbols_.end();
151 return cmplx ? tribool::tritrue : tribool::indeterminate;
152}
153
154tribool Assumptions::is_real(const RCP<const Basic> &symbol) const
155{
156 bool real = real_symbols_.find(symbol) != real_symbols_.end();
157 return real ? tribool::tritrue : tribool::indeterminate;
158}
159
160tribool Assumptions::is_rational(const RCP<const Basic> &symbol) const
161{
162 bool rational = rational_symbols_.find(symbol) != rational_symbols_.end();
163 return rational ? tribool::tritrue : tribool::indeterminate;
164}
165
166tribool Assumptions::is_integer(const RCP<const Basic> &symbol) const
167{
168 bool integer = integer_symbols_.find(symbol) != integer_symbols_.end();
169 return integer ? tribool::tritrue : tribool::indeterminate;
170}
171
172tribool Assumptions::is_positive(const RCP<const Basic> &symbol) const
173{
174 return from_map(positive_, symbol);
175}
176
177tribool Assumptions::is_nonnegative(const RCP<const Basic> &symbol) const
178{
179 return from_map(nonnegative_, symbol);
180}
181
182tribool Assumptions::is_negative(const RCP<const Basic> &symbol) const
183{
184 return from_map(negative_, symbol);
185}
186
187tribool Assumptions::is_nonpositive(const RCP<const Basic> &symbol) const
188{
189 return from_map(nonpositive_, symbol);
190}
191
192tribool Assumptions::is_nonzero(const RCP<const Basic> &symbol) const
193{
194 return from_map(nonzero_, symbol);
195}
196
197tribool Assumptions::is_zero(const RCP<const Basic> &symbol) const
198{
199 return from_map(zero_, symbol);
200}
201
202} // 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
RCP< const Number > rational(long n, long d)
convenience creator from two longs
Definition: rational.h:328
RCP< const Symbol > symbol(const std::string &name)
inline version to return Symbol
Definition: symbol.h:82
std::enable_if< std::is_integral< T >::value, RCP< constInteger > >::type integer(T i)
Definition: integer.h:197