src/theory/arith/cut_log.cpp

   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-2020 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 }/* CVC4 namespace */