Changes:
[cvc5.git] / src / theory / arith / tableau.cpp
1 /********************* */
2 /*! \file tableau.cpp
3 ** \verbatim
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
13 **
14 ** \brief [[ Add one-line brief description here ]]
15 **
16 ** [[ Add lengthier description here ]]
17 ** \todo document this file
18 **/
19
20
21 #include "theory/arith/tableau.h"
22
23 using namespace CVC4;
24 using namespace CVC4::theory;
25 using namespace CVC4::theory::arith;
26
27 Tableau::~Tableau(){
28 while(!d_activeBasicVars.empty()){
29 ArithVar curr = *(d_activeBasicVars.begin());
30 ReducedRowVector* vec = removeRow(curr);
31 delete vec;
32 }
33 }
34
35 void Tableau::addRow(ArithVar basicVar,
36 const std::vector<Rational>& coeffs,
37 const std::vector<ArithVar>& variables){
38
39 Assert(coeffs.size() == variables.size());
40 Assert(d_basicManager.isMember(basicVar));
41
42 //The new basic variable cannot already be a basic variable
43 Assert(!d_activeBasicVars.isMember(basicVar));
44 d_activeBasicVars.add(basicVar);
45 ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount);
46 d_rowsTable[basicVar] = row_current;
47
48 //A variable in the row may have been made non-basic already.
49 //If this is the case we fake pivoting this variable
50 vector<ArithVar>::const_iterator varsIter = variables.begin();
51 vector<ArithVar>::const_iterator varsEnd = variables.end();
52
53 for( ; varsIter != varsEnd; ++varsIter){
54 ArithVar var = *varsIter;
55
56 if(d_basicManager.isMember(var)){
57 Assert(d_activeBasicVars.isMember(var));
58
59 ReducedRowVector& row_var = lookup(var);
60 row_current->substitute(row_var);
61 }
62 }
63 }
64
65 ReducedRowVector* Tableau::removeRow(ArithVar basic){
66 Assert(d_basicManager.isMember(basic));
67 Assert(d_activeBasicVars.isMember(basic));
68
69 ReducedRowVector* row = d_rowsTable[basic];
70
71 d_activeBasicVars.remove(basic);
72 d_rowsTable[basic] = NULL;
73
74 return row;
75 }
76
77 void Tableau::pivot(ArithVar x_r, ArithVar x_s){
78 Assert(d_basicManager.isMember(x_r));
79 Assert(!d_basicManager.isMember(x_s));
80
81 Debug("tableau") << "Tableau::pivot(" << x_r <<", " <<x_s <<")" << endl;
82
83 ReducedRowVector* row_s = d_rowsTable[x_r];
84 Assert(row_s != NULL);
85 Assert(row_s->has(x_s));
86
87 //Swap x_r and x_s in d_activeRows
88 d_rowsTable[x_s] = row_s;
89 d_rowsTable[x_r] = NULL;
90
91 d_activeBasicVars.remove(x_r);
92 d_basicManager.remove(x_r);
93
94 d_activeBasicVars.add(x_s);
95 d_basicManager.add(x_s);
96
97 row_s->pivot(x_s);
98
99 for(ArithVarSet::iterator basicIter = begin(), endIter = end();
100 basicIter != endIter; ++basicIter){
101 ArithVar basic = *basicIter;
102 if(basic == x_s) continue;
103
104 ReducedRowVector& row_k = lookup(basic);
105 if(row_k.has(x_s)){
106 row_k.substitute(*row_s);
107 }
108 }
109 }
110 void Tableau::printTableau(){
111 Debug("tableau") << "Tableau::d_activeRows" << endl;
112
113 typedef RowsTable::iterator table_iter;
114 for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end();
115 rowIter != end; ++rowIter){
116 ReducedRowVector* row_k = *rowIter;
117 if(row_k != NULL){
118 row_k->printRow();
119 }
120 }
121 }