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 : : */
11 : :
12 : : #include "theory/arith/linear/cut_log.h"
13 : :
14 : : #include <climits>
15 : : #include <cmath>
16 : : #include <iomanip>
17 : : #include <map>
18 : :
19 : : #include "base/cvc5config.h"
20 : : #include "base/output.h"
21 : : #include "theory/arith/linear/approx_simplex.h"
22 : : #include "theory/arith/linear/constraint.h"
23 : : #include "theory/arith/linear/normal_form.h"
24 : : #include "util/ostream_util.h"
25 : :
26 : : using namespace std;
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : : namespace arith::linear {
31 : :
32 : 0 : NodeLog::const_iterator NodeLog::begin() const { return d_cuts.begin(); }
33 : 0 : NodeLog::const_iterator NodeLog::end() const { return d_cuts.end(); }
34 : :
35 : 0 : NodeLog& TreeLog::getNode(int nid)
36 : : {
37 : 0 : ToNodeMap::iterator i = d_toNode.find(nid);
38 : 0 : Assert(i != d_toNode.end());
39 : 0 : return (*i).second;
40 : : }
41 : :
42 : 0 : TreeLog::const_iterator TreeLog::begin() const { return d_toNode.begin(); }
43 : 0 : TreeLog::const_iterator TreeLog::end() const { return d_toNode.end(); }
44 : :
45 : 50 : int TreeLog::getExecutionOrd()
46 : : {
47 : 50 : int res = next_exec_ord;
48 : 50 : ++next_exec_ord;
49 : 50 : return res;
50 : : }
51 : 6 : void TreeLog::makeInactive() { d_active = false; }
52 : 0 : void TreeLog::makeActive() { d_active = true; }
53 : 50 : bool TreeLog::isActivelyLogging() const { return d_active; }
54 : :
55 : 0 : PrimitiveVec::PrimitiveVec() : len(0), inds(nullptr), coeffs(nullptr) {}
56 : :
57 : 0 : PrimitiveVec::~PrimitiveVec() { clear(); }
58 : 0 : bool PrimitiveVec::initialized() const { return inds != nullptr; }
59 : 0 : void PrimitiveVec::clear()
60 : : {
61 [ - - ]: 0 : if (initialized())
62 : : {
63 [ - - ]: 0 : delete[] inds;
64 [ - - ]: 0 : delete[] coeffs;
65 : 0 : len = 0;
66 : 0 : inds = nullptr;
67 : 0 : coeffs = nullptr;
68 : : }
69 : 0 : }
70 : 0 : void PrimitiveVec::setup(int l)
71 : : {
72 : 0 : Assert(!initialized());
73 : 0 : len = l;
74 [ - - ]: 0 : inds = new int[1 + len];
75 [ - - ]: 0 : coeffs = new double[1 + len];
76 : 0 : }
77 : 0 : void PrimitiveVec::print(std::ostream& out) const
78 : : {
79 : 0 : Assert(initialized());
80 : 0 : StreamFormatScope scope(out);
81 : :
82 : 0 : out << len << " " << std::setprecision(15);
83 [ - - ]: 0 : for (int i = 1; i <= len; ++i)
84 : : {
85 : 0 : out << "[" << inds[i] << ", " << coeffs[i] << "]";
86 : : }
87 : 0 : }
88 : 0 : std::ostream& operator<<(std::ostream& os, const PrimitiveVec& pv)
89 : : {
90 : 0 : pv.print(os);
91 : 0 : return os;
92 : : }
93 : :
94 : 0 : CutInfo::CutInfo(CutInfoKlass kl, int eid, int o)
95 : 0 : : d_klass(kl),
96 : 0 : d_execOrd(eid),
97 : 0 : d_poolOrd(o),
98 : 0 : d_cutType(Kind::UNDEFINED_KIND),
99 : 0 : d_cutRhs(),
100 : 0 : d_cutVec(),
101 : 0 : d_mAtCreation(-1),
102 : 0 : d_N(-1),
103 : 0 : d_rowId(-1),
104 : 0 : d_exactPrecision(nullptr),
105 : 0 : d_explanation(nullptr)
106 : : {
107 : 0 : }
108 : :
109 : 0 : CutInfo::~CutInfo() {}
110 : :
111 : 0 : int CutInfo::getId() const { return d_execOrd; }
112 : :
113 : 0 : int CutInfo::getRowId() const { return d_rowId; }
114 : :
115 : 0 : void CutInfo::setRowId(int rid) { d_rowId = rid; }
116 : :
117 : 0 : void CutInfo::print(ostream& out) const
118 : : {
119 : 0 : out << "[CutInfo " << d_execOrd << " " << d_poolOrd << " " << d_klass << " "
120 : 0 : << d_cutType << " " << d_cutRhs << " ";
121 : 0 : d_cutVec.print(out);
122 : 0 : out << "]" << endl;
123 : 0 : }
124 : :
125 : 0 : PrimitiveVec& CutInfo::getCutVector() { return d_cutVec; }
126 : :
127 : 0 : const PrimitiveVec& CutInfo::getCutVector() const { return d_cutVec; }
128 : :
129 : : // void CutInfo::init_cut(int l){
130 : : // cut_vec.setup(l);
131 : : // }
132 : :
133 : 0 : Kind CutInfo::getKind() const { return d_cutType; }
134 : :
135 : 0 : void CutInfo::setKind(Kind k)
136 : : {
137 : 0 : Assert(k == Kind::LEQ || k == Kind::GEQ);
138 : 0 : d_cutType = k;
139 : 0 : }
140 : :
141 : 0 : double CutInfo::getRhs() const { return d_cutRhs; }
142 : :
143 : 0 : void CutInfo::setRhs(double r) { d_cutRhs = r; }
144 : :
145 : 0 : bool CutInfo::reconstructed() const { return d_exactPrecision != nullptr; }
146 : :
147 : 0 : CutInfoKlass CutInfo::getKlass() const { return d_klass; }
148 : :
149 : 0 : int CutInfo::poolOrdinal() const { return d_poolOrd; }
150 : :
151 : 0 : void CutInfo::setDimensions(int N, int M)
152 : : {
153 : 0 : d_mAtCreation = M;
154 : 0 : d_N = N;
155 : 0 : }
156 : :
157 : 0 : int CutInfo::getN() const { return d_N; }
158 : :
159 : 0 : int CutInfo::getMAtCreation() const { return d_mAtCreation; }
160 : :
161 : : /* Returns true if the cut has an explanation. */
162 : 0 : bool CutInfo::proven() const { return d_explanation != nullptr; }
163 : :
164 : 0 : bool CutInfo::operator<(const CutInfo& o) const
165 : : {
166 : 0 : return d_execOrd < o.d_execOrd;
167 : : }
168 : :
169 : 0 : void CutInfo::setReconstruction(const DenseVector& ep)
170 : : {
171 : 0 : Assert(!reconstructed());
172 : 0 : d_exactPrecision.reset(new DenseVector(ep));
173 : 0 : }
174 : :
175 : 0 : void CutInfo::setExplanation(const ConstraintCPVec& ex)
176 : : {
177 : 0 : Assert(reconstructed());
178 [ - - ]: 0 : if (d_explanation == nullptr)
179 : : {
180 : 0 : d_explanation.reset(new ConstraintCPVec(ex));
181 : : }
182 : : else
183 : : {
184 : 0 : *d_explanation = ex;
185 : : }
186 : 0 : }
187 : :
188 : 0 : void CutInfo::swapExplanation(ConstraintCPVec& ex)
189 : : {
190 : 0 : Assert(reconstructed());
191 : 0 : Assert(!proven());
192 [ - - ]: 0 : if (d_explanation == nullptr)
193 : : {
194 : 0 : d_explanation.reset(new ConstraintCPVec());
195 : : }
196 : 0 : d_explanation->swap(ex);
197 : 0 : }
198 : :
199 : 0 : const DenseVector& CutInfo::getReconstruction() const
200 : : {
201 : 0 : Assert(reconstructed());
202 : 0 : return *d_exactPrecision;
203 : : }
204 : :
205 : 0 : void CutInfo::clearReconstruction()
206 : : {
207 [ - - ]: 0 : if (proven())
208 : : {
209 : 0 : d_explanation = nullptr;
210 : : }
211 : :
212 [ - - ]: 0 : if (reconstructed())
213 : : {
214 : 0 : d_exactPrecision = nullptr;
215 : : }
216 : :
217 : 0 : Assert(!reconstructed());
218 : 0 : Assert(!proven());
219 : 0 : }
220 : :
221 : 0 : const ConstraintCPVec& CutInfo::getExplanation() const
222 : : {
223 : 0 : Assert(proven());
224 : 0 : return *d_explanation;
225 : : }
226 : :
227 : 0 : std::ostream& operator<<(std::ostream& os, const CutInfo& ci)
228 : : {
229 : 0 : ci.print(os);
230 : 0 : return os;
231 : : }
232 : :
233 : 0 : std::ostream& operator<<(std::ostream& out, CutInfoKlass kl)
234 : : {
235 [ - - ][ - - ]: 0 : switch (kl)
[ - - ]
236 : : {
237 : 0 : case MirCutKlass: out << "MirCutKlass"; break;
238 : 0 : case GmiCutKlass: out << "GmiCutKlass"; break;
239 : 0 : case BranchCutKlass: out << "BranchCutKlass"; break;
240 : 0 : case RowsDeletedKlass: out << "RowDeletedKlass"; break;
241 : 0 : case UnknownKlass: out << "UnknownKlass"; break;
242 : 0 : default: out << "unexpected CutInfoKlass"; break;
243 : : }
244 : 0 : return out;
245 : : }
246 : 0 : bool NodeLog::isBranch() const { return d_brVar >= 0; }
247 : :
248 : 0 : NodeLog::NodeLog()
249 : 0 : : d_nid(-1),
250 : 0 : d_parent(nullptr),
251 : 0 : d_tl(nullptr),
252 : 0 : d_cuts(),
253 : 0 : d_rowIdsSelected(),
254 : 0 : d_stat(Open),
255 : 0 : d_brVar(-1),
256 : 0 : d_brVal(0.0),
257 : 0 : d_downId(-1),
258 : 0 : d_upId(-1),
259 : 0 : d_rowId2ArithVar()
260 : : {
261 : 0 : }
262 : :
263 : 12 : NodeLog::NodeLog(TreeLog* tl, int node, const RowIdMap& m)
264 : 12 : : d_nid(node),
265 : 12 : d_parent(nullptr),
266 : 12 : d_tl(tl),
267 : 12 : d_cuts(),
268 : 12 : d_rowIdsSelected(),
269 : 12 : d_stat(Open),
270 : 12 : d_brVar(-1),
271 : 12 : d_brVal(0.0),
272 : 12 : d_downId(-1),
273 : 12 : d_upId(-1),
274 : 12 : d_rowId2ArithVar(m)
275 : : {
276 : 12 : }
277 : :
278 : 0 : NodeLog::NodeLog(TreeLog* tl, NodeLog* parent, int node)
279 : 0 : : d_nid(node),
280 : 0 : d_parent(parent),
281 : 0 : d_tl(tl),
282 : 0 : d_cuts(),
283 : 0 : d_rowIdsSelected(),
284 : 0 : d_stat(Open),
285 : 0 : d_brVar(-1),
286 : 0 : d_brVal(0.0),
287 : 0 : d_downId(-1),
288 : 0 : d_upId(-1),
289 : 0 : d_rowId2ArithVar()
290 : : {
291 : 0 : }
292 : :
293 : 36 : NodeLog::~NodeLog()
294 : : {
295 : 36 : CutSet::iterator i = d_cuts.begin(), iend = d_cuts.end();
296 [ - + ]: 36 : for (; i != iend; ++i)
297 : : {
298 : 0 : CutInfo* c = *i;
299 [ - - ]: 0 : delete c;
300 : : }
301 : 36 : d_cuts.clear();
302 [ - + ][ - + ]: 36 : Assert(d_cuts.empty());
303 : 36 : }
304 : :
305 : 0 : std::ostream& operator<<(std::ostream& os, const NodeLog& nl)
306 : : {
307 : 0 : nl.print(os);
308 : 0 : return os;
309 : : }
310 : :
311 : 0 : void NodeLog::copyParentRowIds()
312 : : {
313 : 0 : Assert(d_parent != nullptr);
314 : 0 : d_rowId2ArithVar = d_parent->d_rowId2ArithVar;
315 : 0 : }
316 : :
317 : 0 : int NodeLog::branchVariable() const { return d_brVar; }
318 : 0 : double NodeLog::branchValue() const { return d_brVal; }
319 : 0 : int NodeLog::getNodeId() const { return d_nid; }
320 : 0 : int NodeLog::getDownId() const { return d_downId; }
321 : 0 : int NodeLog::getUpId() const { return d_upId; }
322 : 0 : void NodeLog::addSelected(int ord, int sel)
323 : : {
324 : 0 : Assert(d_rowIdsSelected.find(ord) == d_rowIdsSelected.end());
325 : 0 : d_rowIdsSelected[ord] = sel;
326 [ - - ]: 0 : Trace("approx::nodelog") << "addSelected(" << ord << ", " << sel << ")"
327 : 0 : << endl;
328 : 0 : }
329 : 0 : void NodeLog::applySelected()
330 : : {
331 : 0 : CutSet::iterator iter = d_cuts.begin(), iend = d_cuts.end(), todelete;
332 [ - - ]: 0 : while (iter != iend)
333 : : {
334 : 0 : CutInfo* curr = *iter;
335 : 0 : int poolOrd = curr->poolOrdinal();
336 [ - - ]: 0 : if (curr->getRowId() >= 0)
337 : : {
338 : : // selected previously, kip
339 : 0 : ++iter;
340 : : }
341 [ - - ]: 0 : else if (curr->getKlass() == RowsDeletedKlass)
342 : : {
343 : : // skip
344 : 0 : ++iter;
345 : : }
346 [ - - ]: 0 : else if (curr->getKlass() == BranchCutKlass)
347 : : {
348 : : // skip
349 : 0 : ++iter;
350 : : }
351 [ - - ]: 0 : else if (d_rowIdsSelected.find(poolOrd) == d_rowIdsSelected.end())
352 : : {
353 : 0 : todelete = iter;
354 : 0 : ++iter;
355 : 0 : d_cuts.erase(todelete);
356 [ - - ]: 0 : delete curr;
357 : : }
358 : : else
359 : : {
360 [ - - ]: 0 : Trace("approx::nodelog")
361 : 0 : << "applySelected " << curr->getId() << " " << poolOrd << "->"
362 : 0 : << d_rowIdsSelected[poolOrd] << endl;
363 : 0 : curr->setRowId(d_rowIdsSelected[poolOrd]);
364 : 0 : ++iter;
365 : : }
366 : : }
367 : 0 : d_rowIdsSelected.clear();
368 : 0 : }
369 : :
370 : 0 : void NodeLog::applyRowsDeleted(const RowsDeleted& rd)
371 : : {
372 : 0 : std::map<int, CutInfo*> currInOrd; // sorted
373 : :
374 : 0 : const PrimitiveVec& cv = rd.getCutVector();
375 : 0 : std::vector<int> sortedRemoved(cv.inds + 1, cv.inds + cv.len + 1);
376 : 0 : sortedRemoved.push_back(INT_MAX);
377 : 0 : std::sort(sortedRemoved.begin(), sortedRemoved.end());
378 : :
379 [ - - ]: 0 : if (TraceIsOn("approx::nodelog"))
380 : : {
381 [ - - ]: 0 : Trace("approx::nodelog") << "Removing #" << sortedRemoved.size() << "...";
382 [ - - ]: 0 : for (unsigned k = 0; k < sortedRemoved.size(); k++)
383 : : {
384 [ - - ]: 0 : Trace("approx::nodelog") << ", " << sortedRemoved[k];
385 : : }
386 [ - - ]: 0 : Trace("approx::nodelog") << endl;
387 [ - - ]: 0 : Trace("approx::nodelog") << "cv.len" << cv.len << endl;
388 : : }
389 : :
390 : 0 : int min = sortedRemoved.front();
391 : :
392 : 0 : CutSet::iterator iter = d_cuts.begin(), iend = d_cuts.end();
393 [ - - ]: 0 : while (iter != iend)
394 : : {
395 : 0 : CutInfo* curr = *iter;
396 [ - - ]: 0 : if (curr->getId() < rd.getId())
397 : : {
398 [ - - ]: 0 : if (d_rowId2ArithVar.find(curr->getRowId()) != d_rowId2ArithVar.end())
399 : : {
400 [ - - ]: 0 : if (curr->getRowId() >= min)
401 : : {
402 : 0 : currInOrd.insert(make_pair(curr->getRowId(), curr));
403 : : }
404 : : }
405 : : }
406 : 0 : ++iter;
407 : : }
408 : :
409 : 0 : RowIdMap::const_iterator i, end;
410 : 0 : i = d_rowId2ArithVar.begin(), end = d_rowId2ArithVar.end();
411 [ - - ]: 0 : for (; i != end; ++i)
412 : : {
413 : 0 : int key = (*i).first;
414 [ - - ]: 0 : if (key >= min)
415 : : {
416 [ - - ]: 0 : if (currInOrd.find(key) == currInOrd.end())
417 : : {
418 : 0 : CutInfo* null = nullptr;
419 : 0 : currInOrd.insert(make_pair(key, null));
420 : : }
421 : : }
422 : : }
423 : :
424 : 0 : std::map<int, CutInfo*>::iterator j, jend;
425 : :
426 : 0 : int posInSorted = 0;
427 [ - - ]: 0 : for (j = currInOrd.begin(), jend = currInOrd.end(); j != jend; ++j)
428 : : {
429 : 0 : int origOrd = (*j).first;
430 : 0 : ArithVar v = d_rowId2ArithVar[origOrd];
431 : 0 : int headRemovedOrd = sortedRemoved[posInSorted];
432 [ - - ]: 0 : while (headRemovedOrd < origOrd)
433 : : {
434 : 0 : ++posInSorted;
435 : 0 : headRemovedOrd = sortedRemoved[posInSorted];
436 : : }
437 : : // headRemoveOrd >= origOrd
438 : 0 : Assert(headRemovedOrd >= origOrd);
439 : :
440 : 0 : CutInfo* ci = (*j).second;
441 [ - - ]: 0 : if (headRemovedOrd == origOrd)
442 : : {
443 [ - - ]: 0 : if (ci == nullptr)
444 : : {
445 [ - - ]: 0 : Trace("approx::nodelog")
446 : 0 : << "deleting from above because of " << rd << endl;
447 [ - - ]: 0 : Trace("approx::nodelog") << "had " << origOrd << " <-> " << v << endl;
448 : 0 : d_rowId2ArithVar.erase(origOrd);
449 : : }
450 : : else
451 : : {
452 [ - - ]: 0 : Trace("approx::nodelog")
453 : 0 : << "deleting " << ci << " because of " << rd << endl;
454 [ - - ]: 0 : Trace("approx::nodelog") << "had " << origOrd << " <-> " << v << endl;
455 : 0 : d_rowId2ArithVar.erase(origOrd);
456 : 0 : ci->setRowId(-1);
457 : : }
458 : : }
459 : : else
460 : : {
461 : 0 : Assert(headRemovedOrd > origOrd);
462 : : // headRemoveOrd > origOrd
463 : 0 : int newOrd = origOrd - posInSorted;
464 : 0 : Assert(newOrd > 0);
465 [ - - ]: 0 : if (ci == nullptr)
466 : : {
467 [ - - ]: 0 : Trace("approx::nodelog") << "shifting above down due to " << rd << endl;
468 [ - - ]: 0 : Trace("approx::nodelog") << "had " << origOrd << " <-> " << v << endl;
469 [ - - ]: 0 : Trace("approx::nodelog")
470 : 0 : << "now have " << newOrd << " <-> " << v << endl;
471 : 0 : d_rowId2ArithVar.erase(origOrd);
472 : 0 : mapRowId(newOrd, v);
473 : : }
474 : : else
475 : : {
476 [ - - ]: 0 : Trace("approx::nodelog")
477 : 0 : << "shifting " << ci << " down due to " << rd << endl;
478 [ - - ]: 0 : Trace("approx::nodelog") << "had " << origOrd << " <-> " << v << endl;
479 [ - - ]: 0 : Trace("approx::nodelog")
480 : 0 : << "now have " << newOrd << " <-> " << v << endl;
481 : 0 : ci->setRowId(newOrd);
482 : 0 : d_rowId2ArithVar.erase(origOrd);
483 : 0 : mapRowId(newOrd, v);
484 : : }
485 : : }
486 : : }
487 : 0 : }
488 : :
489 : 0 : ArithVar NodeLog::lookupRowId(int rowId) const
490 : : {
491 : 0 : RowIdMap::const_iterator i = d_rowId2ArithVar.find(rowId);
492 [ - - ]: 0 : if (i == d_rowId2ArithVar.end())
493 : : {
494 : 0 : return ARITHVAR_SENTINEL;
495 : : }
496 : : else
497 : : {
498 : 0 : return (*i).second;
499 : : }
500 : : }
501 : :
502 : 0 : void NodeLog::mapRowId(int rowId, ArithVar v)
503 : : {
504 : 0 : Assert(lookupRowId(rowId) == ARITHVAR_SENTINEL);
505 [ - - ]: 0 : Trace("approx::nodelog") << "On " << getNodeId() << " adding row id " << rowId
506 : 0 : << " <-> " << v << endl;
507 : 0 : d_rowId2ArithVar[rowId] = v;
508 : 0 : }
509 : :
510 : 0 : void NodeLog::addCut(CutInfo* ci)
511 : : {
512 : 0 : Assert(ci != nullptr);
513 : 0 : d_cuts.insert(ci);
514 : 0 : }
515 : :
516 : 0 : void NodeLog::print(ostream& o) const
517 : : {
518 : 0 : o << "[n" << getNodeId();
519 [ - - ]: 0 : for (const_iterator iter = begin(), iend = end(); iter != iend; ++iter)
520 : : {
521 : 0 : CutInfo* cut = *iter;
522 : 0 : o << ", " << cut->poolOrdinal();
523 [ - - ]: 0 : if (cut->getRowId() >= 0)
524 : : {
525 : 0 : o << " " << cut->getRowId();
526 : : }
527 : : }
528 : 0 : o << "]" << std::endl;
529 : 0 : }
530 : :
531 : 0 : void NodeLog::closeNode()
532 : : {
533 : 0 : Assert(d_stat == Open);
534 : 0 : d_stat = Closed;
535 : 0 : }
536 : :
537 : 0 : void NodeLog::setBranch(int br, double val, int d, int u)
538 : : {
539 : 0 : Assert(d_stat == Open);
540 : 0 : d_brVar = br;
541 : 0 : d_brVal = val;
542 : 0 : d_downId = d;
543 : 0 : d_upId = u;
544 : 0 : d_stat = Branched;
545 : 0 : }
546 : :
547 : 6 : TreeLog::TreeLog()
548 : 6 : : next_exec_ord(0), d_toNode(), d_branches(), d_numCuts(0), d_active(false)
549 : : {
550 : 6 : NodeLog::RowIdMap empty;
551 : 6 : reset(empty);
552 : 6 : }
553 : :
554 : 24 : int TreeLog::getRootId() const { return 1; }
555 : :
556 : 0 : NodeLog& TreeLog::getRootNode() { return getNode(getRootId()); }
557 : :
558 : 12 : void TreeLog::clear()
559 : : {
560 : 12 : next_exec_ord = 0;
561 : 12 : d_toNode.clear();
562 : 12 : d_branches.purge();
563 : :
564 : 12 : d_numCuts = 0;
565 : :
566 : : // add root
567 : 12 : }
568 : :
569 : 12 : void TreeLog::reset(const NodeLog::RowIdMap& m)
570 : : {
571 : 12 : clear();
572 : 12 : d_toNode.insert(make_pair(getRootId(), NodeLog(this, getRootId(), m)));
573 : 12 : }
574 : :
575 : 6 : void TreeLog::addCut() { d_numCuts++; }
576 : 0 : uint32_t TreeLog::cutCount() const { return d_numCuts; }
577 : 0 : void TreeLog::logBranch(uint32_t x) { d_branches.add(x); }
578 : 0 : uint32_t TreeLog::numBranches(uint32_t x) { return d_branches.count(x); }
579 : :
580 : 0 : void TreeLog::branch(int nid, int br, double val, int dn, int up)
581 : : {
582 : 0 : NodeLog& nl = getNode(nid);
583 : 0 : nl.setBranch(br, val, dn, up);
584 : :
585 : 0 : d_toNode.insert(make_pair(dn, NodeLog(this, &nl, dn)));
586 : 0 : d_toNode.insert(make_pair(up, NodeLog(this, &nl, up)));
587 : 0 : }
588 : :
589 : 0 : void TreeLog::close(int nid)
590 : : {
591 : 0 : NodeLog& nl = getNode(nid);
592 : 0 : nl.closeNode();
593 : 0 : }
594 : :
595 : : // void TreeLog::applySelected() {
596 : : // std::map<int, NodeLog>::iterator iter, end;
597 : : // for(iter = d_toNode.begin(), end = d_toNode.end(); iter != end; ++iter){
598 : : // NodeLog& onNode = (*iter).second;
599 : : // //onNode.applySelected();
600 : : // }
601 : : // }
602 : :
603 : 0 : void TreeLog::print(ostream& o) const
604 : : {
605 : 0 : o << "TreeLog: " << d_toNode.size() << std::endl;
606 [ - - ]: 0 : for (const_iterator iter = begin(), iend = end(); iter != iend; ++iter)
607 : : {
608 : 0 : const NodeLog& onNode = (*iter).second;
609 : 0 : onNode.print(o);
610 : : }
611 : 0 : }
612 : :
613 : 0 : void TreeLog::applyRowsDeleted(int nid, const RowsDeleted& rd)
614 : : {
615 : 0 : NodeLog& nl = getNode(nid);
616 : 0 : nl.applyRowsDeleted(rd);
617 : 0 : }
618 : :
619 : 0 : void TreeLog::mapRowId(int nid, int ind, ArithVar v)
620 : : {
621 : 0 : NodeLog& nl = getNode(nid);
622 : 0 : nl.mapRowId(ind, v);
623 : 0 : }
624 : :
625 : 30 : void DenseVector::purge()
626 : : {
627 : 30 : lhs.purge();
628 : 30 : rhs = Rational(0);
629 : 30 : }
630 : :
631 : 0 : RowsDeleted::RowsDeleted(int execOrd, int nrows, const int num[])
632 : 0 : : CutInfo(RowsDeletedKlass, execOrd, 0)
633 : : {
634 : 0 : d_cutVec.setup(nrows);
635 [ - - ]: 0 : for (int j = 1; j <= nrows; j++)
636 : : {
637 : 0 : d_cutVec.coeffs[j] = 0;
638 : 0 : d_cutVec.inds[j] = num[j];
639 : : }
640 : 0 : }
641 : :
642 : 0 : BranchCutInfo::BranchCutInfo(int execOrd, int br, Kind dir, double val)
643 : 0 : : CutInfo(BranchCutKlass, execOrd, 0)
644 : : {
645 : 0 : d_cutVec.setup(1);
646 : 0 : d_cutVec.inds[1] = br;
647 : 0 : d_cutVec.coeffs[1] = +1.0;
648 : 0 : d_cutRhs = val;
649 : 0 : d_cutType = dir;
650 : 0 : }
651 : :
652 : 0 : void TreeLog::printBranchInfo(ostream& os) const
653 : : {
654 : 0 : uint32_t total = 0;
655 : 0 : DenseMultiset::const_iterator iter = d_branches.begin(),
656 : 0 : iend = d_branches.end();
657 [ - - ]: 0 : for (; iter != iend; ++iter)
658 : : {
659 : 0 : uint32_t el = *iter;
660 : 0 : total += el;
661 : : }
662 : 0 : os << "printBranchInfo() : " << total << endl;
663 : 0 : iter = d_branches.begin(), iend = d_branches.end();
664 [ - - ]: 0 : for (; iter != iend; ++iter)
665 : : {
666 : 0 : uint32_t el = *iter;
667 : 0 : os << "[" << el << ", " << d_branches.count(el) << "]";
668 : : }
669 : 0 : os << endl;
670 : 0 : }
671 : :
672 : 0 : void DenseVector::print(std::ostream& os) const
673 : : {
674 : 0 : os << rhs << " + ";
675 : 0 : print(os, lhs);
676 : 0 : }
677 : 0 : void DenseVector::print(ostream& out, const DenseMap<Rational>& v)
678 : : {
679 : 0 : out << "[DenseVec len " << v.size();
680 : 0 : DenseMap<Rational>::const_iterator iter, end;
681 [ - - ]: 0 : for (iter = v.begin(), end = v.end(); iter != end; ++iter)
682 : : {
683 : 0 : ArithVar x = *iter;
684 : 0 : out << ", " << x << " " << v[x];
685 : : }
686 : 0 : out << "]";
687 : 0 : }
688 : :
689 : : } // namespace arith::linear
690 : : } // namespace theory
691 : : } // namespace cvc5::internal
|
