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 |
|
* Extract bounds on variables from theory atoms. |
14 |
|
*/ |
15 |
|
|
16 |
|
#ifndef CVC5__THEORY__ARITH__BOUND_INFERENCE_H |
17 |
|
#define CVC5__THEORY__ARITH__BOUND_INFERENCE_H |
18 |
|
|
19 |
|
#include <map> |
20 |
|
#include <utility> |
21 |
|
#include <vector> |
22 |
|
|
23 |
|
#include "expr/node.h" |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
namespace theory { |
27 |
|
namespace arith { |
28 |
|
|
29 |
526540 |
struct Bounds |
30 |
|
{ |
31 |
|
/** The lower bound value */ |
32 |
|
Node lower_value; |
33 |
|
/** Whether the lower bound is strict or weak */ |
34 |
|
bool lower_strict = true; |
35 |
|
/** The lower bound as constraint */ |
36 |
|
Node lower_bound; |
37 |
|
/** The origin of the lower bound */ |
38 |
|
Node lower_origin; |
39 |
|
/** The upper bound value */ |
40 |
|
Node upper_value; |
41 |
|
/** Whether the upper bound is strict or weak */ |
42 |
|
bool upper_strict = true; |
43 |
|
/** The upper bound as constraint */ |
44 |
|
Node upper_bound; |
45 |
|
/** The origin of the upper bound */ |
46 |
|
Node upper_origin; |
47 |
|
}; |
48 |
|
|
49 |
|
/** Print the current bounds. */ |
50 |
|
std::ostream& operator<<(std::ostream& os, const Bounds& b); |
51 |
|
|
52 |
|
/** |
53 |
|
* A utility class that extracts direct bounds on arithmetic terms from theory |
54 |
|
* atoms. |
55 |
|
*/ |
56 |
16420 |
class BoundInference |
57 |
|
{ |
58 |
|
public: |
59 |
|
void reset(); |
60 |
|
|
61 |
|
/** |
62 |
|
* Get the current interval for lhs. Creates a new (full) interval if |
63 |
|
* necessary. |
64 |
|
*/ |
65 |
|
Bounds& get_or_add(const Node& lhs); |
66 |
|
/** |
67 |
|
* Get the current interval for lhs. Returns a full interval if no interval |
68 |
|
* was derived yet. |
69 |
|
*/ |
70 |
|
Bounds get(const Node& lhs) const; |
71 |
|
|
72 |
|
/** Return the current term bounds as an interval assignment. */ |
73 |
|
const std::map<Node, Bounds>& get() const; |
74 |
|
|
75 |
|
/** |
76 |
|
* Add a new theory atom. Return true if the theory atom induces a new |
77 |
|
* term bound. |
78 |
|
* If onlyVariables is true, the left hand side needs to be a single |
79 |
|
* variable to induce a bound. |
80 |
|
*/ |
81 |
|
bool add(const Node& n, bool onlyVariables = true); |
82 |
|
|
83 |
|
/** |
84 |
|
* Post-processes a set of nodes and replaces bounds by their origins. |
85 |
|
* This utility sometimes creates new bounds, either due to tightening of |
86 |
|
* integer terms or because an equality was derived from two weak |
87 |
|
* inequalities. While the origins of these new bounds are recorded in |
88 |
|
* lower_origin and upper_origin, this method can be used to conveniently |
89 |
|
* replace these new nodes by their origins. |
90 |
|
* This can be used, for example, when constructing conflicts. |
91 |
|
*/ |
92 |
|
void replaceByOrigins(std::vector<Node>& nodes) const; |
93 |
|
|
94 |
|
private: |
95 |
|
/** The currently strictest bounds for every lhs. */ |
96 |
|
std::map<Node, Bounds> d_bounds; |
97 |
|
|
98 |
|
/** Updates the lower bound for the given lhs */ |
99 |
|
void update_lower_bound(const Node& origin, |
100 |
|
const Node& lhs, |
101 |
|
const Node& value, |
102 |
|
bool strict); |
103 |
|
/** Updates the upper bound for the given lhs */ |
104 |
|
void update_upper_bound(const Node& origin, |
105 |
|
const Node& lhs, |
106 |
|
const Node& value, |
107 |
|
bool strict); |
108 |
|
}; |
109 |
|
|
110 |
|
/** Print the current variable bounds. */ |
111 |
|
std::ostream& operator<<(std::ostream& os, const BoundInference& bi); |
112 |
|
|
113 |
|
std::map<Node, std::pair<Node,Node>> getBounds(const std::vector<Node>& assertions); |
114 |
|
|
115 |
|
} // namespace arith |
116 |
|
} // namespace theory |
117 |
|
} // namespace cvc5 |
118 |
|
|
119 |
|
#endif |