d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
d_statUpdateConflicts("theory::arith::UpdateConflicts", 0),
- d_statEjections("theory::arith::Ejections", 0),
- d_statUnEjections("theory::arith::UnEjections", 0),
d_statEarlyConflicts("theory::arith::EarlyConflicts", 0),
d_statEarlyConflictImprovements("theory::arith::EarlyConflictImprovements", 0),
d_selectInitialConflictTime("theory::arith::selectInitialConflictTime"),
StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
StatisticsRegistry::registerStat(&d_statUpdateConflicts);
- StatisticsRegistry::registerStat(&d_statEjections);
- StatisticsRegistry::registerStat(&d_statUnEjections);
StatisticsRegistry::registerStat(&d_statEarlyConflicts);
StatisticsRegistry::registerStat(&d_statEarlyConflictImprovements);
StatisticsRegistry::registerStat(&d_selectInitialConflictTime);
StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
- StatisticsRegistry::unregisterStat(&d_statEjections);
- StatisticsRegistry::unregisterStat(&d_statUnEjections);
StatisticsRegistry::unregisterStat(&d_statEarlyConflicts);
StatisticsRegistry::unregisterStat(&d_statEarlyConflictImprovements);
StatisticsRegistry::unregisterStat(&d_selectInitialConflictTime);
StatisticsRegistry::unregisterStat(&d_pivotTime);
}
-
-/*
-void SimplexDecisionProcedure::ejectInactiveVariables(){
- return; //die die die
-
- for(ArithVarSet::iterator i = d_tableau.begin(), end = d_tableau.end(); i != end;){
- ArithVar variable = *i;
- ++i;
- Assert(d_basicManager.isMember(variable));
-
- if(d_basicManager.isMember(variable) && shouldEject(variable)){
- Debug("decay") << "ejecting basic " << variable << endl;
- ++(d_statistics.d_statEjections);
- d_tableau.ejectBasic(variable);
- }
- }
-}
-*/
-
-/*
-void SimplexDecisionProcedure::reinjectVariable(ArithVar x){
- ++(d_statistics.d_statUnEjections);
-
- d_tableau.reinjectBasic(x);
-
- DeltaRational safeAssignment = computeRowValue(x, true);
- DeltaRational assignment = computeRowValue(x, false);
- d_partialModel.setAssignment(x,safeAssignment,assignment);
-}
-*/
-
-/*
-bool SimplexDecisionProcedure::shouldEject(ArithVar var){
- if(d_partialModel.hasEitherBound(var)){
- return false;
- }else if(d_tableau.isEjected(var)) {
- return false;
- }else if(!d_partialModel.hasEverHadABound(var)){
- return true;
- }else if(d_activityMonitor[var] >= ACTIVITY_THRESHOLD){
- return false;
- }
- return false;
-}
-*/
-
/* procedure AssertLower( x_i >= c_i ) */
bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
- /*
- if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
- reinjectVariable(x_i);
- }
- */
-
if(d_partialModel.belowLowerBound(x_i, c_i, false)){
return false; //sat
}
bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){
Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
- /*
- if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
- reinjectVariable(x_i);
- }
- */
if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i
return false; //sat
Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
- /*
- if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
- reinjectVariable(x_i);
- }
- */
-
// u_i <= c_i <= l_i
// This can happen if both c_i <= x_i and x_i <= c_i are in the system.
if(d_partialModel.belowLowerBound(x_i, c_i, false) &&
Debug("arith") << "updateInconsistentVars" << endl;
uint32_t iteratationNum = 0;
- //static const int EJECT_FREQUENCY = 10;
while(!d_pivotStage || iteratationNum <= d_numVariables){
if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
}
++iteratationNum;
- /*
- if(iteratationNum % EJECT_FREQUENCY == 0)
- ejectInactiveVariables();
- */
DeltaRational beta_i = d_partialModel.getAssignment(x_i);
ArithVar x_j = ARITHVAR_SENTINEL;
Node generateConflictBelow(ArithVar conflictVar);
public:
- /** Checks to make sure the assignment is consistent with the tableau. */
+ /**
+ * Checks to make sure the assignment is consistent with the tableau.
+ * This code is for debugging.
+ */
void checkTableau();
-private:
- //bool shouldEject(ArithVar var);
- //void ejectInactiveVariables();
-
-public:
- //void reinjectVariable(ArithVar x);
-
/**
* Computes the value of a basic variable using the assignments
* of the values of the variables in the basic variable's row tableau.
*/
Node checkBasicForConflict(ArithVar b);
- bool d_foundAConflict;
- unsigned d_pivotsSinceConflict;
+ bool d_foundAConflict; // This field is used for statistics keeping ONLY!
+ unsigned d_pivotsSinceConflict; // This field is used for statistics keeping ONLY!
/** These fields are designed to be accessable to TheoryArith methods. */
class Statistics {
public:
- IntStat d_statPivots, d_statUpdates, d_statAssertUpperConflicts;
- IntStat d_statAssertLowerConflicts, d_statUpdateConflicts;
-
- IntStat d_statEjections, d_statUnEjections;
+ IntStat d_statPivots, d_statUpdates;
+ IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts;
+ IntStat d_statUpdateConflicts;
IntStat d_statEarlyConflicts, d_statEarlyConflictImprovements;
TimerStat d_selectInitialConflictTime;
ArithVar var = *varsIter;
if(d_basicManager.isMember(var)){
- /*
- if(!isActiveBasicVariable(var)){
- reinjectBasic(var);
- }
- Assert(isActiveBasicVariable(var));
- */
Assert(d_activeBasicVars.isMember(var));
ReducedRowVector& row_var = lookup(var);
}
}
}
-
-
-/*
-void Tableau::updateRow(ReducedRowVector* row){
- ArithVar basic = row->basic();
- for(ReducedRowVector::NonZeroIterator i=row->beginNonZero(), endIter = row->endNonZero(); i != endIter; ){
- ArithVar var = i->first;
- ++i;
- if(var != basic && d_basicManager.isMember(var)){
- ReducedRowVector* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
-
- Assert(row_var != row);
- row->substitute(*row_var);
-
- i = row->beginNonZero();
- endIter = row->endNonZero();
- }
- }
-}
-*/
return *(d_rowsTable[var]);
}
- /*
-private:
- ReducedRowVector* lookupEjected(ArithVar var){
- Assert(isEjected(var));
- return d_rowsTable[var];
- }
- */
public:
-
-
uint32_t getRowCount(ArithVar x){
Assert(x < d_rowCount.size());
return d_rowCount[x];
}
-
+ /**
+ * Adds a row to the tableau.
+ * The new row is equivalent to:
+ * basicVar = \sum_i coeffs[i] * variables[i]
+ * preconditions:
+ * basicVar is already declared to be basic
+ * basicVar does not have a row associated with it in the tableau.
+ *
+ * Note: each variables[i] does not have to be non-basic.
+ * Pivoting will be mimicked if it is basic.
+ */
void addRow(ArithVar basicVar,
const std::vector<Rational>& coeffs,
const std::vector<ArithVar>& variables);
void printTableau();
- /*
- bool isEjected(ArithVar var){
- return d_basicManager.isMember(var) && !isActiveBasicVariable(var);
- }
- */
-
ReducedRowVector* removeRow(ArithVar basic);
-
- /*
- void ejectBasic(ArithVar basic){
- Assert(d_basicManager.isMember(basic));
- Assert(isActiveBasicVariable(basic));
-
- d_activeBasicVars.remove(basic);
- }
- */
-
- /*
- void reinjectBasic(ArithVar basic){
- AlwaysAssert(false);
-
- Assert(d_basicManager.isMember(basic));
- Assert(isEjected(basic));
-
- ReducedRowVector* row = lookupEjected(basic);
- d_activeBasicVars.add(basic);
- updateRow(row);
- }
- */
-private:
- /*
- inline bool isActiveBasicVariable(ArithVar var){
- return d_activeBasicVars.isMember(var);
- }
- */
-
- void updateRow(ReducedRowVector* row);
};
}; /* namespace arith */
TNode rhs = eq[1];
Assert(rhs.getKind() == CONST_RATIONAL);
ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
- /*
- if(d_tableau.isEjected(lhsVar)){
- d_simplex.reinjectVariable(lhsVar);
- }
- */
DeltaRational lhsValue = d_partialModel.getAssignment(lhsVar);
DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
if (lhsValue == rhsValue) {
switch(n.getKind()) {
case kind::VARIABLE: {
ArithVar var = asArithVar(n);
- /*
- if(d_tableau.isEjected(var)){
- d_simplex.reinjectVariable(var);
- }
- */
DeltaRational drat = d_partialModel.getAssignment(var);
const Rational& delta = d_partialModel.getDelta();
projects / cvc5.git / commitdiff