Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * [[ Add one-line brief description here ]]
11 : : *
12 : : * [[ Add lengthier description here ]]
13 : : * \todo document this file
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #pragma once
19 : :
20 : : #include <map>
21 : : #include <memory>
22 : : #include <set>
23 : : #include <unordered_map>
24 : :
25 : : #include "expr/kind.h"
26 : : #include "theory/arith/linear/arithvar.h"
27 : : #include "theory/arith/linear/constraint_forward.h"
28 : : #include "util/dense_map.h"
29 : :
30 : : namespace cvc5::internal {
31 : : namespace theory {
32 : : namespace arith::linear {
33 : :
34 : : /** A low level vector of indexed doubles. */
35 : : struct PrimitiveVec
36 : : {
37 : : int len;
38 : : int* inds;
39 : : double* coeffs;
40 : : PrimitiveVec();
41 : : ~PrimitiveVec();
42 : : bool initialized() const;
43 : : void clear();
44 : : void setup(int l);
45 : : void print(std::ostream& out) const;
46 : : };
47 : : std::ostream& operator<<(std::ostream& os, const PrimitiveVec& pv);
48 : :
49 : : struct DenseVector
50 : : {
51 : : DenseMap<Rational> lhs;
52 : : Rational rhs;
53 : : void purge();
54 : : void print(std::ostream& os) const;
55 : :
56 : : static void print(std::ostream& os, const DenseMap<Rational>& lhs);
57 : : };
58 : :
59 : : /** The different kinds of cuts. */
60 : : enum CutInfoKlass
61 : : {
62 : : MirCutKlass,
63 : : GmiCutKlass,
64 : : BranchCutKlass,
65 : : RowsDeletedKlass,
66 : : UnknownKlass
67 : : };
68 : : std::ostream& operator<<(std::ostream& os, CutInfoKlass kl);
69 : :
70 : : /** A general class for describing a cut. */
71 : : class CutInfo
72 : : {
73 : : protected:
74 : : CutInfoKlass d_klass;
75 : : int d_execOrd;
76 : :
77 : : int d_poolOrd; /* cut's ordinal in the current node pool */
78 : : Kind d_cutType; /* Lowerbound, upperbound or undefined. */
79 : : double d_cutRhs; /* right hand side of the cut */
80 : : PrimitiveVec d_cutVec; /* vector of the cut */
81 : :
82 : : /**
83 : : * The number of rows at the time the cut was made.
84 : : * This is required to descramble indices after the fact!
85 : : */
86 : : int d_mAtCreation;
87 : :
88 : : /** This is the number of structural variables. */
89 : : int d_N;
90 : :
91 : : /** if selected, make this non-zero */
92 : : int d_rowId;
93 : :
94 : : /* If the cut has been successfully created,
95 : : * the cut is stored in exact precision in d_exactPrecision.
96 : : * If the cut has not yet been proven, this is null.
97 : : */
98 : : std::unique_ptr<DenseVector> d_exactPrecision;
99 : :
100 : : std::unique_ptr<ConstraintCPVec> d_explanation;
101 : :
102 : : public:
103 : : CutInfo(CutInfoKlass kl, int cutid, int ordinal);
104 : :
105 : : virtual ~CutInfo();
106 : :
107 : : int getId() const;
108 : :
109 : : int getRowId() const;
110 : : void setRowId(int rid);
111 : :
112 : : void print(std::ostream& out) const;
113 : : // void init_cut(int l);
114 : : PrimitiveVec& getCutVector();
115 : : const PrimitiveVec& getCutVector() const;
116 : :
117 : : Kind getKind() const;
118 : : void setKind(Kind k);
119 : :
120 : : void setRhs(double r);
121 : : double getRhs() const;
122 : :
123 : : CutInfoKlass getKlass() const;
124 : : int poolOrdinal() const;
125 : :
126 : : void setDimensions(int N, int M);
127 : : int getN() const;
128 : : int getMAtCreation() const;
129 : :
130 : : bool operator<(const CutInfo& o) const;
131 : :
132 : : /* Returns true if the cut was successfully made in exact precision.*/
133 : : bool reconstructed() const;
134 : :
135 : : /* Returns true if the cut has an explanation. */
136 : : bool proven() const;
137 : :
138 : : void setReconstruction(const DenseVector& ep);
139 : : void setExplanation(const ConstraintCPVec& ex);
140 : : void swapExplanation(ConstraintCPVec& ex);
141 : :
142 : : const DenseVector& getReconstruction() const;
143 : : const ConstraintCPVec& getExplanation() const;
144 : :
145 : : void clearReconstruction();
146 : : };
147 : : std::ostream& operator<<(std::ostream& os, const CutInfo& ci);
148 : :
149 : : class BranchCutInfo : public CutInfo
150 : : {
151 : : public:
152 : : BranchCutInfo(int execOrd, int br, Kind dir, double val);
153 : : };
154 : :
155 : : class RowsDeleted : public CutInfo
156 : : {
157 : : public:
158 : : RowsDeleted(int execOrd, int nrows, const int num[]);
159 : : };
160 : :
161 : : class TreeLog;
162 : :
163 : : class NodeLog
164 : : {
165 : : private:
166 : : int d_nid;
167 : : NodeLog* d_parent; /* If null this is the root */
168 : : TreeLog* d_tl; /* TreeLog containing the node. */
169 : :
170 : : struct CmpCutPointer
171 : : {
172 : 34266 : int operator()(const CutInfo* a, const CutInfo* b) const { return *a < *b; }
173 : : };
174 : : typedef std::set<CutInfo*, CmpCutPointer> CutSet;
175 : : CutSet d_cuts;
176 : : std::map<int, int> d_rowIdsSelected;
177 : :
178 : : enum Status
179 : : {
180 : : Open,
181 : : Closed,
182 : : Branched
183 : : };
184 : : Status d_stat;
185 : :
186 : : int d_brVar; // branching variable
187 : : double d_brVal;
188 : : int d_downId;
189 : : int d_upId;
190 : :
191 : : public:
192 : : typedef std::unordered_map<int, ArithVar> RowIdMap;
193 : :
194 : : private:
195 : : RowIdMap d_rowId2ArithVar;
196 : :
197 : : public:
198 : : NodeLog(); /* default constructor. */
199 : : NodeLog(TreeLog* tl, int node, const RowIdMap& m); /* makes a root node. */
200 : : NodeLog(TreeLog* tl, NodeLog* parent, int node); /* makes a non-root node. */
201 : :
202 : : ~NodeLog();
203 : :
204 : : int getNodeId() const;
205 : : void addSelected(int ord, int sel);
206 : : void applySelected();
207 : : void addCut(CutInfo* ci);
208 : : void print(std::ostream& o) const;
209 : :
210 : : bool isRoot() const;
211 : : const NodeLog& getParent() const;
212 : :
213 : : void copyParentRowIds();
214 : :
215 : : bool isBranch() const;
216 : : int branchVariable() const;
217 : : double branchValue() const;
218 : :
219 : : typedef CutSet::const_iterator const_iterator;
220 : : const_iterator begin() const;
221 : : const_iterator end() const;
222 : :
223 : : void setBranch(int br, double val, int dn, int up);
224 : : void closeNode();
225 : :
226 : : int getDownId() const;
227 : : int getUpId() const;
228 : :
229 : : /**
230 : : * Looks up a row id to the appropriate arith variable.
231 : : * Be careful these are deleted in context during replay!
232 : : * failure returns ARITHVAR_SENTINEL */
233 : : ArithVar lookupRowId(int rowId) const;
234 : :
235 : : /**
236 : : * Maps a row id to an arithvar.
237 : : * Be careful these are deleted in context during replay!
238 : : */
239 : : void mapRowId(int rowid, ArithVar v);
240 : : void applyRowsDeleted(const RowsDeleted& rd);
241 : : };
242 : : std::ostream& operator<<(std::ostream& os, const NodeLog& nl);
243 : :
244 : : class TreeLog
245 : : {
246 : : private:
247 : : int next_exec_ord;
248 : : typedef std::map<int, NodeLog> ToNodeMap;
249 : : ToNodeMap d_toNode;
250 : : DenseMultiset d_branches;
251 : :
252 : : uint32_t d_numCuts;
253 : :
254 : : bool d_active;
255 : :
256 : : public:
257 : : TreeLog();
258 : :
259 : : NodeLog& getNode(int nid);
260 : : void branch(int nid, int br, double val, int dn, int up);
261 : : void close(int nid);
262 : :
263 : : // void applySelected();
264 : : void print(std::ostream& o) const;
265 : :
266 : : typedef ToNodeMap::const_iterator const_iterator;
267 : : const_iterator begin() const;
268 : : const_iterator end() const;
269 : :
270 : : int getExecutionOrd();
271 : :
272 : : void reset(const NodeLog::RowIdMap& m);
273 : :
274 : : // Applies rd tp to the node with id nid
275 : : void applyRowsDeleted(int nid, const RowsDeleted& rd);
276 : :
277 : : // Synonym for getNode(nid).mapRowId(ind, v)
278 : : void mapRowId(int nid, int ind, ArithVar v);
279 : :
280 : : private:
281 : : void clear();
282 : :
283 : : public:
284 : : void makeInactive();
285 : : void makeActive();
286 : :
287 : : bool isActivelyLogging() const;
288 : :
289 : : void addCut();
290 : : uint32_t cutCount() const;
291 : :
292 : : void logBranch(uint32_t x);
293 : : uint32_t numBranches(uint32_t x);
294 : :
295 : : int getRootId() const;
296 : :
297 : : uint32_t numNodes() const { return d_toNode.size(); }
298 : :
299 : : NodeLog& getRootNode();
300 : : void printBranchInfo(std::ostream& os) const;
301 : : };
302 : :
303 : : } // namespace arith::linear
304 : : } // namespace theory
305 : : } // namespace cvc5::internal
|
