GCC Code Coverage Report
 Directory: . Exec Total Coverage File: src/theory/arith/tableau.h Lines: 18 33 54.5 % Date: 2021-03-22 Branches: 3 36 8.3 %

 Line Exec Source 1 /********************* */ 2 /*! \file tableau.h 3  ** \verbatim 4  ** Top contributors (to current version): 5  ** Tim King, Morgan Deters 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 "cvc4_private.h" 19 20 #pragma once 21 22 #include  23 24 #include "theory/arith/arithvar.h" 25 #include "theory/arith/matrix.h" 26 #include "util/dense_map.h" 27 #include "util/rational.h" 28 29 namespace CVC4 { 30 namespace theory { 31 namespace arith { 32 33 /** 34  * A Tableau is a Rational matrix that keeps its rows in solved form. 35  * Each row has a basic variable with coefficient -1 that is solved. 36  * Tableau is optimized for pivoting. 37  * The tableau should only be updated via pivot calls. 38  */ 39 17984 class Tableau : public Matrix { 40 public: 41 private: 42  typedef DenseMap BasicToRowMap; 43  // Set of all of the basic variables in the tableau. 44  // ArithVarMap : ArithVar |-> RowIndex 45  BasicToRowMap d_basic2RowIndex; 46 47  // RowIndex |-> Basic Variable 48  typedef DenseMap RowIndexToBasicMap; 49  RowIndexToBasicMap d_rowIndex2basic; 50 51 public: 52 53 17990  Tableau() : Matrix(Rational(0)) {} 54 55  typedef Matrix::ColIterator ColIterator; 56  typedef Matrix::RowIterator RowIterator; 57  typedef BasicToRowMap::const_iterator BasicIterator; 58 59  typedef MatrixEntry Entry; 60 61 19283881  bool isBasic(ArithVar v) const{ 62 19283881  return d_basic2RowIndex.isKey(v); 63  } 64 65  void debugPrintIsBasic(ArithVar v) const { 66  if(isBasic(v)){ 67  Warning() << v << " is basic." << std::endl; 68  }else{ 69  Warning() << v << " is non-basic." << std::endl; 70  } 71  } 72 73  BasicIterator beginBasic() const { 74  return d_basic2RowIndex.begin(); 75  } 76  BasicIterator endBasic() const { 77  return d_basic2RowIndex.end(); 78  } 79 80 10643334  RowIndex basicToRowIndex(ArithVar x) const { 81 10643334  return d_basic2RowIndex[x]; 82  } 83 84 29914363  ArithVar rowIndexToBasic(RowIndex rid) const { 85 29914363  Assert(d_rowIndex2basic.isKey(rid)); 86 29914363  return d_rowIndex2basic[rid]; 87  } 88 89 6145632  ColIterator colIterator(ArithVar x) const { 90 6145632  return getColumn(x).begin(); 91  } 92 93 6557240  RowIterator ridRowIterator(RowIndex rid) const { 94 6557240  return getRow(rid).begin(); 95  } 96 97 621496  RowIterator basicRowIterator(ArithVar basic) const { 98 621496  return ridRowIterator(basicToRowIndex(basic)); 99  } 100 101  const Entry& basicFindEntry(ArithVar basic, ArithVar col) const { 102  return findEntry(basicToRowIndex(basic), col); 103  } 104 105  /** 106  * Adds a row to the tableau. 107  * The new row is equivalent to: 108  * basicVar = \f$\sum_i\f$ coeffs[i] * variables[i] 109  * preconditions: 110  * basicVar is already declared to be basic 111  * basicVar does not have a row associated with it in the tableau. 112  * 113  * Note: each variables[i] does not have to be non-basic. 114  * Pivoting will be mimicked if it is basic. 115  */ 116  void addRow(ArithVar basicVar, 117  const std::vector& coeffs, 118  const std::vector& variables); 119 120  /** 121  * preconditions: 122  * x_r is basic, 123  * x_s is non-basic, and 124  * a_rs != 0. 125  */ 126  void pivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb); 127 128  void removeBasicRow(ArithVar basic); 129 130 896141  uint32_t basicRowLength(ArithVar basic) const{ 131 896141  RowIndex ridx = basicToRowIndex(basic); 132 896141  return getRowLength(ridx); 133  } 134 135  /** 136  * to += mult * from 137  * replacing from with its row. 138  */ 139  void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult, CoefficientChangeCallback& cb); 140 141  void directlyAddToCoefficient(ArithVar rowVar, ArithVar col, const Rational& mult, CoefficientChangeCallback& cb){ 142  RowIndex ridx = basicToRowIndex(rowVar); 143  manipulateRowEntry(ridx, col, mult, cb); 144  } 145 146  /* Returns the complexity of a row in the tableau. */ 147  uint32_t rowComplexity(ArithVar basic) const; 148 149  /* Returns the average complexity of the rows in the tableau. */ 150  double avgRowComplexity() const; 151 152  void printBasicRow(ArithVar basic, std::ostream& out); 153 154 private: 155  /* Changes the basic variable on the row for basicOld to basicNew. */ 156  void rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb); 157 158 };/* class Tableau */ 159 160 161 162 }/* CVC4::theory::arith namespace */ 163 }/* CVC4::theory namespace */ 164 }/* CVC4 namespace */

 Generated by: GCOVR (Version 3.2)