1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Represents a contraction candidate for ICP-style propagation. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/arith/nl/icp/candidate.h" |
17 |
|
|
18 |
|
#ifdef CVC5_POLY_IMP |
19 |
|
|
20 |
|
#include <iostream> |
21 |
|
|
22 |
|
#include "base/check.h" |
23 |
|
#include "base/output.h" |
24 |
|
#include "theory/arith/nl/icp/intersection.h" |
25 |
|
#include "theory/arith/nl/poly_conversion.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace theory { |
29 |
|
namespace arith { |
30 |
|
namespace nl { |
31 |
|
namespace icp { |
32 |
|
|
33 |
118 |
PropagationResult Candidate::propagate(poly::IntervalAssignment& ia, |
34 |
|
std::size_t size_threshold) const |
35 |
|
{ |
36 |
|
// Evaluate the right hand side |
37 |
236 |
auto res = poly::evaluate(rhs, ia) * poly::Interval(poly::Value(rhsmult)); |
38 |
354 |
if (get_lower(res) == poly::Value::minus_infty() |
39 |
354 |
&& get_upper(res) == poly::Value::plus_infty()) |
40 |
|
{ |
41 |
30 |
return PropagationResult::NOT_CHANGED; |
42 |
|
} |
43 |
88 |
Trace("nl-icp") << "Prop: " << *this << " -> " << res << std::endl; |
44 |
|
// Remove bounds based on the sign condition |
45 |
88 |
switch (rel) |
46 |
|
{ |
47 |
16 |
case poly::SignCondition::LT: |
48 |
16 |
res.set_lower(poly::Value::minus_infty(), true); |
49 |
16 |
res.set_upper(get_upper(res), true); |
50 |
16 |
break; |
51 |
|
case poly::SignCondition::LE: |
52 |
|
res.set_lower(poly::Value::minus_infty(), true); |
53 |
|
break; |
54 |
42 |
case poly::SignCondition::EQ: break; |
55 |
|
case poly::SignCondition::NE: Assert(false); break; |
56 |
30 |
case poly::SignCondition::GT: |
57 |
30 |
res.set_lower(get_lower(res), true); |
58 |
30 |
res.set_upper(poly::Value::plus_infty(), true); |
59 |
30 |
break; |
60 |
|
case poly::SignCondition::GE: |
61 |
|
res.set_upper(poly::Value::plus_infty(), true); |
62 |
|
break; |
63 |
|
} |
64 |
|
// Get the current interval for lhs |
65 |
176 |
auto cur = ia.get(lhs); |
66 |
|
|
67 |
|
// Update the current interval |
68 |
88 |
PropagationResult result = intersect_interval_with(cur, res, size_threshold); |
69 |
|
// Check for strong propagations |
70 |
88 |
switch (result) |
71 |
|
{ |
72 |
4 |
case PropagationResult::CONTRACTED: |
73 |
|
case PropagationResult::CONTRACTED_WITHOUT_CURRENT: |
74 |
|
{ |
75 |
8 |
Trace("nl-icp") << *this << " contracted " << lhs << " -> " << cur |
76 |
4 |
<< std::endl; |
77 |
8 |
auto old = ia.get(lhs); |
78 |
4 |
bool strong = false; |
79 |
4 |
strong = strong |
80 |
4 |
|| (is_minus_infinity(get_lower(old)) |
81 |
|
&& !is_minus_infinity(get_lower(cur))); |
82 |
4 |
strong = strong |
83 |
6 |
|| (is_plus_infinity(get_upper(old)) |
84 |
2 |
&& !is_plus_infinity(get_upper(cur))); |
85 |
4 |
ia.set(lhs, cur); |
86 |
4 |
if (strong) |
87 |
|
{ |
88 |
2 |
if (result == PropagationResult::CONTRACTED) |
89 |
|
{ |
90 |
|
result = PropagationResult::CONTRACTED_STRONGLY; |
91 |
|
} |
92 |
2 |
else if (result == PropagationResult::CONTRACTED_WITHOUT_CURRENT) |
93 |
|
{ |
94 |
2 |
result = PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT; |
95 |
|
} |
96 |
|
} |
97 |
4 |
break; |
98 |
|
} |
99 |
|
case PropagationResult::CONTRACTED_STRONGLY: |
100 |
|
case PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT: |
101 |
|
Assert(false) << "This method should not return strong flags."; |
102 |
|
break; |
103 |
84 |
default: break; |
104 |
|
} |
105 |
88 |
return result; |
106 |
|
} |
107 |
|
|
108 |
|
std::ostream& operator<<(std::ostream& os, const Candidate& c) |
109 |
|
{ |
110 |
|
os << c.lhs << " " << c.rel << " "; |
111 |
|
if (c.rhsmult != poly::Rational(1)) os << c.rhsmult << " * "; |
112 |
|
return os << c.rhs; |
113 |
|
} |
114 |
|
|
115 |
|
} // namespace icp |
116 |
|
} // namespace nl |
117 |
|
} // namespace arith |
118 |
|
} // namespace theory |
119 |
29358 |
} // namespace cvc5 |
120 |
|
|
121 |
|
#endif |