summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arith/row_vector.cpp56
-rw-r--r--src/theory/arith/row_vector.h37
-rw-r--r--src/theory/arith/simplex.cpp56
-rw-r--r--src/theory/arith/simplex.h3
-rw-r--r--src/theory/arith/tableau.cpp2
-rw-r--r--src/theory/arith/tableau.h8
6 files changed, 120 insertions, 42 deletions
diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp
index 6835fc435..f3b979bfd 100644
--- a/src/theory/arith/row_vector.cpp
+++ b/src/theory/arith/row_vector.cpp
@@ -5,6 +5,31 @@ using namespace CVC4;
using namespace CVC4::theory;
using namespace CVC4::theory::arith ;
+bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) {
+ if(arr.size() >= 2){
+ NonZeroIterator curr = arr.begin();
+ NonZeroIterator end = arr.end();
+ ArithVar prev = getArithVar(*curr);
+ ++curr;
+ for(;curr != end; ++curr){
+ ArithVar v = getArithVar(*curr);
+ if(strictlySorted && prev > v) return false;
+ if(!strictlySorted && prev >= v) return false;
+ prev = v;
+ }
+ }
+ return true;
+}
+
+bool RowVector::noZeroCoefficients(const VarCoeffArray& arr){
+ for(NonZeroIterator curr = arr.begin(), end = arr.end();
+ curr != end; ++curr){
+ const Rational& coeff = getCoefficient(*curr);
+ if(coeff == 0) return false;
+ }
+ return true;
+}
+
void RowVector::zip(const vector< ArithVar >& variables,
const vector< Rational >& coefficients,
VarCoeffArray& output){
@@ -24,16 +49,26 @@ void RowVector::zip(const vector< ArithVar >& variables,
}
RowVector::RowVector(const vector< ArithVar >& variables,
- const vector< Rational >& coefficients){
+ const vector< Rational >& coefficients,
+ std::vector<uint32_t>& counts):
+ d_rowCount(counts)
+{
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)];
+ }
+
Assert(isSorted(d_entries, true));
Assert(noZeroCoefficients(d_entries));
}
-void RowVector::merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c){
+void RowVector::merge(VarCoeffArray& arr,
+ const VarCoeffArray& other,
+ const Rational& c,
+ std::vector<uint32_t>& counts){
VarCoeffArray copy = arr;
arr.clear();
@@ -48,12 +83,18 @@ void RowVector::merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rati
arr.push_back(*curr1);
++curr1;
}else if(getArithVar(*curr1) > getArithVar(*curr2)){
+ ++counts[getArithVar(*curr2)];
+
arr.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
++curr2;
}else{
Rational res = getCoefficient(*curr1) + c * getCoefficient(*curr2);
if(res != 0){
+ ++counts[getArithVar(*curr2)];
+
arr.push_back(make_pair(getArithVar(*curr1), res));
+ }else{
+ --counts[getArithVar(*curr2)];
}
++curr1;
++curr2;
@@ -64,6 +105,8 @@ void RowVector::merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rati
++curr1;
}
while(curr2 != end2){
+ ++counts[getArithVar(*curr2)];
+
arr.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
++curr2;
}
@@ -80,7 +123,7 @@ void RowVector::multiply(const Rational& c){
void RowVector::addRowTimesConstant(const Rational& c, const RowVector& other){
Assert(c != 0);
- merge(d_entries, other.d_entries, c);
+ merge(d_entries, other.d_entries, c, d_rowCount);
}
void RowVector::printRow(){
@@ -93,14 +136,15 @@ void RowVector::printRow(){
ReducedRowVector::ReducedRowVector(ArithVar basic,
const vector<ArithVar>& variables,
- const vector<Rational>& coefficients):
- RowVector(variables, coefficients), d_basic(basic){
+ const vector<Rational>& coefficients,
+ std::vector<uint32_t>& count):
+ RowVector(variables, coefficients, count), d_basic(basic){
VarCoeffArray justBasic;
justBasic.push_back(make_pair(basic, Rational(-1)));
- merge(d_entries,justBasic, Rational(1));
+ merge(d_entries,justBasic, Rational(1), d_rowCount);
Assert(wellFormed());
}
diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index d68f8bc30..efb64d1c7 100644
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -36,34 +36,13 @@ public:
* 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) {
- if(arr.size() >= 2){
- NonZeroIterator curr = arr.begin();
- NonZeroIterator end = arr.end();
- ArithVar prev = getArithVar(*curr);
- ++curr;
- for(;curr != end; ++curr){
- ArithVar v = getArithVar(*curr);
- if(strictlySorted && prev > v) return false;
- if(!strictlySorted && prev >= v) return false;
- prev = v;
- }
- }
- return true;
- }
+ static bool isSorted(const VarCoeffArray& arr, bool strictlySorted);
/**
* noZeroCoefficients(arr) is equivalent to
* 0 != getCoefficient(arr[i]) for all i.
*/
- static bool noZeroCoefficients(const VarCoeffArray& arr){
- for(NonZeroIterator curr = arr.begin(), end = arr.end();
- curr != end; ++curr){
- const Rational& coeff = getCoefficient(*curr);
- if(coeff == 0) return false;
- }
- return true;
- }
+ static bool noZeroCoefficients(const VarCoeffArray& arr);
/**
* Zips together an array of variables and coefficients and appends
@@ -73,7 +52,7 @@ public:
const std::vector< Rational >& coefficients,
VarCoeffArray& output);
- static void merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c);
+ static void merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c, std::vector<uint32_t>& count);
protected:
@@ -84,6 +63,8 @@ protected:
*/
VarCoeffArray d_entries;
+ std::vector<uint32_t>& d_rowCount;
+
NonZeroIterator lower_bound(ArithVar x_j) const{
return std::lower_bound(d_entries.begin(), d_entries.end(), make_pair(x_j,0), cmp);
}
@@ -92,10 +73,11 @@ protected:
public:
- RowVector() : d_entries() {}
+ //RowVector() : d_entries() {}
RowVector(const std::vector< ArithVar >& variables,
- const std::vector< Rational >& coefficients);
+ const std::vector< Rational >& coefficients,
+ std::vector<uint32_t>& counts);
//Iterates over the nonzero entries in the Vector
@@ -154,7 +136,8 @@ public:
ReducedRowVector(ArithVar basic,
const std::vector< ArithVar >& variables,
- const std::vector< Rational >& coefficients);
+ const std::vector< Rational >& coefficients,
+ std::vector<uint32_t>& count);
ArithVar basic() const{
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index e435fd3dc..e30d935f3 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -306,6 +306,9 @@ template <bool above>
ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
ReducedRowVector* row_i = d_tableau.lookup(x_i);
+ ArithVar slack = ARITHVAR_SENTINEL;
+ uint32_t numRows = std::numeric_limits<uint32_t>::max();
+
for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero();
nbi != end; ++nbi){
ArithVar nonbasic = getArithVar(*nbi);
@@ -315,24 +318,63 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
int cmp = a_ij.cmp(d_constants.d_ZERO);
if(above){ // beta(x_i) > u_i
if( cmp < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){
- return nonbasic;
+ if(d_pivotStage){
+ if(d_tableau.getRowCount(nonbasic) < numRows){
+ slack = nonbasic;
+ numRows = d_tableau.getRowCount(nonbasic);
+ }
+ }else{
+ slack = nonbasic; break;
+ }
}else if( cmp > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
- return nonbasic;
+ if(d_pivotStage){
+ if(d_tableau.getRowCount(nonbasic) < numRows){
+ slack = nonbasic;
+ numRows = d_tableau.getRowCount(nonbasic);
+ }
+ }else{
+ slack = nonbasic; break;
+ }
}
}else{ //beta(x_i) < l_i
if(cmp > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){
- return nonbasic;
- }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
- return nonbasic;
+ if(d_pivotStage){
+ if(d_tableau.getRowCount(nonbasic) < numRows){
+ slack = nonbasic;
+ numRows = d_tableau.getRowCount(nonbasic);
+ }
+ }else{
+ slack = nonbasic; break;
+ }
+ }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){if(d_pivotStage){
+ if(d_tableau.getRowCount(nonbasic) < numRows){
+ slack = nonbasic;
+ numRows = d_tableau.getRowCount(nonbasic);
+ }
+ }else{
+ slack = nonbasic; break;
+ }
}
}
}
- return ARITHVAR_SENTINEL;
+
+ return slack;
}
Node SimplexDecisionProcedure::updateInconsistentVars(){
+ Node possibleConflict = privateUpdateInconsistentVars();
+ Assert(!possibleConflict.isNull() || d_griggioRuleQueue.empty());
+ Assert(!possibleConflict.isNull() || d_possiblyInconsistent.empty());
d_pivotStage = true;
- return privateUpdateInconsistentVars();
+
+ while(!d_griggioRuleQueue.empty()){
+ d_griggioRuleQueue.pop();
+ }
+ while(!d_possiblyInconsistent.empty()){
+ d_possiblyInconsistent.pop();
+ }
+
+ return possibleConflict;
}
//corresponds to Check() in dM06
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 440d7063c..e753ebc28 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -75,7 +75,8 @@ public:
d_activityMonitor(am),
d_out(out),
d_tableau(tableau),
- d_numVariables(0)
+ d_numVariables(0),
+ d_pivotStage(true)
{}
void increaseMax() {d_numVariables++;}
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 3c1cd36ba..1d58c5e1d 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -34,7 +34,7 @@ void Tableau::addRow(ArithVar basicVar,
//The new basic variable cannot already be a basic variable
Assert(!isActiveBasicVariable(basicVar));
d_activeBasicVars.insert(basicVar);
- ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs);
+ ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount);
d_rowsTable[basicVar] = row_current;
//A variable in the row may have been made non-basic already.
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 758e5d92d..5e34ac1a2 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -97,6 +97,8 @@ private:
ActivityMonitor& d_activityMonitor;
ArithVarDenseSet& d_basicManager;
+ std::vector<uint32_t> d_rowCount;
+
public:
/**
* Constructs an empty tableau.
@@ -111,6 +113,7 @@ public:
void increaseSize(){
d_activeBasicVars.increaseSize();
d_rowsTable.push_back(NULL);
+ d_rowCount.push_back(0);
}
ArithVarSet::iterator begin(){
@@ -133,6 +136,11 @@ private:
}
public:
+ uint32_t getRowCount(ArithVar x){
+ Assert(x < d_rowCount.size());
+ return d_rowCount[x];
+ }
+
void addRow(ArithVar basicVar,
const std::vector<Rational>& coeffs,
const std::vector<ArithVar>& variables);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback