Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/tableau.cpp	Lines:	76	109	69.7 %
Date:	2021-08-13	Branches:	117	492	23.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King
 *
 * 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 "base/output.h"
#include "theory/arith/tableau.h"

using namespace std;
namespace cvc5 {
namespace theory {
namespace arith {


void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic, CoefficientChangeCallback& cb){
  Assert(isBasic(oldBasic));
  Assert(!isBasic(newBasic));
  Assert(d_mergeBuffer.empty());

  Debug("tableau") << "Tableau::pivot(" <<  oldBasic <<", " << newBasic <<")"  << endl;

  RowIndex ridx = basicToRowIndex(oldBasic);

  rowPivot(oldBasic, newBasic, cb);
  Assert(ridx == basicToRowIndex(newBasic));

  loadRowIntoBuffer(ridx);

  ColIterator colIter = colIterator(newBasic);
  while(!colIter.atEnd()){
    EntryID id = colIter.getID();
    Entry& entry = d_entries.get(id);

    ++colIter; //needs to be incremented before the variable is removed
    if(entry.getRowIndex() == ridx){ continue; }

    RowIndex to = entry.getRowIndex();
    Rational coeff = entry.getCoefficient();
    if(cb.canUseRow(to)){
      rowPlusBufferTimesConstant(to, coeff, cb);
    }else{
      rowPlusBufferTimesConstant(to, coeff);
    }
  }
  clearBuffer();

  //Clear the column for used for this variable

  Assert(d_mergeBuffer.empty());
  Assert(!isBasic(oldBasic));
  Assert(isBasic(newBasic));
  Assert(getColLength(newBasic) == 1);
}

/**
 * Changes basic to newbasic (a variable on the row).
 */
void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb){
  Assert(isBasic(basicOld));
  Assert(!isBasic(basicNew));

  RowIndex rid = basicToRowIndex(basicOld);

  EntryID newBasicID = findOnRow(rid, basicNew);

  Assert(newBasicID != ENTRYID_SENTINEL);

  Tableau::Entry& newBasicEntry = d_entries.get(newBasicID);
  const Rational& a_rs = newBasicEntry.getCoefficient();
  int a_rs_sgn = a_rs.sgn();
  Rational negInverseA_rs = -(a_rs.inverse());

  for(RowIterator i = basicRowIterator(basicOld); !i.atEnd(); ++i){
    EntryID id = i.getID();
    Tableau::Entry& entry = d_entries.get(id);

    entry.getCoefficient() *=  negInverseA_rs;
  }

  d_basic2RowIndex.remove(basicOld);
  d_basic2RowIndex.set(basicNew, rid);
  d_rowIndex2basic.set(rid, basicNew);

  cb.multiplyRow(rid, -a_rs_sgn);
}

void Tableau::addRow(ArithVar basic,
                     const std::vector<Rational>& coefficients,
                     const std::vector<ArithVar>& variables)
{
  Assert(basic < getNumColumns());
  Assert(debugIsASet(variables));
  Assert(coefficients.size() == variables.size());
  Assert(!isBasic(basic));

  RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
  addEntry(newRow, basic, Rational(-1));

  Assert(!d_basic2RowIndex.isKey(basic));
  Assert(!d_rowIndex2basic.isKey(newRow));

  d_basic2RowIndex.set(basic, newRow);
  d_rowIndex2basic.set(newRow, basic);


  if(Debug.isOn("matrix")){ printMatrix(); }

  NoEffectCCCB noeffect;
  NoEffectCCCB* nep = &noeffect;
  CoefficientChangeCallback* cccb = static_cast<CoefficientChangeCallback*>(nep);

  vector<Rational>::const_iterator coeffIter = coefficients.begin();
  vector<ArithVar>::const_iterator varsIter = variables.begin();
  vector<ArithVar>::const_iterator varsEnd = variables.end();
  for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
    ArithVar var = *varsIter;

    if(isBasic(var)){
      Rational coeff = *coeffIter;

      RowIndex ri = basicToRowIndex(var);

      loadRowIntoBuffer(ri);
      rowPlusBufferTimesConstant(newRow, coeff, *cccb);
      clearBuffer();
    }
  }

  if(Debug.isOn("matrix")) { printMatrix(); }

  Assert(debugNoZeroCoefficients(newRow));
  Assert(debugMatchingCountsForRow(newRow));
  Assert(getColLength(basic) == 1);
}

void Tableau::removeBasicRow(ArithVar basic){
  RowIndex rid = basicToRowIndex(basic);

  removeRow(rid);
  d_basic2RowIndex.remove(basic);
  d_rowIndex2basic.remove(rid);
}

void Tableau::substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult,  CoefficientChangeCallback& cb){
  if(!mult.isZero()){
    RowIndex to_idx = basicToRowIndex(to);
    addEntry(to_idx, from, mult); // Add an entry to be cancelled out
    RowIndex from_idx = basicToRowIndex(from);

    cb.update(to_idx, from, 0, mult.sgn());

    loadRowIntoBuffer(from_idx);
    rowPlusBufferTimesConstant(to_idx, mult, cb);
    clearBuffer();
  }
}

uint32_t Tableau::rowComplexity(ArithVar basic) const{
  uint32_t complexity = 0;
  for(RowIterator i = basicRowIterator(basic); !i.atEnd(); ++i){
    const Entry& e = *i;
    complexity += e.getCoefficient().complexity();
  }
  return complexity;
}

double Tableau::avgRowComplexity() const{
  double sum = 0;
  uint32_t rows = 0;
  for(BasicIterator i = beginBasic(), i_end = endBasic(); i != i_end; ++i){
    sum += rowComplexity(*i);
    rows++;
  }
  return (rows == 0) ? 0 : (sum/rows);
}

