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