arithvar_set.h \
tableau.h \
tableau.cpp \
+ arith_priority_queue.h \
+ arith_priority_queue.cpp \
simplex.h \
simplex.cpp \
row_vector.h \
--- /dev/null
+
+#include "theory/arith/arith_priority_queue.h"
+
+using namespace std;
+
+using namespace CVC4;
+using namespace CVC4::kind;
+
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+ArithPriorityQueue::ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau):
+ d_partialModel(pm), d_tableau(tableau), d_usingGriggioRule(true)
+{}
+
+ArithVar ArithPriorityQueue::popInconsistentBasicVariable(){
+ Debug("arith_update") << "popInconsistentBasicVariable()" << endl;
+
+ if(usingGriggioRule()){
+ while(!d_griggioRuleQueue.empty()){
+ ArithVar var = d_griggioRuleQueue.top().first;
+ d_griggioRuleQueue.pop();
+ Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl;
+ if(basicAndInconsistent(var)){
+ return var;
+ }
+ }
+ }else{
+ Debug("arith_update") << "possiblyInconsistent.size()"
+ << d_possiblyInconsistent.size() << endl;
+
+ while(!d_possiblyInconsistent.empty()){
+ ArithVar var = d_possiblyInconsistent.top();
+ d_possiblyInconsistent.pop();
+ Debug("arith_update") << "possiblyInconsistent var" << var << endl;
+ if(basicAndInconsistent(var)){
+ return var;
+ }
+ }
+ }
+ return ARITHVAR_SENTINEL;
+}
+
+void ArithPriorityQueue::enqueueIfInconsistent(ArithVar basic){
+ Assert(d_tableau.isBasic(basic));
+ if(basicAndInconsistent(basic)){
+ if( usingGriggioRule() ){
+ const DeltaRational& beta = d_partialModel.getAssignment(basic);
+ DeltaRational diff = d_partialModel.belowLowerBound(basic,beta,true) ?
+ d_partialModel.getLowerBound(basic) - beta:
+ beta - d_partialModel.getUpperBound(basic);
+ d_griggioRuleQueue.push(make_pair(basic,diff));
+ }else{
+ d_possiblyInconsistent.push(basic);
+ }
+ }
+}
+
+
+void ArithPriorityQueue::enqueueTrustedVector(const vector<VarDRatPair>& trusted){
+ Assert(usingGriggioRule());
+ Assert(empty());
+
+ d_griggioRuleQueue = GriggioPQueue(trusted.begin(), trusted.end());
+ Assert(size() == trusted.size());
+}
+
+
+void ArithPriorityQueue::dumpQueueIntoVector(vector<VarDRatPair>& target){
+ Assert(usingGriggioRule());
+ while( !d_griggioRuleQueue.empty()){
+ ArithVar var = d_griggioRuleQueue.top().first;
+ if(basicAndInconsistent(var)){
+ target.push_back( d_griggioRuleQueue.top());
+ }
+ d_griggioRuleQueue.pop();
+ }
+}
+
+
+void ArithPriorityQueue::useGriggioQueue(){
+ Assert(!usingGriggioRule());
+ Assert(d_possiblyInconsistent.empty());
+ Assert(d_griggioRuleQueue.empty());
+ d_usingGriggioRule = true;
+}
+
+void ArithPriorityQueue::useBlandQueue(){
+ Assert(usingGriggioRule());
+ while(!d_griggioRuleQueue.empty()){
+ ArithVar var = d_griggioRuleQueue.top().first;
+ if(basicAndInconsistent(var)){
+ d_possiblyInconsistent.push(var);
+ }
+ d_griggioRuleQueue.pop();
+ }
+ d_usingGriggioRule = false;
+
+ Assert(d_griggioRuleQueue.empty());
+ Assert(!usingGriggioRule());
+}
+
+
+void ArithPriorityQueue::clear(){
+ if(usingGriggioRule() && !d_griggioRuleQueue.empty()){
+ d_griggioRuleQueue = GriggioPQueue();
+ }else if(!d_possiblyInconsistent.empty()) {
+ d_possiblyInconsistent = PQueue();
+ }
+ Assert(d_possiblyInconsistent.empty());
+ Assert(d_griggioRuleQueue.empty());
+}
--- /dev/null
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H
+#define __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H
+
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/delta_rational.h"
+#include "theory/arith/tableau.h"
+#include "theory/arith/partial_model.h"
+
+#include <queue>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+typedef std::pair<ArithVar, DeltaRational> VarDRatPair;
+
+struct VarDRatPairCompare{
+ inline bool operator()(const VarDRatPair& a, const VarDRatPair& b){
+ return a.second > b.second;
+ }
+};
+
+typedef std::priority_queue<VarDRatPair, std::vector<VarDRatPair>, VarDRatPairCompare> GriggioPQueue;
+
+typedef std::priority_queue<ArithVar, vector<ArithVar>, std::greater<ArithVar> > PQueue;
+
+
+class ArithPriorityQueue {
+private:
+ /**
+ * Priority Queue of the basic variables that may be inconsistent.
+ * Variables are ordered according to which violates its bound the most.
+ * This is a hueristic and makes no guarentees to terminate!
+ * This heuristic comes from Alberto Griggio's thesis.
+ */
+ GriggioPQueue d_griggioRuleQueue;
+
+ /**
+ * Priority Queue of the basic variables that may be inconsistent.
+ *
+ * This is required to contain at least 1 instance of every inconsistent
+ * basic variable. This is only required to be a superset though so its
+ * contents must be checked to still be basic and inconsistent.
+ *
+ * This is also required to agree with the row on variable order for termination.
+ * Effectively this means that this must be a min-heap.
+ */
+ PQueue d_possiblyInconsistent;
+
+ /**
+ * Reference to the arithmetic partial model for checking if a variable
+ * is consistent with its upper and lower bounds.
+ */
+ ArithPartialModel& d_partialModel;
+
+ /** Reference to the Tableau for checking if a variable is basic. */
+ const Tableau& d_tableau;
+
+ /**
+ * Controls which priority queue is in use.
+ * If true, d_griggioRuleQueue is used.
+ * If false, d_possiblyInconsistent is used.
+ */
+ bool d_usingGriggioRule;
+
+public:
+ ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau);
+
+ ArithVar popInconsistentBasicVariable();
+
+ void enqueueIfInconsistent(ArithVar basic);
+
+ void enqueueTrustedVector(const vector<VarDRatPair>& trusted);
+
+ void dumpQueueIntoVector(vector<VarDRatPair>& target);
+
+ inline bool basicAndInconsistent(ArithVar var) const{
+ return d_tableau.isBasic(var)
+ && !d_partialModel.assignmentIsConsistent(var) ;
+ }
+
+ void useGriggioQueue();
+
+ void useBlandQueue();
+
+ inline bool usingGriggioRule() const{
+ return d_usingGriggioRule;
+ }
+
+ inline bool empty() const{
+ if(usingGriggioRule()){
+ return d_griggioRuleQueue.empty();
+ }else{
+ return d_possiblyInconsistent.empty();
+ }
+ }
+
+ inline size_t size() const {
+ if(usingGriggioRule()){
+ return d_griggioRuleQueue.size();
+ }else{
+ return d_possiblyInconsistent.size();
+ }
+ }
+
+ void clear();
+};
+
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH_PRIORITY_QUEUE_H */
using namespace CVC4::theory;
using namespace CVC4::theory::arith;
-const static uint64_t ACTIVITY_THRESHOLD = 100;
-
SimplexDecisionProcedure::Statistics::Statistics():
d_statPivots("theory::arith::pivots",0),
d_statUpdates("theory::arith::updates",0),
update(x_i, c_i);
}
}else{
- checkBasicVariable(x_i);
+ d_queue.enqueueIfInconsistent(x_i);
+ //checkBasicVariable(x_i);
}
return false;
update(x_i, c_i);
}
}else{
- checkBasicVariable(x_i);
+ d_queue.enqueueIfInconsistent(x_i);
}
d_partialModel.printModel(x_i);
return false;
update(x_i, c_i);
}
}else{
- checkBasicVariable(x_i);
+ d_queue.enqueueIfInconsistent(x_i);
+ //checkBasicVariable(x_i);
}
return false;
DeltaRational nAssignment = assignment+(diff * a_ji);
d_partialModel.setAssignment(x_j, nAssignment);
- checkBasicVariable(x_j);
+ d_queue.enqueueIfInconsistent(x_j);
+ //checkBasicVariable(x_j);
}
}
DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
d_partialModel.setAssignment(x_k, nextAssignment);
- checkBasicVariable(x_k);
+ d_queue.enqueueIfInconsistent(x_k);
}
}
d_tableau.pivot(x_i, x_j);
- checkBasicVariable(x_j);
+ d_queue.enqueueIfInconsistent(x_j);
// Debug found conflict
if( !d_foundAConflict ){
}
}
-ArithVar SimplexDecisionProcedure::selectSmallestInconsistentVar(){
- Debug("arith_update") << "selectSmallestInconsistentVar()" << endl;
- Debug("arith_update") << "possiblyInconsistent.size()"
- << d_possiblyInconsistent.size() << endl;
-
- if(d_pivotStage){
- while(!d_griggioRuleQueue.empty()){
- ArithVar var = d_griggioRuleQueue.top().first;
- Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl;
- if(d_tableau.isBasic(var)){
- if(!d_partialModel.assignmentIsConsistent(var)){
- return var;
- }
- }
- d_griggioRuleQueue.pop();
- }
- }else{
- while(!d_possiblyInconsistent.empty()){
- ArithVar var = d_possiblyInconsistent.top();
- Debug("arith_update") << "possiblyInconsistent var" << var << endl;
- if(d_tableau.isBasic(var)){
- if(!d_partialModel.assignmentIsConsistent(var)){
- return var;
- }
- }
- d_possiblyInconsistent.pop();
- }
- }
- return ARITHVAR_SENTINEL;
-}
-
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();
+ bool pivotStage = d_queue.usingGriggioRule();
+
for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
nbi != end; ++nbi){
ArithVar nonbasic = getArithVar(*nbi);
int cmp = a_ij.cmp(d_constants.d_ZERO);
if(above){ // beta(x_i) > u_i
if( cmp < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){
- if(d_pivotStage){
+ if(pivotStage){
if(d_tableau.getRowCount(nonbasic) < numRows){
slack = nonbasic;
numRows = d_tableau.getRowCount(nonbasic);
slack = nonbasic; break;
}
}else if( cmp > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
- if(d_pivotStage){
+ if(pivotStage){
if(d_tableau.getRowCount(nonbasic) < numRows){
slack = nonbasic;
numRows = d_tableau.getRowCount(nonbasic);
}
}else{ //beta(x_i) < l_i
if(cmp > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){
- if(d_pivotStage){
+ if(pivotStage){
if(d_tableau.getRowCount(nonbasic) < numRows){
slack = nonbasic;
numRows = d_tableau.getRowCount(nonbasic);
slack = nonbasic; break;
}
}else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
- if(d_pivotStage){
+ if(pivotStage){
if(d_tableau.getRowCount(nonbasic) < numRows){
slack = nonbasic;
numRows = d_tableau.getRowCount(nonbasic);
TimerStat::CodeTimer codeTimer(d_statistics.d_selectInitialConflictTime);
vector<VarDRatPair> init;
-
- while( !d_griggioRuleQueue.empty()){
- ArithVar var = d_griggioRuleQueue.top().first;
- if(d_tableau.isBasic(var)){
- if(!d_partialModel.assignmentIsConsistent(var)){
- init.push_back( d_griggioRuleQueue.top());
- }
- }
- d_griggioRuleQueue.pop();
- }
+ d_queue.dumpQueueIntoVector(init);
int conflictChanges = 0;
-
- for(vector<VarDRatPair>::iterator i=init.begin(), end=init.end(); i != end; ++i){
+ vector<VarDRatPair>::iterator i=init.begin(), end=init.end();
+ for(; i != end; ++i){
ArithVar x_i = (*i).first;
- d_griggioRuleQueue.push(*i);
Node possibleConflict = checkBasicForConflict(x_i);
if(!possibleConflict.isNull()){
++(d_statistics.d_statEarlyConflicts);
}
}
+ if(bestConflict.isNull()){
+ d_queue.enqueueTrustedVector(init);
+ }
+
if(conflictChanges > 1) ++(d_statistics.d_statEarlyConflictImprovements);
return bestConflict;
}
Node SimplexDecisionProcedure::updateInconsistentVars(){
- if(d_griggioRuleQueue.empty()) return Node::null();
+ if(d_queue.empty()){
+ return Node::null();
+ }
d_foundAConflict = false;
d_pivotsSinceConflict = 0;
Node possibleConflict = Node::null();
- if(d_griggioRuleQueue.size() > 1){
+ if(d_queue.size() > 1){
possibleConflict = selectInitialConflict();
}
if(possibleConflict.isNull()){
- possibleConflict = privateUpdateInconsistentVars();
+ possibleConflict = searchForFeasibleSolution<true>(d_numVariables + 1);
}
- Assert(!possibleConflict.isNull() || d_griggioRuleQueue.empty());
- Assert(!possibleConflict.isNull() || d_possiblyInconsistent.empty());
- d_pivotStage = true;
-
- while(!d_griggioRuleQueue.empty()){
- d_griggioRuleQueue.pop();
+ if(possibleConflict.isNull()){
+ d_queue.useBlandQueue();
+ possibleConflict = searchForFeasibleSolution<false>(0);
}
- while(!d_possiblyInconsistent.empty()){
- d_possiblyInconsistent.pop();
+
+ Assert(!possibleConflict.isNull() || d_queue.empty());
+
+ // Curiously the invariant that we always do a full check
+ // means that the assignment we can always empty these queues.
+ d_queue.clear();
+
+ if(!d_queue.usingGriggioRule()){
+ d_queue.useGriggioQueue();
}
+ Assert(d_queue.usingGriggioRule());
return possibleConflict;
}
}
//corresponds to Check() in dM06
-Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
- Assert(d_pivotStage || d_griggioRuleQueue.empty());
+template <bool limitIterations>
+Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
Debug("arith") << "updateInconsistentVars" << endl;
- uint32_t iteratationNum = 0;
+ //uint32_t iteratationNum = 0;
- while(!d_pivotStage || iteratationNum <= d_numVariables){
+ while(!limitIterations || remainingIterations > 0){
if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
- ArithVar x_i = selectSmallestInconsistentVar();
+ ArithVar x_i = d_queue.popInconsistentBasicVariable();
+ //selectSmallestInconsistentVar<useGriggioQueue>();
Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
if(x_i == ARITHVAR_SENTINEL){
Debug("arith_update") << "No inconsistent variables" << endl;
return Node::null(); //sat
}
- ++iteratationNum;
+ --remainingIterations;
DeltaRational beta_i = d_partialModel.getAssignment(x_i);
ArithVar x_j = ARITHVAR_SENTINEL;
if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
- DeltaRational l_i = d_partialModel.getLowerBound(x_i);
x_j = selectSlackBelow(x_i);
if(x_j == ARITHVAR_SENTINEL ){
++(d_statistics.d_statUpdateConflicts);
return generateConflictBelow(x_i); //unsat
}
+ DeltaRational l_i = d_partialModel.getLowerBound(x_i);
pivotAndUpdate(x_i, x_j, l_i);
}else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
- DeltaRational u_i = d_partialModel.getUpperBound(x_i);
x_j = selectSlackAbove(x_i);
if(x_j == ARITHVAR_SENTINEL ){
++(d_statistics.d_statUpdateConflicts);
return generateConflictAbove(x_i); //unsat
}
+ DeltaRational u_i = d_partialModel.getUpperBound(x_i);
pivotAndUpdate(x_i, x_j, u_i);
}
Assert(x_j != ARITHVAR_SENTINEL);
return earlyConflict;
}
}
-
- if(d_pivotStage && iteratationNum >= d_numVariables){
- while(!d_griggioRuleQueue.empty()){
- ArithVar var = d_griggioRuleQueue.top().first;
- if(d_tableau.isBasic(var)){
- d_possiblyInconsistent.push(var);
- }
- d_griggioRuleQueue.pop();
- }
-
- d_pivotStage = false;
- return privateUpdateInconsistentVars();
+ if(remainingIterations == 0 && limitIterations){
+ return Node::null();
}
Unreachable();
return sum;
}
-
+/*
void SimplexDecisionProcedure::checkBasicVariable(ArithVar basic){
Assert(d_tableau.isBasic(basic));
if(!d_partialModel.assignmentIsConsistent(basic)){
}
}
}
+*/
/**
* This check is quite expensive.
#define __CVC4__THEORY__ARITH__SIMPLEX_H
#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arith_priority_queue.h"
#include "theory/arith/arithvar_set.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/tableau.h"
class SimplexDecisionProcedure {
private:
- typedef std::pair<ArithVar, DeltaRational> VarDRatPair;
- struct VarDRatPairCompare{
- inline bool operator()(const VarDRatPair& a, const VarDRatPair& b){
- return a.second > b.second;
- }
- };
- typedef std::priority_queue<VarDRatPair, std::vector<VarDRatPair>, VarDRatPairCompare> GriggioPQueue;
-
- GriggioPQueue d_griggioRuleQueue;
-
- /**
- * Priority Queue of the basic variables that may be inconsistent.
- *
- * This is required to contain at least 1 instance of every inconsistent
- * basic variable. This is only required to be a superset though so its
- * contents must be checked to still be basic and inconsistent.
- *
- * This is also required to agree with the row on variable order for termination.
- * Effectively this means that this must be a min-heap.
- */
- typedef std::priority_queue<ArithVar, vector<ArithVar>, std::greater<ArithVar> > PQueue;
-
- PQueue d_possiblyInconsistent;
/** Stores system wide constants to avoid unnessecary reconstruction. */
const ArithConstants& d_constants;
OutputChannel* d_out;
Tableau& d_tableau;
+ ArithPriorityQueue d_queue;
ArithVar d_numVariables;
- bool d_pivotStage;
-
public:
SimplexDecisionProcedure(const ArithConstants& constants,
ArithPartialModel& pm,
OutputChannel* out,
Tableau& tableau) :
- d_possiblyInconsistent(),
d_constants(constants),
d_partialModel(pm),
d_out(out),
d_tableau(tableau),
- d_numVariables(0),
- d_pivotStage(true)
+ d_queue(pm, tableau),
+ d_numVariables(0)
{}
void increaseMax() {d_numVariables++;}
*/
Node updateInconsistentVars();
private:
- Node privateUpdateInconsistentVars();
+ template <bool limitIterations> Node searchForFeasibleSolution(uint32_t maxIterations);
Node selectInitialConflict();
DeltaRational computeRowValue(ArithVar x, bool useSafe);
private:
- /** Check to make sure all of the basic variables are within their bounds. */
- void checkBasicVariable(ArithVar basic);
/**
* Checks a basic variable, b, to see if it is in conflict.
projects / cvc5.git / commitdiff