void Tableau::printBasicRow(ArithVar basic, std::ostream& out){
  printRow(basicToRowIndex(basic), out);
}

}  // 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
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 "base/output.h"
20		#include "theory/arith/tableau.h"
21
22		using namespace std;
23		namespace cvc5 {
24		namespace theory {
25		namespace arith {
26
27
28	198105	void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic, CoefficientChangeCallback& cb){
29	198105	Assert(isBasic(oldBasic));
30	198105	Assert(!isBasic(newBasic));
31	198105	Assert(d_mergeBuffer.empty());
32
33	198105	Debug("tableau") << "Tableau::pivot(" << oldBasic <<", " << newBasic <<")" << endl;
34
35	198105	RowIndex ridx = basicToRowIndex(oldBasic);
36
37	198105	rowPivot(oldBasic, newBasic, cb);
38	198105	Assert(ridx == basicToRowIndex(newBasic));
39
40	198105	loadRowIntoBuffer(ridx);
41
42	198105	ColIterator colIter = colIterator(newBasic);
43	7616561	while(!colIter.atEnd()){
44	3709228	EntryID id = colIter.getID();
45	3709228	Entry& entry = d_entries.get(id);
46
47	3709228	++colIter; //needs to be incremented before the variable is removed
48	3709228	if(entry.getRowIndex() == ridx){ continue; }
49
50	3511123	RowIndex to = entry.getRowIndex();
51	7022246	Rational coeff = entry.getCoefficient();
52	3511123	if(cb.canUseRow(to)){
53	3511123	rowPlusBufferTimesConstant(to, coeff, cb);
54		}else{
55		rowPlusBufferTimesConstant(to, coeff);
56		}
57		}
58	198105	clearBuffer();
59
60		//Clear the column for used for this variable
61
62	198105	Assert(d_mergeBuffer.empty());
63	198105	Assert(!isBasic(oldBasic));
64	198105	Assert(isBasic(newBasic));
65	198105	Assert(getColLength(newBasic) == 1);
66	198105	}
67
68		/**
69		* Changes basic to newbasic (a variable on the row).
70		*/
71	198105	void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb){
72	198105	Assert(isBasic(basicOld));
73	198105	Assert(!isBasic(basicNew));
74
75	198105	RowIndex rid = basicToRowIndex(basicOld);
76
77	198105	EntryID newBasicID = findOnRow(rid, basicNew);
78
79	198105	Assert(newBasicID != ENTRYID_SENTINEL);
80
81	198105	Tableau::Entry& newBasicEntry = d_entries.get(newBasicID);
82	198105	const Rational& a_rs = newBasicEntry.getCoefficient();
83	198105	int a_rs_sgn = a_rs.sgn();
84	396210	Rational negInverseA_rs = -(a_rs.inverse());
85
86	5061424	for(RowIterator i = basicRowIterator(basicOld); !i.atEnd(); ++i){
87	4863319	EntryID id = i.getID();
88	4863319	Tableau::Entry& entry = d_entries.get(id);
89
90	4863319	entry.getCoefficient() *= negInverseA_rs;
91		}
92
93	198105	d_basic2RowIndex.remove(basicOld);
94	198105	d_basic2RowIndex.set(basicNew, rid);
95	198105	d_rowIndex2basic.set(rid, basicNew);
96
97	198105	cb.multiplyRow(rid, -a_rs_sgn);
98	198105	}
99
100	92722	void Tableau::addRow(ArithVar basic,
101		const std::vector<Rational>& coefficients,
102		const std::vector<ArithVar>& variables)
103		{
104	92722	Assert(basic < getNumColumns());
105	92722	Assert(debugIsASet(variables));
106	92722	Assert(coefficients.size() == variables.size());
107	92722	Assert(!isBasic(basic));
108
109	92722	RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
110	92722	addEntry(newRow, basic, Rational(-1));
111
112	92722	Assert(!d_basic2RowIndex.isKey(basic));
113	92722	Assert(!d_rowIndex2basic.isKey(newRow));
114
115	92722	d_basic2RowIndex.set(basic, newRow);
116	92722	d_rowIndex2basic.set(newRow, basic);
117
118
119	92722	if(Debug.isOn("matrix")){ printMatrix(); }
120
121	185444	NoEffectCCCB noeffect;
122	92722	NoEffectCCCB* nep = &noeffect;
123	92722	CoefficientChangeCallback* cccb = static_cast<CoefficientChangeCallback*>(nep);
124
125	92722	vector<Rational>::const_iterator coeffIter = coefficients.begin();
126	92722	vector<ArithVar>::const_iterator varsIter = variables.begin();
127	92722	vector<ArithVar>::const_iterator varsEnd = variables.end();
128	520646	for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
129	213962	ArithVar var = *varsIter;
130
131	213962	if(isBasic(var)){
132	104154	Rational coeff = *coeffIter;
133
134	52077	RowIndex ri = basicToRowIndex(var);
135
136	52077	loadRowIntoBuffer(ri);
137	52077	rowPlusBufferTimesConstant(newRow, coeff, *cccb);
138	52077	clearBuffer();
139		}
140		}
141
142	92722	if(Debug.isOn("matrix")) { printMatrix(); }
143
144	92722	Assert(debugNoZeroCoefficients(newRow));
145	92722	Assert(debugMatchingCountsForRow(newRow));
146	92722	Assert(getColLength(basic) == 1);
147	92722	}
148
149		void Tableau::removeBasicRow(ArithVar basic){
150		RowIndex rid = basicToRowIndex(basic);
151
152		removeRow(rid);
153		d_basic2RowIndex.remove(basic);
154		d_rowIndex2basic.remove(rid);
155		}
156
157		void Tableau::substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult, CoefficientChangeCallback& cb){
158		if(!mult.isZero()){
159		RowIndex to_idx = basicToRowIndex(to);
160		addEntry(to_idx, from, mult); // Add an entry to be cancelled out
161		RowIndex from_idx = basicToRowIndex(from);
162
163		cb.update(to_idx, from, 0, mult.sgn());
164
165		loadRowIntoBuffer(from_idx);
166		rowPlusBufferTimesConstant(to_idx, mult, cb);
167		clearBuffer();
168		}
169		}
170
171		uint32_t Tableau::rowComplexity(ArithVar basic) const{
172		uint32_t complexity = 0;
173		for(RowIterator i = basicRowIterator(basic); !i.atEnd(); ++i){
174		const Entry& e = *i;
175		complexity += e.getCoefficient().complexity();
176		}
177		return complexity;
178		}
179
180		double Tableau::avgRowComplexity() const{
181		double sum = 0;
182		uint32_t rows = 0;
183		for(BasicIterator i = beginBasic(), i_end = endBasic(); i != i_end; ++i){
184		sum += rowComplexity(*i);
185		rows++;
186		}
187		return (rows == 0) ? 0 : (sum/rows);
188		}
189
190		void Tableau::printBasicRow(ArithVar basic, std::ostream& out){
191		printRow(basicToRowIndex(basic), out);
192		}
193
194		} // namespace arith
195		} // namespace theory
196	29340	} // namespace cvc5