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