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