Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/tableau.h	Lines:	18	33	54.5 %
Date:	2021-08-14	Branches:	3	36	8.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "cvc5_private.h"

#pragma once

#include <vector>

#include "theory/arith/arithvar.h"
#include "theory/arith/matrix.h"
#include "util/dense_map.h"
#include "util/rational.h"

namespace cvc5 {
namespace theory {
namespace arith {

/**
 * A Tableau is a Rational matrix that keeps its rows in solved form.
 * Each row has a basic variable with coefficient -1 that is solved.
 * Tableau is optimized for pivoting.
 * The tableau should only be updated via pivot calls.
 */
class Tableau : public Matrix<Rational> {
public:
private:
  typedef DenseMap<RowIndex> BasicToRowMap;
  // Set of all of the basic variables in the tableau.
  // ArithVarMap<RowIndex> : ArithVar |-> RowIndex
  BasicToRowMap d_basic2RowIndex;

  // RowIndex |-> Basic Variable
  typedef DenseMap<ArithVar> RowIndexToBasicMap;
  RowIndexToBasicMap d_rowIndex2basic;

public:

  Tableau() : Matrix<Rational>(Rational(0)) {}

  typedef Matrix<Rational>::ColIterator ColIterator;
  typedef Matrix<Rational>::RowIterator RowIterator;
  typedef BasicToRowMap::const_iterator BasicIterator;

  typedef MatrixEntry<Rational> Entry;

  bool isBasic(ArithVar v) const{
    return d_basic2RowIndex.isKey(v);
  }

  void debugPrintIsBasic(ArithVar v) const {
    if(isBasic(v)){
      Warning() << v << " is basic." << std::endl;
    }else{
      Warning() << v << " is non-basic." << std::endl;
    }
  }

  BasicIterator beginBasic() const {
    return d_basic2RowIndex.begin();
  }
  BasicIterator endBasic() const {
    return d_basic2RowIndex.end();
  }

  RowIndex basicToRowIndex(ArithVar x) const {
    return d_basic2RowIndex[x];
  }

  ArithVar rowIndexToBasic(RowIndex rid) const {
    Assert(d_rowIndex2basic.isKey(rid));
    return d_rowIndex2basic[rid];
  }

  ColIterator colIterator(ArithVar x) const {
    return getColumn(x).begin();
  }

  RowIterator ridRowIterator(RowIndex rid) const {
    return getRow(rid).begin();
  }

  RowIterator basicRowIterator(ArithVar basic) const {
    return ridRowIterator(basicToRowIndex(basic));
  }

  const Entry& basicFindEntry(ArithVar basic, ArithVar col) const {
    return findEntry(basicToRowIndex(basic), col);
  }

  /**
   * Adds a row to the tableau.
   * The new row is equivalent to:
   *   basicVar = \f$\sum_i\f$ coeffs[i] * variables[i]
   * preconditions:
   *   basicVar is already declared to be basic
   *   basicVar does not have a row associated with it in the tableau.
   *
   * Note: each variables[i] does not have to be non-basic.
   * Pivoting will be mimicked if it is basic.
   */
  void addRow(ArithVar basicVar,
              const std::vector<Rational>& coeffs,
              const std::vector<ArithVar>& variables);

  /**
   * preconditions:
   *   x_r is basic,
   *   x_s is non-basic, and
   *   a_rs != 0.
   */
  void pivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb);

  void removeBasicRow(ArithVar basic);

  uint32_t basicRowLength(ArithVar basic) const{
    RowIndex ridx = basicToRowIndex(basic);
    return getRowLength(ridx);
  }

  /**
   *  to += mult * from
   * replacing from with its row.
   */
  void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult,  CoefficientChangeCallback& cb);

  void directlyAddToCoefficient(ArithVar rowVar, ArithVar col, const Rational& mult,  CoefficientChangeCallback& cb){
    RowIndex ridx = basicToRowIndex(rowVar);
    manipulateRowEntry(ridx, col, mult, cb);
  }

  /* Returns the complexity of a row in the tableau. */
  uint32_t rowComplexity(ArithVar basic) const;

  /* Returns the average complexity of the rows in the tableau. */
  double avgRowComplexity() const;

  void printBasicRow(ArithVar basic, std::ostream& out);

private:
  /* Changes the basic variable on the row for basicOld to basicNew. */
  void rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb);

};/* class Tableau */

}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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