Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/tableau.cpp	Lines:	76	109	69.7 %
Date:	2021-08-17	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	197101	void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic, CoefficientChangeCallback& cb){
29	197101	Assert(isBasic(oldBasic));
30	197101	Assert(!isBasic(newBasic));
31	197101	Assert(d_mergeBuffer.empty());
32
33	197101	Debug("tableau") << "Tableau::pivot(" << oldBasic <<", " << newBasic <<")" << endl;
34
35	197101	RowIndex ridx = basicToRowIndex(oldBasic);
36
37	197101	rowPivot(oldBasic, newBasic, cb);
38	197101	Assert(ridx == basicToRowIndex(newBasic));
39
40	197101	loadRowIntoBuffer(ridx);
41
42	197101	ColIterator colIter = colIterator(newBasic);
43	7599829	while(!colIter.atEnd()){
44	3701364	EntryID id = colIter.getID();
45	3701364	Entry& entry = d_entries.get(id);
46
47	3701364	++colIter; //needs to be incremented before the variable is removed
48	3701364	if(entry.getRowIndex() == ridx){ continue; }
49
50	3504263	RowIndex to = entry.getRowIndex();
51	7008526	Rational coeff = entry.getCoefficient();
52	3504263	if(cb.canUseRow(to)){
53	3504263	rowPlusBufferTimesConstant(to, coeff, cb);
54		}else{
55		rowPlusBufferTimesConstant(to, coeff);
56		}
57		}
58	197101	clearBuffer();
59
60		//Clear the column for used for this variable
61
62	197101	Assert(d_mergeBuffer.empty());
63	197101	Assert(!isBasic(oldBasic));
64	197101	Assert(isBasic(newBasic));
65	197101	Assert(getColLength(newBasic) == 1);
66	197101	}
67
68		/**
69		* Changes basic to newbasic (a variable on the row).
70		*/
71	197101	void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb){
72	197101	Assert(isBasic(basicOld));
73	197101	Assert(!isBasic(basicNew));
74
75	197101	RowIndex rid = basicToRowIndex(basicOld);
76
77	197101	EntryID newBasicID = findOnRow(rid, basicNew);
78
79	197101	Assert(newBasicID != ENTRYID_SENTINEL);
80
81	197101	Tableau::Entry& newBasicEntry = d_entries.get(newBasicID);
82	197101	const Rational& a_rs = newBasicEntry.getCoefficient();
83	197101	int a_rs_sgn = a_rs.sgn();
84	394202	Rational negInverseA_rs = -(a_rs.inverse());
85
86	5057636	for(RowIterator i = basicRowIterator(basicOld); !i.atEnd(); ++i){
87	4860535	EntryID id = i.getID();
88	4860535	Tableau::Entry& entry = d_entries.get(id);
89
90	4860535	entry.getCoefficient() *= negInverseA_rs;
91		}
92
93	197101	d_basic2RowIndex.remove(basicOld);
94	197101	d_basic2RowIndex.set(basicNew, rid);
95	197101	d_rowIndex2basic.set(rid, basicNew);
96
97	197101	cb.multiplyRow(rid, -a_rs_sgn);
98	197101	}
99
100	92695	void Tableau::addRow(ArithVar basic,
101		const std::vector<Rational>& coefficients,
102		const std::vector<ArithVar>& variables)
103		{
104	92695	Assert(basic < getNumColumns());
105	92695	Assert(debugIsASet(variables));
106	92695	Assert(coefficients.size() == variables.size());
107	92695	Assert(!isBasic(basic));
108
109	92695	RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
110	92695	addEntry(newRow, basic, Rational(-1));
111
112	92695	Assert(!d_basic2RowIndex.isKey(basic));
113	92695	Assert(!d_rowIndex2basic.isKey(newRow));
114
115	92695	d_basic2RowIndex.set(basic, newRow);
116	92695	d_rowIndex2basic.set(newRow, basic);
117
118
119	92695	if(Debug.isOn("matrix")){ printMatrix(); }
120
121	185390	NoEffectCCCB noeffect;
122	92695	NoEffectCCCB* nep = &noeffect;
123	92695	CoefficientChangeCallback* cccb = static_cast<CoefficientChangeCallback*>(nep);
124
125	92695	vector<Rational>::const_iterator coeffIter = coefficients.begin();
126	92695	vector<ArithVar>::const_iterator varsIter = variables.begin();
127	92695	vector<ArithVar>::const_iterator varsEnd = variables.end();
128	520473	for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
129	213889	ArithVar var = *varsIter;
130
131	213889	if(isBasic(var)){
132	104126	Rational coeff = *coeffIter;
133
134	52063	RowIndex ri = basicToRowIndex(var);
135
136	52063	loadRowIntoBuffer(ri);
137	52063	rowPlusBufferTimesConstant(newRow, coeff, *cccb);
138	52063	clearBuffer();
139		}
140		}
141
142	92695	if(Debug.isOn("matrix")) { printMatrix(); }
143
144	92695	Assert(debugNoZeroCoefficients(newRow));
145	92695	Assert(debugMatchingCountsForRow(newRow));
146	92695	Assert(getColLength(basic) == 1);
147	92695	}
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	29337	} // namespace cvc5