LMCAS
Lamina Computer Algebra System
载入中...
搜索中...
未找到
inference_engine_sign_queries.cpp
浏览该文件的文档.
1#define _USE_MATH_DEFINES
3
4namespace LMCAS {
5
6InferenceTriboolResult InferenceEngine::query_positive_checked(const SymbolicExpr& expr) const {
7 ComputationContext context;
8 return query_positive_checked(expr, context);
9}
10
11InferenceTriboolResult InferenceEngine::query_positive_checked(const SymbolicExpr& expr, ComputationContext& context) const {
12 return checked_inference_result<Tribool>(expr, "query_positive_checked", context,
13 [&]() -> InferenceTriboolResult {
14 const int infinity = infinity_sign(expr, context);
15 if (infinity != 0) {
17 infinity > 0 ? Tribool::True : Tribool::False);
18 }
19 DepthGuard guard(*this, *LMCAS::detail::node(expr));
20 if (guard.should_abort()) {
21 return Tribool::Unknown;
22 }
23
24 if (auto num = std::dynamic_pointer_cast<const NumberNode>(LMCAS::detail::node(expr))) {
25 return Impl::number_positive(*num);
26 }
27 if (auto var = std::dynamic_pointer_cast<const VariableNode>(LMCAS::detail::node(expr))) {
28 if (var->is_constant()) return Tribool::True;
29 const auto& props = impl_->ctx;
30 if (props.has_sign(var->name(), Sign::Positive)) {
31 return Tribool::True;
32 }
33 if (props.has_sign(var->name(), Sign::Negative) ||
34 props.has_sign(var->name(), Sign::Zero) ||
35 props.has_sign(var->name(), Sign::NonPositive)) {
36 return Tribool::False;
37 }
38 if (props.has_domain(var->name(), Domain::PositiveInt)) {
39 return Tribool::True;
40 }
41 return Tribool::Unknown;
42 }
43
44 return impl_->composite_positive(*this, expr, context);
45 });
46}
47
48InferenceTriboolResult InferenceEngine::query_negative_checked(const SymbolicExpr& expr) const {
49 ComputationContext context;
50 return query_negative_checked(expr, context);
51}
52
53InferenceTriboolResult InferenceEngine::query_negative_checked(const SymbolicExpr& expr, ComputationContext& context) const {
54 return checked_inference_result<Tribool>(expr, "query_negative_checked", context,
55 [&]() -> InferenceTriboolResult {
56 const int infinity = infinity_sign(expr, context);
57 if (infinity != 0) {
59 infinity < 0 ? Tribool::True : Tribool::False);
60 }
61 DepthGuard guard(*this, *LMCAS::detail::node(expr));
62 if (guard.should_abort()) {
63 return Tribool::Unknown;
64 }
65
66 if (auto num = std::dynamic_pointer_cast<const NumberNode>(LMCAS::detail::node(expr))) {
67 return Impl::number_negative(*num);
68 }
69
70 if (auto var = std::dynamic_pointer_cast<const VariableNode>(LMCAS::detail::node(expr))) {
71 if (var->is_constant()) return Tribool::False;
72 const auto& props = impl_->ctx;
73 if (props.has_sign(var->name(), Sign::Negative)) {
74 return Tribool::True;
75 }
76 if (props.has_sign(var->name(), Sign::Positive) ||
77 props.has_sign(var->name(), Sign::Zero) ||
78 props.has_sign(var->name(), Sign::NonNegative)) {
79 return Tribool::False;
80 }
81 return Tribool::Unknown;
82 }
83
84 return impl_->composite_negative(*this, expr, context);
85 });
86}
87
88InferenceTriboolResult InferenceEngine::query_nonnegative_checked(const SymbolicExpr& expr) const {
89 ComputationContext context;
90 return query_nonnegative_checked(expr, context);
91}
92
93InferenceTriboolResult InferenceEngine::query_nonnegative_checked(const SymbolicExpr& expr, ComputationContext& context) const {
94 return checked_inference_result<Tribool>(expr, "query_nonnegative_checked", context,
95 [&]() -> InferenceTriboolResult {
96 const int infinity = infinity_sign(expr, context);
97 if (infinity != 0) {
99 infinity > 0 ? Tribool::True : Tribool::False);
100 }
101 DepthGuard guard(*this, *LMCAS::detail::node(expr));
102 if (guard.should_abort()) {
103 return Tribool::Unknown;
104 }
105
106 if (auto num = std::dynamic_pointer_cast<const NumberNode>(LMCAS::detail::node(expr))) {
107 return Impl::number_nonnegative(*num);
108 }
109
110 if (auto var = std::dynamic_pointer_cast<const VariableNode>(LMCAS::detail::node(expr))) {
111 if (var->is_constant()) return Tribool::True;
112 const auto& props = impl_->ctx;
113 if (props.has_sign(var->name(), Sign::NonNegative)) {
114 return Tribool::True;
115 }
116 if (props.has_sign(var->name(), Sign::Negative)) {
117 return Tribool::False;
118 }
119 return Tribool::Unknown;
120 }
121
122 return impl_->composite_nonnegative(*this, expr, context);
123 });
124}
125
126InferenceTriboolResult InferenceEngine::query_nonpositive_checked(const SymbolicExpr& expr) const {
127 ComputationContext context;
128 return query_nonpositive_checked(expr, context);
129}
130
131InferenceTriboolResult InferenceEngine::query_nonpositive_checked(const SymbolicExpr& expr, ComputationContext& context) const {
132 return checked_inference_result<Tribool>(expr, "query_nonpositive_checked", context,
133 [&]() -> InferenceTriboolResult {
134 DepthGuard guard(*this, *LMCAS::detail::node(expr));
135 if (guard.should_abort()) {
136 return Tribool::Unknown;
137 }
138
139 if (auto num = std::dynamic_pointer_cast<const NumberNode>(LMCAS::detail::node(expr))) {
140 return Impl::number_nonpositive(*num);
141 }
142
143 if (auto var = std::dynamic_pointer_cast<const VariableNode>(LMCAS::detail::node(expr))) {
144 if (var->is_constant()) return Tribool::False;
145 const auto& props = impl_->ctx;
146 if (props.has_sign(var->name(), Sign::NonPositive)) {
147 return Tribool::True;
148 }
149 if (props.has_sign(var->name(), Sign::Positive)) {
150 return Tribool::False;
151 }
152 return Tribool::Unknown;
153 }
154
155 return impl_->composite_nonpositive(*this, expr, context);
156 });
157}
158
159InferenceTriboolResult InferenceEngine::query_nonzero_checked(const SymbolicExpr& expr) const {
160 ComputationContext context;
161 return query_nonzero_checked(expr, context);
162}
163
164InferenceTriboolResult InferenceEngine::query_nonzero_checked(const SymbolicExpr& expr, ComputationContext& context) const {
165 return checked_inference_result<Tribool>(expr, "query_nonzero_checked", context,
166 [&]() -> InferenceTriboolResult {
167 if (infinity_sign(expr, context) != 0) {
169 }
170 DepthGuard guard(*this, *LMCAS::detail::node(expr));
171 if (guard.should_abort()) {
172 return Tribool::Unknown;
173 }
174
175 if (auto num = std::dynamic_pointer_cast<const NumberNode>(LMCAS::detail::node(expr))) {
176 return Impl::number_nonzero(*num);
177 }
178
179 if (auto var = std::dynamic_pointer_cast<const VariableNode>(LMCAS::detail::node(expr))) {
180 if (var->is_constant()) return Tribool::True;
181 const auto& props = impl_->ctx;
182 if (props.has_sign(var->name(), Sign::NonZero)) {
183 return Tribool::True;
184 }
185 if (props.has_sign(var->name(), Sign::Zero)) {
186 return Tribool::False;
187 }
188 return Tribool::Unknown;
189 }
190
191 return impl_->composite_nonzero(*this, expr, context);
192 });
193}
194
195}
static Result success(Tribool value)
const SymbolicNodePtr & node(const ::LMCAS::SymbolicExpr &expression) noexcept
std::shared_ptr< SymbolicExpr > num(int value)
const std::vector< Polynomial< BigInt > > const BigInt ComputationContext & context
Result< T > checked_inference_result(const SymbolicExpr &expr, const std::string &operation, ComputationContext &context, const std::function< Result< T >()> &query)
@ PositiveInt
Positive integers (1, 2, 3, ...)
@ Unknown
Property cannot be determined
@ True
Property definitely holds
@ False
Property definitely does not hold
Result< Tribool > InferenceTriboolResult
int infinity_sign(const SymbolicExpr &expression, ComputationContext &context)