1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Gereon Kremer, Andres Noetzli |
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 ICP-based solver for nonlinear arithmetic. |
14 |
|
*/ |
15 |
|
|
16 |
|
#ifndef CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H |
17 |
|
#define CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H |
18 |
|
|
19 |
|
#include "cvc5_private.h" |
20 |
|
|
21 |
|
#ifdef CVC5_POLY_IMP |
22 |
|
#include <poly/polyxx.h> |
23 |
|
#endif /* CVC5_POLY_IMP */ |
24 |
|
|
25 |
|
#include "expr/node.h" |
26 |
|
#include "theory/arith/bound_inference.h" |
27 |
|
#include "theory/arith/nl/icp/candidate.h" |
28 |
|
#include "theory/arith/nl/icp/contraction_origins.h" |
29 |
|
#include "theory/arith/nl/icp/intersection.h" |
30 |
|
#include "theory/arith/nl/poly_conversion.h" |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
namespace theory { |
34 |
|
namespace arith { |
35 |
|
|
36 |
|
class InferenceManager; |
37 |
|
|
38 |
|
namespace nl { |
39 |
|
namespace icp { |
40 |
|
|
41 |
|
#ifdef CVC5_POLY_IMP |
42 |
|
|
43 |
|
/** |
44 |
|
* This class implements an ICP-based solver. As it is intended to be used in |
45 |
|
* conjunction with other solvers, it only performs contractions, but does not |
46 |
|
* issue splits. |
47 |
|
* |
48 |
|
* In essence, interval constraint propagation has candidates (like x = y^2-z), |
49 |
|
* evaluates their right hand side over the current (interval) assignment and |
50 |
|
* uses the resulting interval to make the interval of the left-hand side |
51 |
|
* variable smaller (contract it). |
52 |
|
* |
53 |
|
* These contractions can yield to a conflict (if the interval of some variable |
54 |
|
* becomes empty) or shrink the search space for a variable. |
55 |
|
*/ |
56 |
4914 |
class ICPSolver |
57 |
|
{ |
58 |
|
/** |
59 |
|
* This encapsulates the state of the ICP solver that is local to a single |
60 |
|
* theory call. It contains the variable bounds and candidates derived from |
61 |
|
* the assertions, the origins manager and the last conflict. |
62 |
|
*/ |
63 |
4914 |
struct ICPState |
64 |
|
{ |
65 |
|
/** The variable bounds extracted from the input assertions */ |
66 |
|
BoundInference d_bounds; |
67 |
|
/** The contraction candidates generated from the theory atoms */ |
68 |
|
std::vector<Candidate> d_candidates; |
69 |
|
/** The current assignment */ |
70 |
|
poly::IntervalAssignment d_assignment; |
71 |
|
/** The origins for the current assignment */ |
72 |
|
ContractionOriginManager d_origins; |
73 |
|
/** The conflict, if any way found. Initially empty */ |
74 |
|
std::vector<Node> d_conflict; |
75 |
|
|
76 |
|
/** Initialized the variable bounds with a variable mapper */ |
77 |
4914 |
ICPState(VariableMapper& vm) {} |
78 |
|
|
79 |
|
/** Reset this state */ |
80 |
32 |
void reset() |
81 |
|
{ |
82 |
32 |
d_bounds = BoundInference(); |
83 |
32 |
d_candidates.clear(); |
84 |
32 |
d_assignment.clear(); |
85 |
32 |
d_origins = ContractionOriginManager(); |
86 |
32 |
d_conflict.clear(); |
87 |
32 |
} |
88 |
|
}; |
89 |
|
|
90 |
|
/** Maps Node (variables) to poly::Variable */ |
91 |
|
VariableMapper d_mapper; |
92 |
|
/** The inference manager */ |
93 |
|
InferenceManager& d_im; |
94 |
|
/** Cache candidates to avoid reconstruction for every theory call */ |
95 |
|
std::map<Node, std::vector<Candidate>> d_candidateCache; |
96 |
|
/** The current state */ |
97 |
|
ICPState d_state; |
98 |
|
|
99 |
|
/** The remaining budget */ |
100 |
|
std::int64_t d_budget = 0; |
101 |
|
/** The budget increment for new candidates and strong contractions */ |
102 |
|
static constexpr std::int64_t d_budgetIncrement = 10; |
103 |
|
|
104 |
|
/** Collect all variables from a node */ |
105 |
|
std::vector<Node> collectVariables(const Node& n) const; |
106 |
|
/** Construct all possible candidates from a given theory atom */ |
107 |
|
std::vector<Candidate> constructCandidates(const Node& n); |
108 |
|
/** Add the given node as candidate */ |
109 |
|
void addCandidate(const Node& n); |
110 |
|
/** Initialize the origin manager from the variable bounds */ |
111 |
|
void initOrigins(); |
112 |
|
|
113 |
|
/** |
114 |
|
* Perform one contraction with every candidate. |
115 |
|
* If any candidate yields a conflict stops immediately and returns |
116 |
|
* PropagationResult::CONFLICT. If any candidate yields a contraction returns |
117 |
|
* PropagationResult::CONTRACTED. Otherwise returns |
118 |
|
* PropagationResult::NOT_CHANGED. |
119 |
|
*/ |
120 |
|
PropagationResult doPropagationRound(); |
121 |
|
|
122 |
|
/** |
123 |
|
* Construct lemmas for all bounds that have been improved. |
124 |
|
* For every improved bound, all origins are collected and a lemma of the form |
125 |
|
* (and origins) ==> (new bound) |
126 |
|
* is constructed. |
127 |
|
*/ |
128 |
|
std::vector<Node> generateLemmas() const; |
129 |
|
|
130 |
|
public: |
131 |
4914 |
ICPSolver(InferenceManager& im) : d_im(im), d_state(d_mapper) {} |
132 |
|
/** Reset this solver for the next theory call */ |
133 |
|
void reset(const std::vector<Node>& assertions); |
134 |
|
|
135 |
|
/** |
136 |
|
* Performs a full ICP check. |
137 |
|
*/ |
138 |
|
void check(); |
139 |
|
}; |
140 |
|
|
141 |
|
#else /* CVC5_POLY_IMP */ |
142 |
|
|
143 |
|
class ICPSolver |
144 |
|
{ |
145 |
|
public: |
146 |
|
ICPSolver(InferenceManager& im) {} |
147 |
|
void reset(const std::vector<Node>& assertions); |
148 |
|
void check(); |
149 |
|
}; |
150 |
|
|
151 |
|
#endif /* CVC5_POLY_IMP */ |
152 |
|
|
153 |
|
} // namespace icp |
154 |
|
} // namespace nl |
155 |
|
} // namespace arith |
156 |
|
} // namespace theory |
157 |
|
} // namespace cvc5 |
158 |
|
|
159 |
|
#endif |