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 |
|
* Implements a way to track the origins of ICP-style contractions. |
14 |
|
*/ |
15 |
|
|
16 |
|
#ifndef CVC5__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H |
17 |
|
#define CVC5__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H |
18 |
|
|
19 |
|
#include <memory> |
20 |
|
#include <vector> |
21 |
|
|
22 |
|
#include "expr/node.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace theory { |
26 |
|
namespace arith { |
27 |
|
namespace nl { |
28 |
|
namespace icp { |
29 |
|
|
30 |
|
/** |
31 |
|
* This class tracks origins of ICP-style contractions of variable intervals. |
32 |
|
* For every variable, it holds one origin object that may recursively depend on |
33 |
|
* previous contraction origins. Initially, a immediate bound on a variable |
34 |
|
* (like x>0) yields an origin for this variable. For every contraction, we then |
35 |
|
* add a new origin that recursively holds the old origins, usually those of all |
36 |
|
* variables involved in the contraction. When generating a conflict or a lemma, |
37 |
|
* a recursive walk through this structure allow to retrieve all input theory |
38 |
|
* atoms that contributed to the new fact or the conflict. |
39 |
|
*/ |
40 |
10548 |
class ContractionOriginManager |
41 |
|
{ |
42 |
|
public: |
43 |
|
/** |
44 |
|
* Origin of one particular contraction step. |
45 |
|
* Usually, this is either a direct bound or the application of a contraction |
46 |
|
* candidate. The direct bound is stored in the candidate while origins |
47 |
|
* remains empty. The contraction candidate is stored in the candidate while |
48 |
|
* origins hold the origins of all variables used in the contraction. |
49 |
|
*/ |
50 |
158 |
struct ContractionOrigin |
51 |
|
{ |
52 |
|
/** The theory atom used to do this contraction. */ |
53 |
|
Node candidate; |
54 |
|
/** All origins required for this contraction. */ |
55 |
|
std::vector<ContractionOrigin*> origins; |
56 |
|
}; |
57 |
|
|
58 |
|
private: |
59 |
|
/** |
60 |
|
* Recursively walks through the data structure, collecting all theory atoms. |
61 |
|
*/ |
62 |
|
void getOrigins(ContractionOrigin const* const origin, |
63 |
|
std::set<Node>& res) const; |
64 |
|
|
65 |
|
public: |
66 |
|
/** Return the current origins for all variables. */ |
67 |
|
const std::map<Node, ContractionOrigin*>& currentOrigins() const; |
68 |
|
/** |
69 |
|
* Add a new contraction for the targetVariable. |
70 |
|
* Adds a new origin with the given candidate and origins. |
71 |
|
* If addTarget is set to true, we also add the current origin of the |
72 |
|
* targetVariable to origins. This corresponds to whether we intersected the |
73 |
|
* new interval with the previous interval, or whether the new interval was a |
74 |
|
* subset of the previous one in the first place. |
75 |
|
*/ |
76 |
|
void add(const Node& targetVariable, |
77 |
|
const Node& candidate, |
78 |
|
const std::vector<Node>& originVariables, |
79 |
|
bool addTarget = true); |
80 |
|
|
81 |
|
/** |
82 |
|
* Collect all theory atoms from the origins of the given variable. |
83 |
|
*/ |
84 |
|
std::vector<Node> getOrigins(const Node& variable) const; |
85 |
|
|
86 |
|
/** Check whether a node c is among the origins of a variable. */ |
87 |
|
bool isInOrigins(const Node& variable, const Node& c) const; |
88 |
|
|
89 |
|
private: |
90 |
|
/** The current origins for every variable. */ |
91 |
|
std::map<Node, ContractionOrigin*> d_currentOrigins; |
92 |
|
/** All allocated origins to allow for proper deallocation. */ |
93 |
|
std::vector<std::unique_ptr<ContractionOrigin>> d_allocations; |
94 |
|
}; |
95 |
|
|
96 |
|
/** Stream the constration origins to an ostream. */ |
97 |
|
std::ostream& operator<<(std::ostream& os, const ContractionOriginManager& com); |
98 |
|
|
99 |
|
} // namespace icp |
100 |
|
} // namespace nl |
101 |
|
} // namespace arith |
102 |
|
} // namespace theory |
103 |
|
} // namespace cvc5 |
104 |
|
|
105 |
|
#endif |