GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/cut_log.cpp Lines: 1 405 0.2 %
Date: 2021-03-23 Branches: 2 850 0.2 %

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