arith_priority_queue.cpp \
simplex.h \
simplex.cpp \
- row_vector.h \
- row_vector.cpp \
unate_propagator.h \
unate_propagator.cpp \
theory_arith.h \
std::vector<unsigned> d_posVector;
public:
- typedef VarList::const_iterator iterator;
+ typedef VarList::const_iterator const_iterator;
ArithVarSetImpl() : d_list(), d_posVector() {}
d_list.push_back(x);
}
- iterator begin() const{ return d_list.begin(); }
- iterator end() const{ return d_list.end(); }
+ const_iterator begin() const{ return d_list.begin(); }
+ const_iterator end() const{ return d_list.end(); }
const VarList& getList() const{
return d_list;
+++ /dev/null
-
-#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);
- }
- }
-}
+++ /dev/null
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__ROW_VECTOR_H
-#define __CVC4__THEORY__ARITH__ROW_VECTOR_H
-
-#include "theory/arith/arith_utilities.h"
-#include "theory/arith/arithvar_set.h"
-#include "util/rational.h"
-#include <vector>
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class VarCoeffPair {
-private:
- ArithVar d_variable;
- Rational d_coeff;
-
-public:
- VarCoeffPair(ArithVar v, const Rational& q): d_variable(v), d_coeff(q) {}
-
- ArithVar getArithVar() const { return d_variable; }
- Rational& getCoefficient() { return d_coeff; }
- const Rational& getCoefficient() const { return d_coeff; }
-
- bool operator<(const VarCoeffPair& other) const{
- return getArithVar() < other.getArithVar();
- }
-
- static bool variableLess(const VarCoeffPair& a, const VarCoeffPair& b){
- return a < b;
- }
-};
-
-/**
- * ReducedRowVector is a sparse vector representation that represents the
- * row as a strictly sorted array of "VarCoeffPair"s.
- * The row has a notion of a basic variable.
- * This is a variable that must have a coefficient of -1 in the array.
- */
-class ReducedRowVector {
-public:
- typedef std::vector<VarCoeffPair> VarCoeffArray;
- typedef VarCoeffArray::const_iterator const_iterator;
-
-private:
- typedef std::vector<bool> ArithVarContainsSet;
- typedef VarCoeffArray::iterator iterator;
-
- /**
- * Invariants:
- * - isSorted(d_entries, true)
- * - noZeroCoefficients(d_entries)
- */
- VarCoeffArray d_entries;
-
- /**
- * Buffer for d_entries to reduce allocations by addRowTimesConstant.
- */
- VarCoeffArray d_buffer;
-
- /**
- * The basic variable associated with the row.
- * Must have a coefficient of -1.
- */
- ArithVar d_basic;
-
-
- /**
- * Invariants:
- * - This set is the same as the set maintained in d_entries.
- */
- ArithVarContainsSet d_contains;
-
- std::vector<uint32_t>& d_rowCount;
- std::vector<PermissiveBackArithVarSet>& d_columnMatrix;
-
-
-public:
-
- ReducedRowVector(ArithVar basic,
- const std::vector< ArithVar >& variables,
- const std::vector< Rational >& coefficients,
- std::vector<uint32_t>& count,
- std::vector< PermissiveBackArithVarSet >& columnMatrix);
- ~ReducedRowVector();
-
- void enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,
- std::vector< Rational >& coefficients) const;
-
- /** Returns the basic variable.*/
- ArithVar basic() const{
- Assert(basicIsSet());
- return d_basic;
- }
-
- /** Returns the number of nonzero variables in the vector. */
- uint32_t size() const {
- return d_entries.size();
- }
-
- /** Iterates over the nonzero entries in the vector. */
- const_iterator begin() const { return d_entries.begin(); }
- const_iterator end() const { return d_entries.end(); }
-
- /** Returns true if the variable is in the row. */
- bool has(ArithVar x_j) const{
- if(x_j >= d_contains.size()){
- return false;
- }else{
- return d_contains[x_j];
- }
- }
-
- /**
- * Returns the coefficient of a variable in the row.
- */
- const Rational& lookup(ArithVar x_j) const{
- Assert(has(x_j));
- Assert(hasInEntries(x_j));
- const_iterator lb = lower_bound(x_j);
- return (*lb).getCoefficient();
- }
-
-
- /** Prints the row to the buffer Debug("row::print"). */
- void printRow();
-
- /**
- * Changes the basic variable to x_j.
- * Precondition: has(x_j)
- */
- void pivot(ArithVar x_j);
-
- /**
- * Replaces other.basic() in the current row using the other row.
- * This assumes the other row represents an equality equal to zero.
- *
- * \sum(this->entries) -= this->lookup(other.basic()) * (\sum(other.d_entries))
- * Precondition:
- * has(other.basic())
- * basic != other.basic()
- */
- void substitute(const ReducedRowVector& other);
-
- /**
- * Returns the reduced row as an equality with
- * the basic variable on the lhs equal to the sum of the non-basics variables.
- * The mapped from ArithVars to Nodes is specificied by map.
- */
- Node asEquality(const ArithVarToNodeMap& map) const;
-
-private:
-
- /**
- * \sum(this->entries) += c * (\sum(other.d_entries) )
- *
- * Updates the current row to be the sum of itself and
- * another vector times c (c != 0).
- */
- void addRowTimesConstant(const Rational& c, const ReducedRowVector& other);
-
-
- /** Multiplies the coefficients of the RowVector by c (where c != 0). */
- void multiply(const Rational& c);
-
- /**
- * Adds v to d_contains.
- * This may resize d_contains.
- */
- static void addArithVar(ArithVarContainsSet& contains, ArithVar v);
-
- /** Removes v from d_contains. */
- static void removeArithVar(ArithVarContainsSet& contains, ArithVar v);
-
-
- /**
- * Let c be -1 if strictlySorted is true and c be 0 otherwise.
- * isSorted(arr, strictlySorted) is then equivalent to
- * If i<j, cmp(getArithVar(d_entries[i]), getArithVar(d_entries[j])) <= c.
- */
- static bool isSorted(const VarCoeffArray& arr, bool strictlySorted);
-
- /**
- * Zips together an array of variables and coefficients and appends
- * it to the end of an output vector.
- */
- static void zip(const std::vector< ArithVar >& variables,
- const std::vector< Rational >& coefficients,
- VarCoeffArray& output);
-
- /**
- * Debugging code.
- * noZeroCoefficients(arr) is equivalent to
- * 0 != getCoefficient(arr[i]) for all i.
- */
- static bool noZeroCoefficients(const VarCoeffArray& arr);
-
- /** Debugging code.*/
- bool matchingCounts() const;
-
- const_iterator lower_bound(ArithVar x_j) const{
- return std::lower_bound(d_entries.begin(), d_entries.end(), VarCoeffPair(x_j, 0));
- }
-
- /** Debugging code */
- bool wellFormed() const{
- return
- isSorted(d_entries, true) &&
- noZeroCoefficients(d_entries) &&
- basicIsSet() &&
- has(basic()) &&
- lookup(basic()) == Rational(-1);
- }
-
- bool basicIsSet() const { return d_basic != ARITHVAR_SENTINEL; }
-
- /** Debugging code. */
- bool hasInEntries(ArithVar x_j) const {
- return std::binary_search(d_entries.begin(), d_entries.end(), VarCoeffPair(x_j,0));
- }
-
-}; /* class ReducedRowVector */
-
-
-}/* namespace CVC4::theory::arith */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
-
-#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */
return Node::null();
}
-set<ArithVar> tableauAndHasSet(Tableau& tab, ArithVar v){
- set<ArithVar> has;
- for(ArithVarSet::iterator basicIter = tab.begin();
- basicIter != tab.end();
- ++basicIter){
- ArithVar basic = *basicIter;
- ReducedRowVector& row = tab.lookup(basic);
-
- if(row.has(v)){
- has.insert(basic);
- }
- }
- return has;
-}
-
-set<ArithVar> columnIteratorSet(Tableau& tab,ArithVar v){
- set<ArithVar> has;
- Column::iterator basicIter = tab.beginColumn(v);
- Column::iterator endIter = tab.endColumn(v);
- for(; basicIter != endIter; ++basicIter){
- ArithVar basic = *basicIter;
- has.insert(basic);
- }
- return has;
-}
-
-
+// set<ArithVar> tableauAndHasSet(Tableau& tab, ArithVar v){
+// set<ArithVar> has;
+// for(ArithVarSet::const_iterator basicIter = tab.beginBasic();
+// basicIter != tab.endBasic();
+// ++basicIter){
+// ArithVar basic = *basicIter;
+// ReducedRowVector& row = tab.lookup(basic);
+
+// if(row.has(v)){
+// has.insert(basic);
+// }
+// }
+// return has;
+// }
+
+// set<ArithVar> columnIteratorSet(Tableau& tab,ArithVar v){
+// set<ArithVar> has;
+// Column::iterator basicIter = tab.beginColumn(v);
+// Column::iterator endIter = tab.endColumn(v);
+// for(; basicIter != endIter; ++basicIter){
+// ArithVar basic = *basicIter;
+// has.insert(basic);
+// }
+// return has;
+// }
+
+
+/*
bool matchingSets(Tableau& tab, ArithVar v){
return tableauAndHasSet(tab, v) == columnIteratorSet(tab, v);
}
+*/
void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
Assert(!d_tableau.isBasic(x_i));
<< assignment_x_i << "|-> " << v << endl;
DeltaRational diff = v - assignment_x_i;
- Assert(matchingSets(d_tableau, x_i));
- Column::iterator basicIter = d_tableau.beginColumn(x_i);
- Column::iterator endIter = d_tableau.endColumn(x_i);
- for(; basicIter != endIter; ++basicIter){
- ArithVar x_j = *basicIter;
- ReducedRowVector& row_j = d_tableau.lookup(x_j);
+ //Assert(matchingSets(d_tableau, x_i));
+ Tableau::ColIterator basicIter = d_tableau.colIterator(x_i);
+ for(; !basicIter.atEnd(); ++basicIter){
+ const TableauEntry& entry = *basicIter;
+ Assert(entry.getColVar() == x_i);
+
+ ArithVar x_j = entry.getRowVar();
+ //ReducedRowVector& row_j = d_tableau.lookup(x_j);
- Assert(row_j.has(x_i));
- const Rational& a_ji = row_j.lookup(x_i);
+ //const Rational& a_ji = row_j.lookup(x_i);
+ const Rational& a_ji = entry.getCoefficient();
const DeltaRational& assignment = d_partialModel.getAssignment(x_j);
DeltaRational nAssignment = assignment+(diff * a_ji);
d_partialModel.setAssignment(x_i, v);
- Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_i));
- double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_i));
+ Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_i));
+ double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_i));
(d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference);
- if(Debug.isOn("paranoid:check_tableau")){
- checkTableau();
+ if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); }
+}
+
+void SimplexDecisionProcedure::debugPivotSimplex(ArithVar x_i, ArithVar x_j){
+ Debug("arith::simplex:row") << "debugRowSimplex("
+ << x_i << "|->" << x_j
+ << ")" << endl;
+
+ for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){
+ const TableauEntry& entry = *iter;
+
+ ArithVar var = entry.getColVar();
+ const Rational& coeff = entry.getCoefficient();
+ DeltaRational beta = d_partialModel.getAssignment(var);
+ Debug("arith::simplex:row") << var << beta << coeff;
+ if(d_partialModel.hasLowerBound(var)){
+ Debug("arith::simplex:row") << "(lb " << d_partialModel.getLowerBound(var) << ")";
+ }
+ if(d_partialModel.hasUpperBound(var)){
+ Debug("arith::simplex:row") << "(up " << d_partialModel.getUpperBound(var) << ")";
+ }
+ Debug("arith::simplex:row") << endl;
}
+ Debug("arith::simplex:row") << "end row"<< endl;
}
void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime);
- if(Debug.isOn("arith::pivotAndUpdate")){
- Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl;
- ReducedRowVector& row_k = d_tableau.lookup(x_i);
- for(ReducedRowVector::const_iterator varIter = row_k.begin();
- varIter != row_k.end();
- ++varIter){
-
- ArithVar var = (*varIter).getArithVar();
- const Rational& coeff = (*varIter).getCoefficient();
- DeltaRational beta = d_partialModel.getAssignment(var);
- Debug("arith::pivotAndUpdate") << var << beta << coeff;
- if(d_partialModel.hasLowerBound(var)){
- Debug("arith::pivotAndUpdate") << "(lb " << d_partialModel.getLowerBound(var) << ")";
- }
- if(d_partialModel.hasUpperBound(var)){
- Debug("arith::pivotAndUpdate") << "(up " << d_partialModel.getUpperBound(var)
- << ")";
- }
- Debug("arith::pivotAndUpdate") << endl;
- }
- Debug("arith::pivotAndUpdate") << "end row"<< endl;
- }
+ if(Debug.isOn("arith::simplex:row")){ debugPivotSimplex(x_i, x_j); }
+
+ const TableauEntry& entry_ij = d_tableau.findEntry(x_i, x_j);
+ Assert(!entry_ij.blank());
- ReducedRowVector& row_i = d_tableau.lookup(x_i);
- const Rational& a_ij = row_i.lookup(x_j);
+ const Rational& a_ij = entry_ij.getCoefficient();
const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i);
d_partialModel.setAssignment(x_j, tmp);
- Assert(matchingSets(d_tableau, x_j));
- Column::iterator basicIter = d_tableau.beginColumn(x_j);
- Column::iterator endIter = d_tableau.endColumn(x_j);
- for(; basicIter != endIter; ++basicIter){
- ArithVar x_k = *basicIter;
- ReducedRowVector& row_k = d_tableau.lookup(x_k);
-
- Assert(row_k.has(x_j));
+ //Assert(matchingSets(d_tableau, x_j));
+ for(Tableau::ColIterator iter = d_tableau.colIterator(x_j); !iter.atEnd(); ++iter){
+ const TableauEntry& entry = *iter;
+ Assert(entry.getColVar() == x_j);
+ ArithVar x_k = entry.getRowVar();
if(x_k != x_i ){
- const Rational& a_kj = row_k.lookup(x_j);
+ const Rational& a_kj = entry.getCoefficient();
DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
d_partialModel.setAssignment(x_k, nextAssignment);
// Pivots
++(d_statistics.d_statPivots);
- Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_j));
- double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_j));
+ Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_j));
+ double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_j));
(d_statistics.d_avgNumRowsNotContainingOnPivot).addEntry(difference);
d_tableau.pivot(x_i, x_j);
}
}
-ArithVar SimplexDecisionProcedure::minRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){
+ArithVar SimplexDecisionProcedure::minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){
Assert(x != ARITHVAR_SENTINEL);
Assert(y != ARITHVAR_SENTINEL);
Assert(!simp.d_tableau.isBasic(x));
Assert(!simp.d_tableau.isBasic(y));
- if(simp.d_tableau.getRowCount(x) > simp.d_tableau.getRowCount(y)){
- return y;
- } else {
+ uint32_t xLen = simp.d_tableau.getColLength(x);
+ uint32_t yLen = simp.d_tableau.getColLength(y);
+ if( xLen > yLen){
+ return y;
+ } else if( xLen== yLen ){
+ return minVarOrder(simp,x,y);
+ }else{
return x;
}
}
}else if(!simp.d_partialModel.hasEitherBound(x) && simp.d_partialModel.hasEitherBound(y)){
return x;
}else {
- return minRowCount(simp, x, y);
+ return minColLength(simp, x, y);
}
}
template <bool above, SimplexDecisionProcedure::PreferenceFunction pref>
ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
- ReducedRowVector& row_i = d_tableau.lookup(x_i);
-
ArithVar slack = ARITHVAR_SENTINEL;
- for(ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
- nbi != end; ++nbi){
- ArithVar nonbasic = (*nbi).getArithVar();
+ for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){
+ const TableauEntry& entry = *iter;
+ ArithVar nonbasic = entry.getColVar();
if(nonbasic == x_i) continue;
- const Rational& a_ij = (*nbi).getCoefficient();
+ const Rational& a_ij = entry.getCoefficient();
int sgn = a_ij.sgn();
- if(( above && sgn < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
- ( above && sgn > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)) ||
- (!above && sgn > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
- (!above && sgn < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic))) {
+ if(isAcceptableSlack<above>(sgn, nonbasic)){
//If one of the above conditions is met, we have found an acceptable
//nonbasic variable to pivot x_i with. We can now choose which one we
//prefer the most.
Assert(remainingIterations > 0);
while(remainingIterations > 0){
- if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
+ if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); }
ArithVar x_i = d_queue.dequeueInconsistentBasicVariable();
Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
- ReducedRowVector& row_i = d_tableau.lookup(conflictVar);
-
NodeBuilder<> nb(kind::AND);
TNode bound = d_partialModel.getUpperConstraint(conflictVar);
nb << bound;
- ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
-
- for(; nbi != end; ++nbi){
- ArithVar nonbasic = (*nbi).getArithVar();
+ Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar);
+ for(; !iter.atEnd(); ++iter){
+ const TableauEntry& entry = *iter;
+ ArithVar nonbasic = entry.getColVar();
if(nonbasic == conflictVar) continue;
- const Rational& a_ij = (*nbi).getCoefficient();
+ const Rational& a_ij = entry.getCoefficient();
Assert(a_ij != d_ZERO);
int sgn = a_ij.sgn();
}
Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
- ReducedRowVector& row_i = d_tableau.lookup(conflictVar);
-
NodeBuilder<> nb(kind::AND);
TNode bound = d_partialModel.getLowerConstraint(conflictVar);
nb << bound;
- ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
- for(; nbi != end; ++nbi){
- ArithVar nonbasic = (*nbi).getArithVar();
+ Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar);
+ for(; !iter.atEnd(); ++iter){
+ const TableauEntry& entry = *iter;
+ ArithVar nonbasic = entry.getColVar();
if(nonbasic == conflictVar) continue;
- const Rational& a_ij = (*nbi).getCoefficient();
+ const Rational& a_ij = entry.getCoefficient();
int sgn = a_ij.sgn();
Assert(a_ij != d_ZERO);
Assert(d_tableau.isBasic(x));
DeltaRational sum(0);
- ReducedRowVector& row = d_tableau.lookup(x);
- for(ReducedRowVector::const_iterator i = row.begin(), end = row.end();
- i != end;++i){
- ArithVar nonbasic = (*i).getArithVar();
- if(nonbasic == row.basic()) continue;
- const Rational& coeff = (*i).getCoefficient();
+ for(Tableau::RowIterator i = d_tableau.rowIterator(x); !i.atEnd(); ++i){
+ const TableauEntry& entry = (*i);
+ ArithVar nonbasic = entry.getColVar();
+ if(nonbasic == x) continue;
+ const Rational& coeff = entry.getCoefficient();
const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe);
sum = sum + (assignment * coeff);
* checkTableau();
* }
*/
-void SimplexDecisionProcedure::checkTableau(){
-
- for(ArithVarSet::iterator basicIter = d_tableau.begin();
- basicIter != d_tableau.end(); ++basicIter){
+void SimplexDecisionProcedure::debugCheckTableau(){
+ ArithVarSet::const_iterator basicIter = d_tableau.beginBasic();
+ ArithVarSet::const_iterator endIter = d_tableau.endBasic();
+ for(; basicIter != endIter; ++basicIter){
ArithVar basic = *basicIter;
- ReducedRowVector& row_k = d_tableau.lookup(basic);
DeltaRational sum;
Debug("paranoid:check_tableau") << "starting row" << basic << endl;
- for(ReducedRowVector::const_iterator nonbasicIter = row_k.begin();
- nonbasicIter != row_k.end();
- ++nonbasicIter){
- ArithVar nonbasic = (*nonbasicIter).getArithVar();
+ Tableau::RowIterator nonbasicIter = d_tableau.rowIterator(basic);
+ for(; !nonbasicIter.atEnd(); ++nonbasicIter){
+ const TableauEntry& entry = *nonbasicIter;
+ ArithVar nonbasic = entry.getColVar();
if(basic == nonbasic) continue;
- const Rational& coeff = (*nonbasicIter).getCoefficient();
+ const Rational& coeff = entry.getCoefficient();
DeltaRational beta = d_partialModel.getAssignment(nonbasic);
Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl;
sum = sum + (beta*coeff);
* This is a hueristic rule and should not be used
* during the VarOrder stage of updateInconsistentVars.
*/
- static ArithVar minRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
+ static ArithVar minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
/**
* minBoundAndRowCount is a PreferenceFunction for preferring a variable
* without an asserted bound over variables with an asserted bound.
* Checks to make sure the assignment is consistent with the tableau.
* This code is for debugging.
*/
- void checkTableau();
+ void debugCheckTableau();
+ void debugPivotSimplex(ArithVar x_i, ArithVar x_j);
+
/**
* Computes the value of a basic variable using the assignments
pushLemma(negatedConflict);
}
+ template <bool above>
+ inline bool isAcceptableSlack(int sgn, ArithVar nonbasic){
+ return
+ ( above && sgn < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
+ ( above && sgn > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)) ||
+ (!above && sgn > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
+ (!above && sgn < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic));
+ }
+
/**
* Checks a basic variable, b, to see if it is in conflict.
* If a conflict is discovered a node summarizing the conflict is returned.
using namespace CVC4::theory::arith;
-Tableau::Tableau(const Tableau& tab){
- internalCopy(tab);
-}
-
-void Tableau::internalCopy(const Tableau& tab){
- uint32_t N = tab.d_rowsTable.size();
-
- Debug("tableau::copy") << "tableau copy "<< N << endl;
-
- if(N > 1){
- d_columnMatrix.insert(d_columnMatrix.end(), N, Column());
- d_rowsTable.insert(d_rowsTable.end(), N, NULL);
- d_basicVariables.increaseSize(N-1);
-
- Assert(d_basicVariables.allocated() == tab.d_basicVariables.allocated());
-
- d_rowCount.insert(d_rowCount.end(), N, 0);
- }
-
- ColumnMatrix::const_iterator otherIter = tab.d_columnMatrix.begin();
- ColumnMatrix::iterator i_colIter = d_columnMatrix.begin();
- ColumnMatrix::iterator end_colIter = d_columnMatrix.end();
- for(; i_colIter != end_colIter; ++i_colIter, ++otherIter){
- Assert(otherIter != tab.d_columnMatrix.end());
- Column& col = *i_colIter;
- const Column& otherCol = *otherIter;
- col.increaseSize(otherCol.allocated());
- }
-
- ArithVarSet::iterator i_basicIter = tab.d_basicVariables.begin();
- ArithVarSet::iterator i_basicEnd = tab.d_basicVariables.end();
- for(; i_basicIter != i_basicEnd; ++i_basicIter){
- ArithVar basicVar = *i_basicIter;
- const ReducedRowVector* otherRow = tab.d_rowsTable[basicVar];
-
- Assert(otherRow != NULL);
-
- std::vector< ArithVar > variables;
- std::vector< Rational > coefficients;
- otherRow->enqueueNonBasicVariablesAndCoefficients(variables, coefficients);
-
- ReducedRowVector* copy = new ReducedRowVector(basicVar, variables, coefficients, d_rowCount, d_columnMatrix);
-
- Debug("tableau::copy") << "copying " << basicVar << endl;
- copy->printRow();
-
- d_basicVariables.add(basicVar);
- d_rowsTable[basicVar] = copy;
- }
-}
-
-Tableau& Tableau::operator=(const Tableau& other){
- clear();
- internalCopy(other);
- return (*this);
-}
-
-Tableau::~Tableau(){
- clear();
-}
-
-void Tableau::clear(){
- while(!d_basicVariables.empty()){
- ArithVar curr = *(d_basicVariables.begin());
- ReducedRowVector* vec = removeRow(curr);
- delete vec;
- }
-
- d_rowsTable.clear();
- d_basicVariables.clear();
- d_rowCount.clear();
- d_columnMatrix.clear();
-}
-
+/*
void Tableau::addRow(ArithVar basicVar,
const std::vector<Rational>& coeffs,
const std::vector<ArithVar>& variables){
ArithVar var = *varsIter;
if(d_basicVariables.isMember(var)){
- ReducedRowVector& row_var = lookup(var);
- row_current->substitute(row_var);
+ EntryID varID = find(basicVar, var);
+ TableauEntry& entry = d_entryManager.get(varID);
+ const Rational& coeff = entry.getCoefficient();
+
+ loadRowIntoMergeBuffer(var);
+ rowPlusRowTimesConstant(coeff, basicVar, var);
+ emptyRowFromMergeBuffer(var);
}
}
}
+*/
+/*
ReducedRowVector* Tableau::removeRow(ArithVar basic){
- Assert(d_basicVariables.isMember(basic));
+ Assert(isBasic(basic));
ReducedRowVector* row = d_rowsTable[basic];
return row;
}
+*/
-void Tableau::pivot(ArithVar x_r, ArithVar x_s){
- Assert(d_basicVariables.isMember(x_r));
- Assert(!d_basicVariables.isMember(x_s));
+void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic){
+ Assert(isBasic(oldBasic));
+ Assert(!isBasic(newBasic));
+ Assert(mergeBufferIsEmpty());
- Debug("tableau") << "Tableau::pivot(" << x_r <<", " <<x_s <<")" << endl;
+ //cout << oldBasic << "," << newBasic << endl;
+ Debug("tableau") << "Tableau::pivot(" << oldBasic <<", " << newBasic <<")" << endl;
- ReducedRowVector* row_s = d_rowsTable[x_r];
- Assert(row_s != NULL);
- Assert(row_s->has(x_s));
+ rowPivot(oldBasic, newBasic);
+ loadRowIntoMergeBuffer(newBasic);
- //Swap x_r and x_s in d_activeRows
- d_rowsTable[x_s] = row_s;
- d_rowsTable[x_r] = NULL;
+ ColIterator colIter = colIterator(newBasic);
+ while(!colIter.atEnd()){
+ EntryID id = colIter.getID();
+ TableauEntry& entry = d_entryManager.get(id);
- d_basicVariables.remove(x_r);
+ ++colIter; //needs to be incremented before the variable is removed
+ if(entry.getRowVar() == newBasic){ continue; }
- d_basicVariables.add(x_s);
+ ArithVar basicTo = entry.getRowVar();
+ Rational coeff = entry.getCoefficient();
- row_s->pivot(x_s);
+ rowPlusRowTimesConstant(basicTo, coeff, newBasic);
+ }
+ emptyRowFromMergeBuffer(newBasic);
- Column::VarList copy(getColumn(x_s).getList());
- vector<ArithVar>::iterator basicIter = copy.begin(), endIter = copy.end();
+ //Clear the column for used for this variable
- for(; basicIter != endIter; ++basicIter){
- ArithVar basic = *basicIter;
- if(basic == x_s) continue;
+ Assert(mergeBufferIsEmpty());
+ Assert(!isBasic(oldBasic));
+ Assert(isBasic(newBasic));
+ Assert(getColLength(newBasic) == 1);
+}
- ReducedRowVector& row_k = lookup(basic);
- Assert(row_k.has(x_s));
+Tableau::~Tableau(){}
- row_k.substitute(*row_s);
+void Tableau::setColumnUnused(ArithVar v){
+ ColIterator colIter = colIterator(v);
+ while(!colIter.atEnd()){
+ ++colIter;
}
- Assert(getColumn(x_s).size() == 1);
- Assert(getRowCount(x_s) == 1);
}
-
void Tableau::printTableau(){
Debug("tableau") << "Tableau::d_activeRows" << endl;
- typedef RowsTable::iterator table_iter;
- for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end();
- rowIter != end; ++rowIter){
- ReducedRowVector* row_k = *rowIter;
- if(row_k != NULL){
- row_k->printRow();
- }
+ ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic();
+ for(; basicIter != endIter; ++basicIter){
+ ArithVar basic = *basicIter;
+ printRow(basic);
}
}
-uint32_t Tableau::numNonZeroEntries() const {
- uint32_t colSum = 0;
- ColumnMatrix::const_iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end();
- for(; i != end; ++i){
- const Column& col = *i;
- colSum += col.size();
+void Tableau::printRow(ArithVar basic){
+ Debug("tableau") << "{" << basic << ":";
+ for(RowIterator entryIter = rowIterator(basic); !entryIter.atEnd(); ++entryIter){
+ const TableauEntry& entry = *entryIter;
+ printEntry(entry);
+ Debug("tableau") << ",";
}
- return colSum;
+ Debug("tableau") << "}" << endl;
+}
+
+void Tableau::printEntry(const TableauEntry& entry){
+ Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient();
}
uint32_t Tableau::numNonZeroEntriesByRow() const {
uint32_t rowSum = 0;
- ArithVarSet::iterator i = d_basicVariables.begin(), end = d_basicVariables.end();
+ ArithVarSet::const_iterator i = d_basicVariables.begin(), end = d_basicVariables.end();
for(; i != end; ++i){
ArithVar basic = *i;
- const ReducedRowVector& row = *(d_rowsTable[basic]);
- rowSum += row.size();
+ rowSum += getRowLength(basic);
}
return rowSum;
}
+
+uint32_t Tableau::numNonZeroEntriesByCol() const {
+ uint32_t colSum = 0;
+ VectorSizeTable::const_iterator i = d_colLengths.begin();
+ VectorSizeTable::const_iterator end = d_colLengths.end();
+ for(; i != end; ++i){
+ colSum += *i;
+ }
+ return colSum;
+}
+
+
+EntryID Tableau::findOnRow(ArithVar row, ArithVar col){
+ for(RowIterator i = rowIterator(row); !i.atEnd(); ++i){
+ EntryID id = i.getID();
+ const TableauEntry& entry = *i;
+ ArithVar colVar = entry.getColVar();
+
+ if(colVar == col){
+ return id;
+ }
+ }
+ return ENTRYID_SENTINEL;
+}
+
+EntryID Tableau::findOnCol(ArithVar row, ArithVar col){
+ for(ColIterator i = colIterator(col); !i.atEnd(); ++i){
+ EntryID id = i.getID();
+ const TableauEntry& entry = *i;
+ ArithVar rowVar = entry.getRowVar();
+
+ if(rowVar == row){
+ return id;
+ }
+ }
+ return ENTRYID_SENTINEL;
+}
+
+const TableauEntry& Tableau::findEntry(ArithVar row, ArithVar col){
+ bool colIsShorter = getColLength(col) < getRowLength(row);
+ EntryID id = colIsShorter ? findOnCol(row,col) : findOnRow(row,col);
+ if(id == ENTRYID_SENTINEL){
+ return d_failedFind;
+ }else{
+ return d_entryManager.get(id);
+ }
+}
+
+void Tableau::removeRow(ArithVar basic){
+ RowIterator i = rowIterator(basic);
+ while(!i.atEnd()){
+ EntryID id = i.getID();
+ ++i;
+ removeEntry(id);
+ }
+ d_basicVariables.remove(basic);
+}
+
+void Tableau::loadRowIntoMergeBuffer(ArithVar basic){
+ Assert(mergeBufferIsEmpty());
+ for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
+ EntryID id = i.getID();
+ const TableauEntry& entry = *i;
+ ArithVar colVar = entry.getColVar();
+ d_mergeBuffer[colVar] = make_pair(id, false);
+ }
+}
+
+void Tableau::emptyRowFromMergeBuffer(ArithVar basic){
+ Assert(isBasic(basic));
+ for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
+ const TableauEntry& entry = *i;
+ ArithVar colVar = entry.getColVar();
+ Assert(d_mergeBuffer[colVar].first == i.getID());
+ d_mergeBuffer[colVar] = make_pair(ENTRYID_SENTINEL, false);
+ }
+
+ Assert(mergeBufferIsEmpty());
+}
+
+
+/**
+ * Changes basic to newbasic (a variable on the row).
+ */
+void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew){
+ Assert(mergeBufferIsEmpty());
+ Assert(isBasic(basicOld));
+ Assert(!isBasic(basicNew));
+
+ EntryID newBasicID = findOnRow(basicOld, basicNew);
+
+ Assert(newBasicID != ENTRYID_SENTINEL);
+
+ TableauEntry& newBasicEntry = d_entryManager.get(newBasicID);
+ Rational negInverseA_rs = -(newBasicEntry.getCoefficient().inverse());
+
+ for(RowIterator i = rowIterator(basicOld); !i.atEnd(); ++i){
+ EntryID id = i.getID();
+ TableauEntry& entry = d_entryManager.get(id);
+
+ entry.getCoefficient() *= negInverseA_rs;
+ entry.setRowVar(basicNew);
+ }
+
+ d_rowHeads[basicNew] = d_rowHeads[basicOld];
+ d_rowHeads[basicOld] = ENTRYID_SENTINEL;
+
+ d_rowLengths[basicNew] = d_rowLengths[basicOld];
+ d_rowLengths[basicOld] = 0;
+
+ d_basicVariables.remove(basicOld);
+ d_basicVariables.add(basicNew);
+}
+
+void Tableau::addEntry(ArithVar row, ArithVar col, const Rational& coeff){
+ Assert(coeff != 0);
+
+ EntryID newId = d_entryManager.newEntry();
+ TableauEntry& newEntry = d_entryManager.get(newId);
+ newEntry = TableauEntry( row, col,
+ d_rowHeads[row], d_colHeads[col],
+ ENTRYID_SENTINEL, ENTRYID_SENTINEL,
+ coeff);
+ Assert(newEntry.getCoefficient() != 0);
+
+ Debug("tableau") << "addEntry(" << row << "," << col <<"," << coeff << ")" << endl;
+
+ ++d_entriesInUse;
+
+ if(d_rowHeads[row] != ENTRYID_SENTINEL)
+ d_entryManager.get(d_rowHeads[row]).setPrevRowID(newId);
+
+ if(d_colHeads[col] != ENTRYID_SENTINEL)
+ d_entryManager.get(d_colHeads[col]).setPrevColID(newId);
+
+ d_rowHeads[row] = newId;
+ d_colHeads[col] = newId;
+ ++d_rowLengths[row];
+ ++d_colLengths[col];
+}
+
+void Tableau::removeEntry(EntryID id){
+ Assert(d_entriesInUse > 0);
+ --d_entriesInUse;
+
+ TableauEntry& entry = d_entryManager.get(id);
+
+ ArithVar row = entry.getRowVar();
+ ArithVar col = entry.getColVar();
+
+ Assert(d_rowLengths[row] > 0);
+ Assert(d_colLengths[col] > 0);
+
+
+ --d_rowLengths[row];
+ --d_colLengths[col];
+
+ EntryID prevRow = entry.getPrevRowID();
+ EntryID prevCol = entry.getPrevColID();
+
+ EntryID nextRow = entry.getNextRowID();
+ EntryID nextCol = entry.getNextColID();
+
+ if(d_rowHeads[row] == id){
+ d_rowHeads[row] = nextRow;
+ }
+ if(d_colHeads[col] == id){
+ d_colHeads[col] = nextCol;
+ }
+
+ entry.markBlank();
+
+ if(prevRow != ENTRYID_SENTINEL){
+ d_entryManager.get(prevRow).setNextRowID(nextRow);
+ }
+ if(nextRow != ENTRYID_SENTINEL){
+ d_entryManager.get(nextRow).setPrevRowID(prevRow);
+ }
+
+ if(prevCol != ENTRYID_SENTINEL){
+ d_entryManager.get(prevCol).setNextColID(nextCol);
+ }
+ if(nextCol != ENTRYID_SENTINEL){
+ d_entryManager.get(nextCol).setPrevColID(prevCol);
+ }
+
+ d_entryManager.freeEntry(id);
+}
+
+void Tableau::rowPlusRowTimesConstant(ArithVar basicTo, const Rational& c, ArithVar basicFrom){
+
+ Debug("tableau") << "rowPlusRowTimesConstant("
+ << basicTo << "," << c << "," << basicFrom << ")"
+ << endl;
+
+ Assert(debugNoZeroCoefficients(basicTo));
+ Assert(debugNoZeroCoefficients(basicFrom));
+
+ Assert(c != 0);
+ Assert(isBasic(basicTo));
+ Assert(isBasic(basicFrom));
+ Assert( d_usedList.empty() );
+
+
+ RowIterator i = rowIterator(basicTo);
+ while(!i.atEnd()){
+ EntryID id = i.getID();
+ TableauEntry& entry = d_entryManager.get(id);
+ ArithVar colVar = entry.getColVar();
+
+ ++i;
+ if(bufferPairIsNotEmpty(d_mergeBuffer[colVar])){
+ d_mergeBuffer[colVar].second = true;
+ d_usedList.push_back(colVar);
+
+ EntryID inOtherRow = d_mergeBuffer[colVar].first;
+ const TableauEntry& other = d_entryManager.get(inOtherRow);
+ entry.getCoefficient() += c * other.getCoefficient();
+
+ if(entry.getCoefficient().sgn() == 0){
+ removeEntry(id);
+ }
+ }
+ }
+
+ for(RowIterator i = rowIterator(basicFrom); !i.atEnd(); ++i){
+ const TableauEntry& entry = *i;
+ ArithVar colVar = entry.getColVar();
+
+ if(!(d_mergeBuffer[colVar]).second){
+ Rational newCoeff = c * entry.getCoefficient();
+ addEntry(basicTo, colVar, newCoeff);
+ }
+ }
+
+ clearUsedList();
+
+ if(Debug.isOn("tableau")) { printTableau(); }
+}
+
+void Tableau::clearUsedList(){
+ ArithVarArray::iterator i, end;
+ for(i = d_usedList.begin(), end = d_usedList.end(); i != end; ++i){
+ ArithVar pos = *i;
+ d_mergeBuffer[pos].second = false;
+ }
+ d_usedList.clear();
+}
+
+void Tableau::addRow(ArithVar basic,
+ const std::vector<Rational>& coefficients,
+ const std::vector<ArithVar>& variables)
+{
+ Assert(coefficients.size() == variables.size() );
+ Assert(!isBasic(basic));
+
+ d_basicVariables.add(basic);
+
+ if(Debug.isOn("tableau")){ printTableau(); }
+
+ addEntry(basic, basic, Rational(-1));
+
+ 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){
+ const Rational& coeff = *coeffIter;
+ ArithVar var_i = *varsIter;
+ addEntry(basic, var_i, coeff);
+ }
+
+ varsIter = variables.begin();
+ coeffIter = coefficients.begin();
+ for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
+ ArithVar var = *varsIter;
+
+ if(isBasic(var)){
+ Rational coeff = *coeffIter;
+
+ loadRowIntoMergeBuffer(var);
+ rowPlusRowTimesConstant(basic, coeff, var);
+ emptyRowFromMergeBuffer(var);
+ }
+ }
+
+ if(Debug.isOn("tableau")) { printTableau(); }
+
+ Assert(debugNoZeroCoefficients(basic));
+
+ Assert(debugMatchingCountsForRow(basic));
+ Assert(getColLength(basic) == 1);
+}
+
+bool Tableau::debugNoZeroCoefficients(ArithVar basic){
+ for(RowIterator i=rowIterator(basic); !i.atEnd(); ++i){
+ const TableauEntry& entry = *i;
+ if(entry.getCoefficient() == 0){
+ return false;
+ }
+ }
+ return true;
+}
+bool Tableau::debugMatchingCountsForRow(ArithVar basic){
+ for(RowIterator i=rowIterator(basic); !i.atEnd(); ++i){
+ const TableauEntry& entry = *i;
+ ArithVar colVar = entry.getColVar();
+ uint32_t count = debugCountColLength(colVar);
+ Debug("tableau") << "debugMatchingCountsForRow "
+ << basic << ":" << colVar << " " << count
+ <<" "<< d_colLengths[colVar] << endl;
+ if( count != d_colLengths[colVar] ){
+ return false;
+ }
+ }
+ return true;
+}
+
+
+uint32_t Tableau::debugCountColLength(ArithVar var){
+ Debug("tableau") << var << " ";
+ uint32_t count = 0;
+ for(ColIterator i=colIterator(var); !i.atEnd(); ++i){
+ const TableauEntry& entry = *i;
+ Debug("tableau") << "(" << entry.getRowVar() << ", " << i.getID() << ") ";
+ ++count;
+ }
+ Debug("tableau") << endl;
+ return count;
+}
+
+uint32_t Tableau::debugCountRowLength(ArithVar var){
+ uint32_t count = 0;
+ for(RowIterator i=rowIterator(var); !i.atEnd(); ++i){
+ ++count;
+ }
+ return count;
+}
+
+/*
+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);
+ }
+ }
+ }*/
+
+Node Tableau::rowAsEquality(ArithVar basic, const ArithVarToNodeMap& map){
+ using namespace CVC4::kind;
+
+ Assert(getRowLength(basic) >= 2);
+
+ vector<Node> nonBasicPairs;
+ for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
+ const TableauEntry& entry = *i;
+ ArithVar colVar = entry.getColVar();
+ if(colVar == basic) continue;
+ Node var = (map.find(colVar))->second;
+ Node coeff = mkRationalNode(entry.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;
+}
+
+double Tableau::densityMeasure() const{
+ Assert(numNonZeroEntriesByRow() == numNonZeroEntries());
+ Assert(numNonZeroEntriesByCol() == numNonZeroEntries());
+
+ uint32_t n = getNumRows();
+ if(n == 0){
+ return 1.0;
+ }else {
+ uint32_t s = numNonZeroEntries();
+ uint32_t m = d_colHeads.size();
+ uint32_t divisor = (n *(m - n + 1));
+
+ Assert(n >= 1);
+ Assert(m >= n);
+ Assert(divisor > 0);
+ Assert(divisor >= s);
+
+ return (double(s)) / divisor;
+ }
+}
+
+void TableauEntryManager::freeEntry(EntryID id){
+ Assert(get(id).blank());
+ Assert(d_size > 0);
+
+ d_freedEntries.push(id);
+ --d_size;
+}
+
+EntryID TableauEntryManager::newEntry(){
+ EntryID newId;
+ if(d_freedEntries.empty()){
+ newId = d_entries.size();
+ d_entries.push_back(TableauEntry());
+ }else{
+ newId = d_freedEntries.front();
+ d_freedEntries.pop();
+ }
+ ++d_size;
+ return newId;
+}
#include "theory/arith/arithvar_set.h"
#include "theory/arith/normal_form.h"
-#include "theory/arith/row_vector.h"
-
-#include <ext/hash_map>
-#include <set>
+#include <queue>
+#include <vector>
+#include <utility>
#ifndef __CVC4__THEORY__ARITH__TABLEAU_H
#define __CVC4__THEORY__ARITH__TABLEAU_H
namespace theory {
namespace arith {
-typedef PermissiveBackArithVarSet Column;
+typedef uint32_t EntryID;
+#define ENTRYID_SENTINEL std::numeric_limits<ArithVar>::max()
+
+class TableauEntry {
+private:
+ ArithVar d_rowVar;
+ ArithVar d_colVar;
+
+ EntryID d_nextRow;
+ EntryID d_nextCol;
+
+ EntryID d_prevRow;
+ EntryID d_prevCol;
+
+ Rational d_coefficient;
+
+public:
+ TableauEntry():
+ d_rowVar(ARITHVAR_SENTINEL),
+ d_colVar(ARITHVAR_SENTINEL),
+ d_nextRow(ENTRYID_SENTINEL),
+ d_nextCol(ENTRYID_SENTINEL),
+ d_prevRow(ENTRYID_SENTINEL),
+ d_prevCol(ENTRYID_SENTINEL),
+ d_coefficient(0)
+ {}
+
+ TableauEntry(ArithVar row, ArithVar col,
+ EntryID nextRowEntry, EntryID nextColEntry,
+ EntryID prevRowEntry, EntryID prevColEntry,
+ const Rational& coeff):
+ d_rowVar(row),
+ d_colVar(col),
+ d_nextRow(nextRowEntry),
+ d_nextCol(nextColEntry),
+ d_prevRow(prevRowEntry),
+ d_prevCol(prevColEntry),
+ d_coefficient(coeff)
+ {}
+
+private:
+ bool unusedConsistent() const {
+ return
+ (d_rowVar == ARITHVAR_SENTINEL && d_colVar == ARITHVAR_SENTINEL) ||
+ (d_rowVar != ARITHVAR_SENTINEL && d_colVar != ARITHVAR_SENTINEL);
+ }
+
+public:
+
+ EntryID getNextRowID() const {
+ return d_nextRow;
+ }
+
+ EntryID getNextColID() const {
+ return d_nextCol;
+ }
+ EntryID getPrevRowID() const {
+ return d_prevRow;
+ }
+
+ EntryID getPrevColID() const {
+ return d_prevCol;
+ }
+
+ void setNextRowID(EntryID id) {
+ d_nextRow = id;
+ }
+ void setNextColID(EntryID id) {
+ d_nextCol = id;
+ }
+ void setPrevRowID(EntryID id) {
+ d_prevRow = id;
+ }
+ void setPrevColID(EntryID id) {
+ d_prevCol = id;
+ }
+
+ void setRowVar(ArithVar newRowVar){
+ d_rowVar = newRowVar;
+ }
+
+ ArithVar getRowVar() const{
+ return d_rowVar;
+ }
+ ArithVar getColVar() const{
+ return d_colVar;
+ }
+
+ const Rational& getCoefficient() const {
+ return d_coefficient;
+ }
+
+ Rational& getCoefficient(){
+ return d_coefficient;
+ }
+
+ void markBlank() {
+ d_rowVar = ARITHVAR_SENTINEL;
+ d_colVar = ARITHVAR_SENTINEL;
+ }
+
+ bool blank() const{
+ Assert(unusedConsistent());
+
+ return d_rowVar == ARITHVAR_SENTINEL;
+ }
+};
+
+class TableauEntryManager {
+private:
+ typedef std::vector<TableauEntry> EntryArray;
+
+ EntryArray d_entries;
+ std::queue<EntryID> d_freedEntries;
+
+ uint32_t d_size;
+
+public:
+ TableauEntryManager():
+ d_entries(), d_freedEntries(), d_size(0)
+ {}
+
+ const TableauEntry& get(EntryID id) const{
+ Assert(inBounds(id));
+ return d_entries[id];
+ }
+
+ TableauEntry& get(EntryID id){
+ Assert(inBounds(id));
+ return d_entries[id];
+ }
+
+ void freeEntry(EntryID id);
+
+ EntryID newEntry();
-typedef std::vector<Column> ColumnMatrix;
+ uint32_t size() const{ return d_size; }
+ uint32_t capacity() const{ return d_entries.capacity(); }
+
+
+private:
+ bool inBounds(EntryID id) const{
+ return id < d_entries.size();
+ }
+};
class Tableau {
private:
- typedef std::vector< ReducedRowVector* > RowsTable;
+ // VectorHeadTable : ArithVar |-> EntryID of the head of the vector
+ typedef std::vector<EntryID> VectorHeadTable;
+ VectorHeadTable d_rowHeads;
+ VectorHeadTable d_colHeads;
- RowsTable d_rowsTable;
+ // VectorSizeTable : ArithVar |-> length of the vector
+ typedef std::vector<uint32_t> VectorSizeTable;
+ VectorSizeTable d_colLengths;
+ VectorSizeTable d_rowLengths;
+ // Set of all of the basic variables in the tableau.
ArithVarSet d_basicVariables;
- std::vector<uint32_t> d_rowCount;
- ColumnMatrix d_columnMatrix;
+ typedef std::pair<EntryID, bool> PosUsedPair;
+ typedef std::vector<PosUsedPair> PosUsedPairArray;
+ PosUsedPairArray d_mergeBuffer;
+
+ typedef std::vector<ArithVar> ArithVarArray;
+ ArithVarArray d_usedList;
+
+
+ uint32_t d_entriesInUse;
+ TableauEntryManager d_entryManager;
public:
/**
* Constructs an empty tableau.
*/
- Tableau() :
- d_rowsTable(),
- d_basicVariables(),
- d_rowCount(),
- d_columnMatrix()
- {}
-
- /** Copy constructor. */
- Tableau(const Tableau& tab);
+ Tableau() : d_entriesInUse(0) {}
~Tableau();
- Tableau& operator=(const Tableau& tab);
+private:
+ void addEntry(ArithVar row, ArithVar col, const Rational& coeff);
+ void removeEntry(EntryID id);
+
+ template <bool isRowIterator>
+ class Iterator {
+ private:
+ EntryID d_curr;
+ TableauEntryManager& d_entryManager;
+
+ public:
+ Iterator(EntryID start, TableauEntryManager& manager) :
+ d_curr(start), d_entryManager(manager)
+ {}
+
+ public:
+
+ EntryID getID() const {
+ return d_curr;
+ }
+
+ const TableauEntry& operator*() const{
+ Assert(!atEnd());
+ return d_entryManager.get(d_curr);
+ }
+
+ Iterator& operator++(){
+ Assert(!atEnd());
+ TableauEntry& entry = d_entryManager.get(d_curr);
+ d_curr = isRowIterator ? entry.getNextRowID() : entry.getNextColID();
+ return *this;
+ }
+
+ bool atEnd() const {
+ return d_curr == ENTRYID_SENTINEL;
+ }
+ };
+
+public:
+ typedef Iterator<true> RowIterator;
+ typedef Iterator<false> ColIterator;
+
+ double densityMeasure() const;
size_t getNumRows() const {
return d_basicVariables.size();
void increaseSize(){
d_basicVariables.increaseSize();
- d_rowsTable.push_back(NULL);
- d_rowCount.push_back(0);
- d_columnMatrix.push_back(PermissiveBackArithVarSet());
+ d_rowHeads.push_back(ENTRYID_SENTINEL);
+ d_colHeads.push_back(ENTRYID_SENTINEL);
+
+ d_colLengths.push_back(0);
+ d_rowLengths.push_back(0);
- //TODO replace with version of ArithVarSet that handles misses as non-entries
- // not as buffer overflows
- // ColumnMatrix::iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end();
- // for(; i != end; ++i){
- // Column& col = *i;
- // col.increaseSize(d_columnMatrix.size());
- // }
+ d_mergeBuffer.push_back(std::make_pair(ENTRYID_SENTINEL, false));
}
bool isBasic(ArithVar v) const {
return d_basicVariables.isMember(v);
}
- ArithVarSet::iterator begin(){
+ ArithVarSet::const_iterator beginBasic() const{
return d_basicVariables.begin();
}
- ArithVarSet::iterator end(){
+ ArithVarSet::const_iterator endBasic() const{
return d_basicVariables.end();
}
- const Column& getColumn(ArithVar v){
- Assert(v < d_columnMatrix.size());
- return d_columnMatrix[v];
+ RowIterator rowIterator(ArithVar v){
+ Assert(v < d_rowHeads.size());
+ EntryID head = d_rowHeads[v];
+ return RowIterator(head, d_entryManager);
}
- Column::iterator beginColumn(ArithVar v){
- return getColumn(v).begin();
- }
- Column::iterator endColumn(ArithVar v){
- return getColumn(v).end();
+ ColIterator colIterator(ArithVar v){
+ Assert(v < d_colHeads.size());
+ EntryID head = d_colHeads[v];
+ return ColIterator(head, d_entryManager);
}
- ReducedRowVector& lookup(ArithVar var){
- Assert(d_basicVariables.isMember(var));
- Assert(d_rowsTable[var] != NULL);
- return *(d_rowsTable[var]);
+ uint32_t getRowLength(ArithVar x) const{
+ Assert(x < d_rowLengths.size());
+ return d_rowLengths[x];
}
- uint32_t getRowCount(ArithVar x){
- Assert(x < d_rowCount.size());
- AlwaysAssert(d_rowCount[x] == getColumn(x).size());
-
- return d_rowCount[x];
+ uint32_t getColLength(ArithVar x) const{
+ Assert(x < d_colLengths.size());
+ return d_colLengths[x];
}
/**
* x_s is non-basic, and
* a_rs != 0.
*/
- void pivot(ArithVar x_r, ArithVar x_s);
+ void pivot(ArithVar basicOld, ArithVar basicNew);
+private:
+ void rowPivot(ArithVar basicOld, ArithVar basicNew);
+ /** Requires merge buffer to be loaded with basicFrom and used to be empty. */
+ void rowPlusRowTimesConstant(ArithVar basicTo, const Rational& coeff, ArithVar basicFrom);
- void printTableau();
+ EntryID findOnRow(ArithVar basic, ArithVar find);
+ EntryID findOnCol(ArithVar basic, ArithVar find);
- ReducedRowVector* removeRow(ArithVar basic);
+ TableauEntry d_failedFind;
+public:
+ /** If the find fails, isUnused is true on the entry. */
+ const TableauEntry& findEntry(ArithVar row, ArithVar col);
/**
- * Let s = numNonZeroEntries(), n = getNumRows(), and m = d_columnMatrix.size().
- * When n >= 1,
- * densityMeasure() := s / (n*m - n**2 + n)
- * := s / (n *(m - n + 1))
- * When n = 0, densityMeasure() := 1
+ * Prints the contents of the Tableau to Debug("tableau::print")
*/
- double densityMeasure() const{
- Assert(numNonZeroEntriesByRow() == numNonZeroEntries());
- uint32_t n = getNumRows();
- if(n == 0){
- return 1.0;
- }else {
- uint32_t s = numNonZeroEntries();
- uint32_t m = d_columnMatrix.size();
- uint32_t divisor = (n *(m - n + 1));
-
- Assert(n >= 1);
- Assert(m >= n);
- Assert(divisor > 0);
- Assert(divisor >= s);
-
- return (double(s)) / divisor;
- }
- }
+ void printTableau();
+ void printRow(ArithVar basic);
+ void printEntry(const TableauEntry& entry);
+
private:
+ void loadRowIntoMergeBuffer(ArithVar basic);
+ void emptyRowFromMergeBuffer(ArithVar basic);
+ void clearUsedList();
- uint32_t numNonZeroEntries() const;
+ static bool bufferPairIsNotEmpty(const PosUsedPair& p){
+ return !(p.first == ENTRYID_SENTINEL && p.second == false);
+ }
+
+ static bool bufferPairIsEmpty(const PosUsedPair& p){
+ return (p.first == ENTRYID_SENTINEL && p.second == false);
+ }
+ bool mergeBufferIsEmpty() const {
+ return d_mergeBuffer.end() == std::find_if(d_mergeBuffer.begin(),
+ d_mergeBuffer.end(),
+ bufferPairIsNotEmpty);
+ }
+
+ void setColumnUnused(ArithVar v);
+
+public:
+ uint32_t size() const {
+ return d_entriesInUse;
+ }
+ uint32_t getNumEntriesInTableau() const {
+ return d_entryManager.size();
+ }
+ uint32_t getEntryCapacity() const {
+ return d_entryManager.capacity();
+ }
+
+ void removeRow(ArithVar basic);
+ Node rowAsEquality(ArithVar basic, const ArithVarToNodeMap& map);
+private:
+ uint32_t numNonZeroEntries() const { return size(); }
uint32_t numNonZeroEntriesByRow() const;
+ uint32_t numNonZeroEntriesByCol() const;
+
- /** Copies the datastructures in tab to this.*/
- void internalCopy(const Tableau& tab);
+ bool debugNoZeroCoefficients(ArithVar basic);
+ bool debugMatchingCountsForRow(ArithVar basic);
+ uint32_t debugCountColLength(ArithVar var);
+ uint32_t debugCountRowLength(ArithVar var);
- /** Clears the structures in the tableau. */
- void clear();
};
}; /* namespace arith */
#include "theory/arith/theory_arith.h"
#include "theory/arith/normal_form.h"
-#include <map>
#include <stdint.h>
using namespace std;
using namespace CVC4::theory;
using namespace CVC4::theory::arith;
+static const uint32_t RESET_START = 2;
+
struct SlackAttrID;
typedef expr::Attribute<SlackAttrID, Node> Slack;
d_diseq(c),
d_tableau(),
d_restartsCounter(0),
- d_initialDensity(1.0),
- d_tableauResetDensity(2.0),
+ d_presolveHasBeenCalled(false),
+ d_tableauResetDensity(1.6),
d_tableauResetPeriod(10),
d_propagator(c, out),
d_simplex(d_partialModel, d_tableau),
d_staticLearningTimer("theory::arith::staticLearningTimer"),
d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
d_presolveTime("theory::arith::presolveTime"),
- d_initialTableauDensity("theory::arith::initialTableauDensity", 0.0),
- d_avgTableauDensityAtRestart("theory::arith::avgTableauDensityAtRestarts"),
- d_tableauResets("theory::arith::tableauResets", 0),
+ d_initialTableauSize("theory::arith::initialTableauSize", 0),
+ //d_tableauSizeHistory("theory::arith::tableauSizeHistory"),
+ d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
+ d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0),
d_restartTimer("theory::arith::restartTimer")
{
StatisticsRegistry::registerStat(&d_statUserVariables);
StatisticsRegistry::registerStat(&d_presolveTime);
- StatisticsRegistry::registerStat(&d_initialTableauDensity);
- StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart);
- StatisticsRegistry::registerStat(&d_tableauResets);
+ StatisticsRegistry::registerStat(&d_initialTableauSize);
+ //StatisticsRegistry::registerStat(&d_tableauSizeHistory);
+ StatisticsRegistry::registerStat(&d_currSetToSmaller);
+ StatisticsRegistry::registerStat(&d_smallerSetToCurr);
StatisticsRegistry::registerStat(&d_restartTimer);
}
StatisticsRegistry::unregisterStat(&d_presolveTime);
- StatisticsRegistry::unregisterStat(&d_initialTableauDensity);
- StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart);
- StatisticsRegistry::unregisterStat(&d_tableauResets);
+ StatisticsRegistry::unregisterStat(&d_initialTableauSize);
+ //StatisticsRegistry::unregisterStat(&d_tableauSizeHistory);
+ StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
+ StatisticsRegistry::unregisterStat(&d_smallerSetToCurr);
StatisticsRegistry::unregisterStat(&d_restartTimer);
}
ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){
ArithVar bestBasic = ARITHVAR_SENTINEL;
- uint64_t rowLength = std::numeric_limits<uint64_t>::max();
-
- Column::iterator basicIter = d_tableau.beginColumn(variable);
- Column::iterator end = d_tableau.endColumn(variable);
- for(; basicIter != end; ++basicIter){
- ArithVar x_j = *basicIter;
- ReducedRowVector& row_j = d_tableau.lookup(x_j);
-
- Assert(row_j.has(variable));
- if((row_j.size() < rowLength) ||
- (row_j.size() == rowLength && x_j < bestBasic)){
- bestBasic = x_j;
- rowLength = row_j.size();
+ uint64_t bestRowLength = std::numeric_limits<uint64_t>::max();
+
+ Tableau::ColIterator basicIter = d_tableau.colIterator(variable);
+ for(; !basicIter.atEnd(); ++basicIter){
+ const TableauEntry& entry = *basicIter;
+ Assert(entry.getColVar() == variable);
+ ArithVar basic = entry.getRowVar();
+ uint32_t rowLength = d_tableau.getRowLength(basic);
+ if((rowLength < bestRowLength) ||
+ (rowLength == bestRowLength && basic < bestBasic)){
+ bestBasic = basic;
+ bestRowLength = rowLength;
}
}
+ Assert(bestBasic == ARITHVAR_SENTINEL || bestRowLength < std::numeric_limits<uint32_t>::max());
return bestBasic;
}
}
}
- if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+ if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
if(Debug.isOn("arith::print_model")) { debugPrintModel(); }
Debug("arith") << "TheoryArith::check end" << std::endl;
}
}
void TheoryArith::notifyEq(TNode lhs, TNode rhs) {
-
}
void TheoryArith::notifyRestart(){
TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer);
- if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+ if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
++d_restartsCounter;
+ /*
if(d_restartsCounter % d_tableauResetPeriod == 0){
double currentDensity = d_tableau.densityMeasure();
d_statistics.d_avgTableauDensityAtRestart.addEntry(currentDensity);
d_tableau = d_initialTableau;
}
}
+ */
+ static const bool debugResetPolicy = false;
+
+ uint32_t currSize = d_tableau.size();
+ uint32_t copySize = d_smallTableauCopy.size();
+
+ //d_statistics.d_tableauSizeHistory << currSize;
+ if(debugResetPolicy){
+ cout << "curr " << currSize << " copy " << copySize << endl;
+ }
+ if(d_presolveHasBeenCalled && copySize == 0 && currSize > 0){
+ if(debugResetPolicy){
+ cout << "initial copy " << d_restartsCounter << endl;
+ }
+ d_smallTableauCopy = d_tableau; // The initial copy
+ }
+
+ if(d_presolveHasBeenCalled && d_restartsCounter >= RESET_START){
+ if(copySize >= currSize * 1.1 ){
+ ++d_statistics.d_smallerSetToCurr;
+ d_smallTableauCopy = d_tableau;
+ }else if(d_tableauResetDensity * copySize <= currSize){
+ ++d_statistics.d_currSetToSmaller;
+ d_tableau = d_smallTableauCopy;
+ }
+ }
}
bool TheoryArith::entireStateIsConsistent(){
Assert(!noRow);
//remove the row from the tableau
- ReducedRowVector* row = d_tableau.removeRow(v);
- Node eq = row->asEquality(d_arithVarToNodeMap);
+ Node eq = d_tableau.rowAsEquality(v, d_arithVarToNodeMap);
+ d_tableau.removeRow(v);
- if(Debug.isOn("row::print")) row->printRow();
if(Debug.isOn("tableau")) d_tableau.printTableau();
Debug("arith::permanentlyRemoveVariable") << eq << endl;
- delete row;
- Assert(d_tableau.getRowCount(v) == 0);
+ Assert(d_tableau.getRowLength(v) == 0);
+ Assert(d_tableau.getColLength(v) == 0);
Assert(d_removedRows.find(v) == d_removedRows.end());
d_removedRows[v] = eq;
}
}
}
- d_initialTableau = d_tableau;
- d_initialDensity = d_initialTableau.densityMeasure();
- d_statistics.d_initialTableauDensity.setData(d_initialDensity);
+ d_statistics.d_initialTableauSize.setData(d_tableau.size());
- if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+ if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
static int callCount = 0;
Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
learner.clear();
+ d_presolveHasBeenCalled = true;
check(FULL_EFFORT);
}
*/
Tableau d_tableau;
- /**
- * A copy of the tableau immediately after removing variables
- * without bounds in presolve().
- */
- Tableau d_initialTableau;
/** Counts the number of notifyRestart() calls to the theory. */
uint32_t d_restartsCounter;
* If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau
* is set to d_initialTableau.
*/
- double d_initialDensity;
+ bool d_presolveHasBeenCalled;
double d_tableauResetDensity;
uint32_t d_tableauResetPeriod;
static const uint32_t s_TABLEAU_RESET_INCREMENT = 5;
+ /**
+ * A copy of the tableau immediately after removing variables
+ * without bounds in presolve().
+ */
+ Tableau d_smallTableauCopy;
ArithUnatePropagator d_propagator;
SimplexDecisionProcedure d_simplex;
IntStat d_permanentlyRemovedVariables;
TimerStat d_presolveTime;
- BackedStat<double> d_initialTableauDensity;
- AverageStat d_avgTableauDensityAtRestart;
- IntStat d_tableauResets;
+ IntStat d_initialTableauSize;
+ //ListStat<uint32_t> d_tableauSizeHistory;
+ IntStat d_currSetToSmaller;
+ IntStat d_smallerSetToCurr;
TimerStat d_restartTimer;
Statistics();
#include <iomanip>
#include <set>
#include <ctime>
+#include <vector>
#include "util/Assert.h"
#include "lib/clock_gettime.h"
};/* class AverageStat */
+template <class T>
+class ListStat : public Stat{
+private:
+ typedef std::vector<T> List;
+ List d_list;
+public:
+
+ /**
+ * Construct an integer-valued statistic with the given name and
+ * initial value.
+ */
+ ListStat(const std::string& name) : Stat(name) {}
+ ~ListStat() {}
+
+ void flushInformation(std::ostream& out) const{
+ if(__CVC4_USE_STATISTICS) {
+ typename List::const_iterator i = d_list.begin(), end = d_list.end();
+ out << "[";
+ if(i != end){
+ out << *i;
+ ++i;
+ for(; i != end; ++i){
+ out << ", " << *i;
+ }
+ }
+ out << "]";
+ }
+ }
+
+ ListStat& operator<<(const T& val){
+ if(__CVC4_USE_STATISTICS) {
+ d_list.push_back(val);
+ }
+ return (*this);
+ }
+
+ std::string getValue() const {
+ std::stringstream ss;
+ flushInformation(ss);
+ return ss.str();
+ }
+
+};/* class ListStat */
/****************************************************************************/
/* Some utility functions for ::timespec */
projects / cvc5.git / commitdiff