diff options
Diffstat (limited to 'src/theory/arith/row_vector.cpp')
-rw-r--r-- | src/theory/arith/row_vector.cpp | 316 |
1 files changed, 0 insertions, 316 deletions
diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp deleted file mode 100644 index 8edfb8612..000000000 --- a/src/theory/arith/row_vector.cpp +++ /dev/null @@ -1,316 +0,0 @@ - -#include "theory/arith/row_vector.h" - -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::arith; - -using namespace std; - -bool ReducedRowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) { - if(arr.size() >= 2){ - const_iterator curr = arr.begin(); - const_iterator end = arr.end(); - ArithVar prev = (*curr).getArithVar(); - ++curr; - for(;curr != end; ++curr){ - ArithVar v = (*curr).getArithVar(); - if(strictlySorted && prev > v) return false; - if(!strictlySorted && prev >= v) return false; - prev = v; - } - } - return true; -} - -ReducedRowVector::~ReducedRowVector(){ - //This executes before the super classes destructor RowVector, - // which will set this to 0. - Assert(d_rowCount[basic()] == 1); - - const_iterator curr = begin(); - const_iterator endEntries = end(); - for(;curr != endEntries; ++curr){ - ArithVar v = (*curr).getArithVar(); - Assert(d_rowCount[v] >= 1); - d_columnMatrix[v].remove(basic()); - --(d_rowCount[v]); - } - - Assert(matchingCounts()); -} - - -bool ReducedRowVector::matchingCounts() const{ - for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ - ArithVar v = (*i).getArithVar(); - if(d_columnMatrix[v].size() != d_rowCount[v]){ - return false; - } - } - return true; -} - -bool ReducedRowVector::noZeroCoefficients(const VarCoeffArray& arr){ - for(const_iterator curr = arr.begin(), endEntries = arr.end(); - curr != endEntries; ++curr){ - const Rational& coeff = (*curr).getCoefficient(); - if(coeff == 0) return false; - } - return true; -} - -void ReducedRowVector::zip(const std::vector< ArithVar >& variables, - const std::vector< Rational >& coefficients, - VarCoeffArray& output){ - - Assert(coefficients.size() == variables.size() ); - - vector<Rational>::const_iterator coeffIter = coefficients.begin(); - vector<Rational>::const_iterator coeffEnd = coefficients.end(); - vector<ArithVar>::const_iterator varIter = variables.begin(); - - for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){ - const Rational& coeff = *coeffIter; - ArithVar var_i = *varIter; - - output.push_back(VarCoeffPair(var_i, coeff)); - } -} - -void ReducedRowVector::addArithVar(ArithVarContainsSet& contains, ArithVar v){ - if(v >= contains.size()){ - contains.resize(v+1, false); - } - contains[v] = true; -} - -void ReducedRowVector::removeArithVar(ArithVarContainsSet& contains, ArithVar v){ - Assert(v < contains.size()); - Assert(contains[v]); - contains[v] = false; -} - -void ReducedRowVector::multiply(const Rational& c){ - Assert(c != 0); - - for(iterator i = d_entries.begin(), end = d_entries.end(); i != end; ++i){ - (*i).getCoefficient() *= c; - } -} - -void ReducedRowVector::addRowTimesConstant(const Rational& c, const ReducedRowVector& other){ - Assert(c != 0); - Assert(d_buffer.empty()); - Assert(wellFormed()); - - d_buffer.reserve(other.d_entries.size()); - - iterator curr1 = d_entries.begin(); - iterator end1 = d_entries.end(); - - const_iterator curr2 = other.d_entries.begin(); - const_iterator end2 = other.d_entries.end(); - - while(curr1 != end1 && curr2 != end2){ - ArithVar var1 = (*curr1).getArithVar(); - ArithVar var2 = (*curr2).getArithVar(); - - if(var1 < var2){ - d_buffer.push_back(*curr1); - ++curr1; - }else if(var1 > var2){ - - ++d_rowCount[var2]; - d_columnMatrix[var2].add(d_basic); - - addArithVar(d_contains, var2); - const Rational& coeff2 = (*curr2).getCoefficient(); - d_buffer.push_back( VarCoeffPair(var2, c * coeff2)); - ++curr2; - }else{ - Assert(var1 == var2); - const Rational& coeff1 = (*curr1).getCoefficient(); - const Rational& coeff2 = (*curr2).getCoefficient(); - Rational res = coeff1 + (c * coeff2); - if(res != 0){ - //The variable is not new so the count stays the same - d_buffer.push_back(VarCoeffPair(var1, res)); - }else{ - removeArithVar(d_contains, var1); - - --d_rowCount[var1]; - d_columnMatrix[var1].remove(d_basic); - } - ++curr1; - ++curr2; - } - } - while(curr1 != end1){ - d_buffer.push_back(*curr1); - ++curr1; - } - while(curr2 != end2){ - ArithVar var2 = (*curr2).getArithVar(); - const Rational& coeff2 = (*curr2).getCoefficient(); - ++d_rowCount[var2]; - d_columnMatrix[var2].add(d_basic); - - addArithVar(d_contains, var2); - - d_buffer.push_back(VarCoeffPair(var2, c * coeff2)); - ++curr2; - } - - d_buffer.swap(d_entries); - d_buffer.clear(); - - Assert(d_buffer.empty()); -} - -void ReducedRowVector::printRow(){ - for(const_iterator i = begin(); i != end(); ++i){ - ArithVar nb = (*i).getArithVar(); - const Rational& coeff = (*i).getCoefficient(); - Debug("row::print") << "{" << nb << "," << coeff << "}"; - } - Debug("row::print") << std::endl; -} - - -ReducedRowVector::ReducedRowVector(ArithVar basic, - const std::vector<ArithVar>& variables, - const std::vector<Rational>& coefficients, - std::vector<uint32_t>& counts, - std::vector<PermissiveBackArithVarSet>& cm): - d_basic(basic), d_rowCount(counts), d_columnMatrix(cm) -{ - zip(variables, coefficients, d_entries); - d_entries.push_back(VarCoeffPair(basic, Rational(-1))); - - std::sort(d_entries.begin(), d_entries.end()); - - for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ - ArithVar var = (*i).getArithVar(); - ++d_rowCount[var]; - addArithVar(d_contains, var); - d_columnMatrix[var].add(d_basic); - } - - Assert(isSorted(d_entries, true)); - Assert(noZeroCoefficients(d_entries)); - - Assert(matchingCounts()); - Assert(wellFormed()); - Assert(d_rowCount[d_basic] == 1); -} - -void ReducedRowVector::substitute(const ReducedRowVector& row_s){ - ArithVar x_s = row_s.basic(); - - Assert(has(x_s)); - Assert(x_s != basic()); - - Rational a_rs = lookup(x_s); - Assert(a_rs != 0); - - addRowTimesConstant(a_rs, row_s); - - - Assert(!has(x_s)); - Assert(wellFormed()); - Assert(matchingCounts()); - Assert(d_rowCount[basic()] == 1); -} - -void ReducedRowVector::pivot(ArithVar x_j){ - Assert(has(x_j)); - Assert(basic() != x_j); - Rational negInverseA_rs = -(lookup(x_j).inverse()); - multiply(negInverseA_rs); - - for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ - ArithVar var = (*i).getArithVar(); - d_columnMatrix[var].remove(d_basic); - d_columnMatrix[var].add(x_j); - } - - d_basic = x_j; - - Assert(matchingCounts()); - Assert(wellFormed()); - //The invariant Assert(d_rowCount[basic()] == 1); does not hold. - //This is because the pivot is within the row first then - //is moved through the propagated through the rest of the tableau. -} - - -Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{ - using namespace CVC4::kind; - - Assert(size() >= 2); - - vector<Node> nonBasicPairs; - for(const_iterator i = begin(); i != end(); ++i){ - ArithVar nb = (*i).getArithVar(); - if(nb == basic()) continue; - Node var = (map.find(nb))->second; - Node coeff = mkRationalNode((*i).getCoefficient()); - - Node mult = NodeBuilder<2>(MULT) << coeff << var; - nonBasicPairs.push_back(mult); - } - - Node sum = Node::null(); - if(nonBasicPairs.size() == 1 ){ - sum = nonBasicPairs.front(); - }else{ - Assert(nonBasicPairs.size() >= 2); - NodeBuilder<> sumBuilder(PLUS); - sumBuilder.append(nonBasicPairs); - sum = sumBuilder; - } - Node basicVar = (map.find(basic()))->second; - return NodeBuilder<2>(EQUAL) << basicVar << sum; - - /* - Node sum = Node::null(); - if(size() > 2){ - NodeBuilder<> sumBuilder(PLUS); - - for(const_iterator i = begin(); i != end(); ++i){ - ArithVar nb = (*i).getArithVar(); - if(nb == basic()) continue; - Node var = (map.find(nb))->second; - Node coeff = mkRationalNode((*i).getCoefficient()); - - Node mult = NodeBuilder<2>(MULT) << coeff << var; - sumBuilder << mult; - } - sum = sumBuilder; - }else{ - Assert(size() == 2); - const_iterator i = begin(); - if((*i).getArithVar() == basic()){ - ++i; - } - Assert((*i).getArithVar() != basic()); - Node var = (map.find((*i).getArithVar()))->second; - Node coeff = mkRationalNode((*i).getCoefficient()); - sum = NodeBuilder<2>(MULT) << coeff << var; - } - Node basicVar = (map.find(basic()))->second; - return NodeBuilder<2>(EQUAL) << basicVar << sum; -*/ -} - -void ReducedRowVector::enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,std::vector< Rational >& coefficients) const{ - for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ - ArithVar var = (*i).getArithVar(); - const Rational& q = (*i).getCoefficient(); - if(var != basic()){ - variables.push_back(var); - coefficients.push_back(q); - } - } -} |