using namespace std;
-bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) {
+bool ReducedRowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) {
if(arr.size() >= 2){
- NonZeroIterator curr = arr.begin();
- NonZeroIterator end = arr.end();
+ const_iterator curr = arr.begin();
+ const_iterator end = arr.end();
ArithVar prev = getArithVar(*curr);
++curr;
for(;curr != end; ++curr){
return true;
}
-RowVector::~RowVector(){
- NonZeroIterator curr = beginNonZero();
- NonZeroIterator end = endNonZero();
- for(;curr != end; ++curr){
+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 = getArithVar(*curr);
Assert(d_rowCount[v] >= 1);
+ d_columnMatrix[v].remove(basic());
--(d_rowCount[v]);
}
Assert(matchingCounts());
}
-bool RowVector::matchingCounts() const{
- for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){
+
+bool ReducedRowVector::matchingCounts() const{
+ for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
ArithVar v = getArithVar(*i);
if(d_columnMatrix[v].size() != d_rowCount[v]){
return false;
return true;
}
-bool RowVector::noZeroCoefficients(const VarCoeffArray& arr){
- for(NonZeroIterator curr = arr.begin(), end = arr.end();
- curr != end; ++curr){
+bool ReducedRowVector::noZeroCoefficients(const VarCoeffArray& arr){
+ for(const_iterator curr = arr.begin(), endEntries = arr.end();
+ curr != endEntries; ++curr){
const Rational& coeff = getCoefficient(*curr);
if(coeff == 0) return false;
}
return true;
}
-void RowVector::zip(const std::vector< ArithVar >& variables,
- const std::vector< Rational >& coefficients,
- VarCoeffArray& output){
+void ReducedRowVector::zip(const std::vector< ArithVar >& variables,
+ const std::vector< Rational >& coefficients,
+ VarCoeffArray& output){
Assert(coefficients.size() == variables.size() );
}
}
-
-RowVector::RowVector(const std::vector< ArithVar >& variables,
- const std::vector< Rational >& coefficients,
- std::vector<uint32_t>& counts,
- std::vector<ArithVarSet>& cm):
- d_rowCount(counts), d_columnMatrix(cm)
-{
- zip(variables, coefficients, d_entries);
-
- std::sort(d_entries.begin(), d_entries.end(), cmp);
-
- for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){
- ++d_rowCount[getArithVar(*i)];
- addArithVar(d_contains, getArithVar(*i));
- }
-
- Assert(isSorted(d_entries, true));
- Assert(noZeroCoefficients(d_entries));
-}
-
-void RowVector::addArithVar(ArithVarContainsSet& contains, ArithVar v){
+void ReducedRowVector::addArithVar(ArithVarContainsSet& contains, ArithVar v){
if(v >= contains.size()){
contains.resize(v+1, false);
}
contains[v] = true;
}
-void RowVector::removeArithVar(ArithVarContainsSet& contains, ArithVar v){
+void ReducedRowVector::removeArithVar(ArithVarContainsSet& contains, ArithVar v){
Assert(v < contains.size());
Assert(contains[v]);
contains[v] = false;
}
-void RowVector::merge(VarCoeffArray& arr,
- ArithVarContainsSet& contains,
- const VarCoeffArray& other,
- const Rational& c,
- std::vector<uint32_t>& counts,
- std::vector<ArithVarSet>& columnMatrix,
- ArithVar basic){
- VarCoeffArray copy = arr;
- arr.clear();
+void ReducedRowVector::merge(const VarCoeffArray& other,
+ const Rational& c){
+ VarCoeffArray copy = d_entries;
+ d_entries.clear();
iterator curr1 = copy.begin();
iterator end1 = copy.end();
- NonZeroIterator curr2 = other.begin();
- NonZeroIterator end2 = other.end();
+ const_iterator curr2 = other.begin();
+ const_iterator end2 = other.end();
while(curr1 != end1 && curr2 != end2){
if(getArithVar(*curr1) < getArithVar(*curr2)){
- arr.push_back(*curr1);
+ d_entries.push_back(*curr1);
++curr1;
}else if(getArithVar(*curr1) > getArithVar(*curr2)){
- ++counts[getArithVar(*curr2)];
- if(basic != ARITHVAR_SENTINEL){
- columnMatrix[getArithVar(*curr2)].add(basic);
+ ++d_rowCount[getArithVar(*curr2)];
+ if(d_basic != ARITHVAR_SENTINEL){
+ d_columnMatrix[getArithVar(*curr2)].add(d_basic);
}
- addArithVar(contains, getArithVar(*curr2));
- arr.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
+ addArithVar(d_contains, getArithVar(*curr2));
+ d_entries.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
++curr2;
}else{
Rational res = getCoefficient(*curr1) + c * getCoefficient(*curr2);
if(res != 0){
//The variable is not new so the count stays the same
- arr.push_back(make_pair(getArithVar(*curr1), res));
+ d_entries.push_back(make_pair(getArithVar(*curr1), res));
}else{
- removeArithVar(contains, getArithVar(*curr2));
+ removeArithVar(d_contains, getArithVar(*curr2));
- --counts[getArithVar(*curr2)];
- if(basic != ARITHVAR_SENTINEL){
- columnMatrix[getArithVar(*curr2)].remove(basic);
+ --d_rowCount[getArithVar(*curr2)];
+ if(d_basic != ARITHVAR_SENTINEL){
+ d_columnMatrix[getArithVar(*curr2)].remove(d_basic);
}
}
++curr1;
}
}
while(curr1 != end1){
- arr.push_back(*curr1);
+ d_entries.push_back(*curr1);
++curr1;
}
while(curr2 != end2){
- ++counts[getArithVar(*curr2)];
- if(basic != ARITHVAR_SENTINEL){
- columnMatrix[getArithVar(*curr2)].add(basic);
+ ++d_rowCount[getArithVar(*curr2)];
+ if(d_basic != ARITHVAR_SENTINEL){
+ d_columnMatrix[getArithVar(*curr2)].add(d_basic);
}
- addArithVar(contains, getArithVar(*curr2));
+ addArithVar(d_contains, getArithVar(*curr2));
- arr.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
+ d_entries.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
++curr2;
}
}
-void RowVector::multiply(const Rational& c){
+void ReducedRowVector::multiply(const Rational& c){
Assert(c != 0);
for(iterator i = d_entries.begin(), end = d_entries.end(); i != end; ++i){
}
}
-void RowVector::addRowTimesConstant(const Rational& c, const RowVector& other, ArithVar basic){
+void ReducedRowVector::addRowTimesConstant(const Rational& c, const ReducedRowVector& other){
Assert(c != 0);
- merge(d_entries, d_contains, other.d_entries, c, d_rowCount, d_columnMatrix, basic);
+ merge(other.d_entries, c);
}
-void RowVector::printRow(){
- for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){
+void ReducedRowVector::printRow(){
+ for(const_iterator i = begin(); i != end(); ++i){
ArithVar nb = getArithVar(*i);
Debug("row::print") << "{" << nb << "," << getCoefficient(*i) << "}";
}
ReducedRowVector::ReducedRowVector(ArithVar basic,
const std::vector<ArithVar>& variables,
const std::vector<Rational>& coefficients,
- std::vector<uint32_t>& count,
- std::vector<ArithVarSet>& columnMatrix):
- RowVector(variables, coefficients, count, columnMatrix), d_basic(basic){
+ std::vector<uint32_t>& counts,
+ std::vector<ArithVarSet>& cm):
+ d_basic(basic), d_rowCount(counts), d_columnMatrix(cm)
+{
+ zip(variables, coefficients, d_entries);
+ d_entries.push_back(make_pair(basic, Rational(-1)));
+ std::sort(d_entries.begin(), d_entries.end(), cmp);
- for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){
- //basic is not yet in d_entries
- Assert(getArithVar(*i) != d_basic);
+ for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
+ ++d_rowCount[getArithVar(*i)];
+ addArithVar(d_contains, getArithVar(*i));
d_columnMatrix[getArithVar(*i)].add(d_basic);
}
- VarCoeffArray justBasic;
- justBasic.push_back(make_pair(basic, Rational(-1)));
-
- merge(d_entries, d_contains, justBasic, Rational(1), d_rowCount, d_columnMatrix, d_basic);
+ Assert(isSorted(d_entries, true));
+ Assert(noZeroCoefficients(d_entries));
Assert(matchingCounts());
Assert(wellFormed());
Rational a_rs = lookup(x_s);
Assert(a_rs != 0);
- addRowTimesConstant(a_rs, row_s, basic());
+ addRowTimesConstant(a_rs, row_s);
Assert(!has(x_s));
Rational negInverseA_rs = -(lookup(x_j).inverse());
multiply(negInverseA_rs);
- for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){
+ for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
d_columnMatrix[getArithVar(*i)].remove(d_basic);
d_columnMatrix[getArithVar(*i)].add(x_j);
}
if(size() > 2){
NodeBuilder<> sumBuilder(PLUS);
- for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){
+ for(const_iterator i = begin(); i != end(); ++i){
ArithVar nb = getArithVar(*i);
if(nb == basic()) continue;
Node var = (map.find(nb))->second;
sum = sumBuilder;
}else{
Assert(size() == 2);
- NonZeroIterator i = beginNonZero();
+ const_iterator i = begin();
if(getArithVar(*i) == basic()){
++i;
}
return NodeBuilder<2>(EQUAL) << basicVar << sum;
}
-
-ReducedRowVector::~ReducedRowVector(){
- //This executes before the super classes destructor RowVector,
- // which will set this to 0.
- Assert(d_rowCount[basic()] == 1);
-
- NonZeroIterator curr = beginNonZero();
- NonZeroIterator end = endNonZero();
- for(;curr != end; ++curr){
- ArithVar v = getArithVar(*curr);
- Assert(d_rowCount[v] >= 1);
- d_columnMatrix[v].remove(basic());
- }
-}
namespace arith {
typedef std::pair<ArithVar, Rational> VarCoeffPair;
+
inline ArithVar getArithVar(const VarCoeffPair& v) { return v.first; }
inline Rational& getCoefficient(VarCoeffPair& v) { return v.second; }
inline const Rational& getCoefficient(const VarCoeffPair& v) { return v.second; }
inline bool cmp(const VarCoeffPair& a, const VarCoeffPair& b){
- return CVC4::theory::arith::getArithVar(a) < CVC4::theory::arith::getArithVar(b);
+ return getArithVar(a) < getArithVar(b);
}
/**
- * RowVector is a sparse vector representation that represents the
+ * 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 RowVector {
+class ReducedRowVector {
public:
typedef std::vector<VarCoeffPair> VarCoeffArray;
- typedef VarCoeffArray::const_iterator NonZeroIterator;
+ typedef VarCoeffArray::const_iterator const_iterator;
typedef std::vector<bool> ArithVarContainsSet;
- /**
- * 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);
-
- static void merge(VarCoeffArray& arr,
- ArithVarContainsSet& contains,
- const VarCoeffArray& other,
- const Rational& c,
- std::vector<uint32_t>& count,
- std::vector<ArithVarSet>& columnMatrix,
- ArithVar basic);
-
-protected:
- /**
- * 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;
+private:
+ typedef VarCoeffArray::iterator iterator;
/**
* Invariants:
*/
VarCoeffArray d_entries;
+ /**
+ * 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.
std::vector<uint32_t>& d_rowCount;
std::vector<ArithVarSet>& d_columnMatrix;
- NonZeroIterator lower_bound(ArithVar x_j) const{
- return std::lower_bound(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
- }
-
- typedef VarCoeffArray::iterator iterator;
public:
- RowVector(const std::vector< ArithVar >& variables,
- const std::vector< Rational >& coefficients,
- std::vector<uint32_t>& counts,
- std::vector<ArithVarSet>& columnMatrix);
+ ReducedRowVector(ArithVar basic,
+ const std::vector< ArithVar >& variables,
+ const std::vector< Rational >& coefficients,
+ std::vector<uint32_t>& count,
+ std::vector<ArithVarSet>& columnMatrix);
- ~RowVector();
+ ~ReducedRowVector();
+
+ ArithVar basic() const{
+ Assert(basicIsSet());
+ return d_basic;
+ }
/** Returns the number of nonzero variables in the vector. */
uint32_t size() const {
}
//Iterates over the nonzero entries in the Vector
- NonZeroIterator beginNonZero() const { return d_entries.begin(); }
- NonZeroIterator endNonZero() const { return d_entries.end(); }
+ 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{
}
}
-private:
- /** Debugging code. */
- bool hasInEntries(ArithVar x_j) const {
- return std::binary_search(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
- }
-public:
-
/**
* Returns the coefficient of a variable in the row.
*/
const Rational& lookup(ArithVar x_j) const{
Assert(has(x_j));
Assert(hasInEntries(x_j));
- NonZeroIterator lb = lower_bound(x_j);
+ const_iterator lb = lower_bound(x_j);
return getCoefficient(*lb);
}
* Updates the current row to be the sum of itself and
* another vector times c (c != 0).
*/
- void addRowTimesConstant(const Rational& c, const RowVector& other, ArithVar basic);
+ void addRowTimesConstant(const Rational& c, const ReducedRowVector& other);
void printRow();
-protected:
+
+ void pivot(ArithVar x_j);
+
+ 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:
/**
* Adds v to d_contains.
* This may resize d_contains.
/** Removes v from d_contains. */
static void removeArithVar(ArithVarContainsSet& contains, ArithVar v);
-}; /* class RowVector */
-/**
- * A reduced row is similar to a normal row except
- * that it also has a notion of a basic variable.
- * This variable that must have a coefficient of -1 in the array.
- */
-class ReducedRowVector : public RowVector{
-private:
- ArithVar d_basic;
+ /**
+ * 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);
+
+ void merge(const VarCoeffArray& other, const Rational& c);
+
+ /**
+ * 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(), std::make_pair(x_j,0), cmp);
+ }
+
+ /** Debugging code */
bool wellFormed() const{
return
isSorted(d_entries, true) &&
lookup(basic()) == Rational(-1);
}
-public:
-
bool basicIsSet() const { return d_basic != ARITHVAR_SENTINEL; }
- ReducedRowVector(ArithVar basic,
- const std::vector< ArithVar >& variables,
- const std::vector< Rational >& coefficients,
- std::vector<uint32_t>& count,
- std::vector<ArithVarSet>& columnMatrix);
-
- ~ReducedRowVector();
-
- ArithVar basic() const{
- Assert(basicIsSet());
- return d_basic;
- }
-
- /** Return true if x is in the row and is not the basic variable. */
- bool hasNonBasic(ArithVar x) const {
- if(x == basic()){
- return false;
- }else{
- return has(x);
- }
+ /** Debugging code. */
+ bool hasInEntries(ArithVar x_j) const {
+ return std::binary_search(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
}
- void pivot(ArithVar x_j);
-
- 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;
}; /* class ReducedRowVector */
if(Debug.isOn("arith::pivotAndUpdate")){
Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl;
ReducedRowVector& row_k = d_tableau.lookup(x_i);
- for(ReducedRowVector::NonZeroIterator varIter = row_k.beginNonZero();
- varIter != row_k.endNonZero();
+ for(ReducedRowVector::const_iterator varIter = row_k.begin();
+ varIter != row_k.end();
++varIter){
ArithVar var = varIter->first;
bool pivotStage = !first;
- for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
+ for(ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
nbi != end; ++nbi){
ArithVar nonbasic = getArithVar(*nbi);
if(nonbasic == x_i) continue;
Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
Debug("arith") << "updateInconsistentVars" << endl;
- static const uint32_t CHECK_PERIOD = 1000;
+ static const uint32_t CHECK_PERIOD = 100;
while(!limitIterations || remainingIterations > 0){
if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
return earlyConflict;
}
//Once every CHECK_PERIOD examine the entire queue for conflicts
- // if(!limitIterations && remainingIterations % CHECK_PERIOD == 0){
- // Node earlyConflict = findConflictOnTheQueue(DuringVarOrderSearch);
- // if(!earlyConflict.isNull()){
- // return earlyConflict;
- // }
- // }
+ if(!limitIterations && remainingIterations % CHECK_PERIOD == 0){
+ Node earlyConflict = findConflictOnTheQueue(DuringVarOrderSearch);
+ if(!earlyConflict.isNull()){
+ return earlyConflict;
+ }
+ }
}
AlwaysAssert(limitIterations && remainingIterations == 0);
nb << bound;
- typedef ReducedRowVector::NonZeroIterator RowIterator;
- RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
+ ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
for(; nbi != end; ++nbi){
ArithVar nonbasic = getArithVar(*nbi);
<< " " << bound << endl;
nb << bound;
- typedef ReducedRowVector::NonZeroIterator RowIterator;
- RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
+
+ ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
for(; nbi != end; ++nbi){
ArithVar nonbasic = getArithVar(*nbi);
if(nonbasic == conflictVar) continue;
DeltaRational sum = d_constants.d_ZERO_DELTA;
ReducedRowVector& row = d_tableau.lookup(x);
- for(ReducedRowVector::NonZeroIterator i = row.beginNonZero(), end = row.endNonZero();
+ for(ReducedRowVector::const_iterator i = row.begin(), end = row.end();
i != end;++i){
ArithVar nonbasic = getArithVar(*i);
if(nonbasic == row.basic()) continue;
ReducedRowVector& row_k = d_tableau.lookup(basic);
DeltaRational sum;
Debug("paranoid:check_tableau") << "starting row" << basic << endl;
- for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k.beginNonZero();
- nonbasicIter != row_k.endNonZero();
+ for(ReducedRowVector::const_iterator nonbasicIter = row_k.begin();
+ nonbasicIter != row_k.end();
++nonbasicIter){
ArithVar nonbasic = nonbasicIter->first;
if(basic == nonbasic) continue;
projects / cvc5.git / commitdiff