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