ordered_bounds_list.h \
ordered_set.h \
arithvar_dense_set.h \
+ arithvar_set.h \
tableau.h \
tableau.cpp \
simplex.h \
--- /dev/null
+/********************* */
+/*! \file arithvar_set.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <vector>
+#include "theory/arith/arith_utilities.h"
+
+
+#ifndef __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
+#define __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/**
+ * This is an abstraction of a set of ArithVars.
+ * This class is designed to provide constant time insertion, deletion, and element_of
+ * and fast iteration.
+ * The cost of doing this is that it takes O(M) where M is the total number
+ * of ArithVars in memory.
+ */
+
+class ArithVarSet {
+private:
+ typedef std::vector<ArithVar> VarList;
+ //List of the ArithVars in the set.
+ VarList d_list;
+
+ //Each ArithVar in the set is mapped to its position in d_list.
+ //Each ArithVar not in the set is mapped to ARITHVAR_SENTINEL
+ std::vector<unsigned> d_posVector;
+
+public:
+ typedef VarList::const_iterator iterator;
+
+ ArithVarSet() : d_list(), d_posVector() {}
+
+ size_t size() const {
+ return d_list.size();
+ }
+
+ size_t allocated() const {
+ return d_posVector.size();
+ }
+
+ void increaseSize(ArithVar max){
+ Assert(max >= allocated());
+ d_posVector.resize(max+1, ARITHVAR_SENTINEL);
+ }
+
+ void increaseSize(){
+ increaseSize(allocated());
+ }
+
+ bool isMember(ArithVar x) const{
+ Assert(x < allocated());
+ return d_posVector[x] != ARITHVAR_SENTINEL;
+ }
+
+ /** Invalidates iterators */
+ void init(ArithVar x, bool val) {
+ Assert(x >= size());
+ increaseSize(x);
+ if(val){
+ add(x);
+ }
+ }
+
+ /** Invalidates iterators */
+ void add(ArithVar x){
+ Assert(!isMember(x));
+ d_posVector[x] = size();
+ d_list.push_back(x);
+ }
+
+ iterator begin() const{ return d_list.begin(); }
+ iterator end() const{ return d_list.end(); }
+
+
+ /** Invalidates iterators */
+ void remove(ArithVar x){
+ Assert(isMember(x));
+ swapToBack(x);
+ d_posVector[x] = ARITHVAR_SENTINEL;
+ d_list.pop_back();
+ }
+
+ private:
+
+ /** This should be true of all x < allocated() after every operation. */
+ bool wellFormed(ArithVar x){
+ if(d_posVector[x] == ARITHVAR_SENTINEL){
+ return true;
+ }else{
+ return d_list[d_posVector[x]] == x;
+ }
+ }
+
+ /** Swaps a member x to the back of d_list. */
+ void swapToBack(ArithVar x){
+ Assert(isMember(x));
+
+ unsigned currentPos = d_posVector[x];
+ ArithVar atBack = d_list.back();
+
+ d_list[currentPos] = atBack;
+ d_posVector[atBack] = currentPos;
+
+ d_list[size() - 1] = x;
+ d_posVector[x] = size() - 1;
+ }
+};
+
+}; /* namespace arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_SET_H */
static bool isMember(Node n) {
if (n.getKind() == kind::CONST_INTEGER) return false;
if (n.getKind() == kind::CONST_RATIONAL) return false;
+ if (isRelationOperator(n.getKind())) return false;
return Theory::isLeafOf(n, theory::THEORY_ARITH);
}
d_statUnEjections("theory::arith::UnEjections", 0),
d_statEarlyConflicts("theory::arith::EarlyConflicts", 0),
d_statEarlyConflictImprovements("theory::arith::EarlyConflictImprovements", 0),
- d_selectInitialConflictTime("theory::arith::selectInitialConflictTime")
+ d_selectInitialConflictTime("theory::arith::selectInitialConflictTime"),
+ d_pivotsAfterConflict("theory::arith::pivotsAfterConflict", 0),
+ d_checksWithWastefulPivots("theory::arith::checksWithWastefulPivots", 0),
+ d_pivotTime("theory::arith::pivotTime")
{
StatisticsRegistry::registerStat(&d_statPivots);
StatisticsRegistry::registerStat(&d_statUpdates);
StatisticsRegistry::registerStat(&d_statEarlyConflicts);
StatisticsRegistry::registerStat(&d_statEarlyConflictImprovements);
StatisticsRegistry::registerStat(&d_selectInitialConflictTime);
+
+ StatisticsRegistry::registerStat(&d_pivotsAfterConflict);
+ StatisticsRegistry::registerStat(&d_checksWithWastefulPivots);
+ StatisticsRegistry::registerStat(&d_pivotTime);
}
SimplexDecisionProcedure::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_statEarlyConflicts);
StatisticsRegistry::unregisterStat(&d_statEarlyConflictImprovements);
StatisticsRegistry::unregisterStat(&d_selectInitialConflictTime);
+
+ StatisticsRegistry::unregisterStat(&d_pivotsAfterConflict);
+ StatisticsRegistry::unregisterStat(&d_checksWithWastefulPivots);
+ 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;
void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
Assert(x_i != x_j);
+ 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::NonZeroIterator varIter = row_k->beginNonZero();
+ varIter != row_k->endNonZero();
+ ++varIter){
+
+ ArithVar var = varIter->first;
+ const Rational& coeff = varIter->second;
+ 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;
+ }
+
+
ReducedRowVector* row_i = d_tableau.lookup(x_i);
const Rational& a_ij = row_i->lookup(x_j);
}
}
+ // Pivots
++(d_statistics.d_statPivots);
+ if( d_foundAConflict ){
+ ++d_pivotsSinceConflict;
+ if(d_pivotsSinceConflict == 1){
+ ++(d_statistics.d_checksWithWastefulPivots);
+ }
+ ++(d_statistics.d_pivotsAfterConflict);
+ }
+
d_tableau.pivot(x_i, x_j);
checkBasicVariable(x_j);
+ // Debug found conflict
+ if( !d_foundAConflict ){
+ DeltaRational beta_j = d_partialModel.getAssignment(x_j);
+
+ if(d_partialModel.belowLowerBound(x_j, beta_j, true)){
+ if(selectSlackBelow(x_j) == ARITHVAR_SENTINEL ){
+ d_foundAConflict = true;
+ }
+ }else if(d_partialModel.aboveUpperBound(x_j, beta_j, true)){
+ if(selectSlackAbove(x_j) == ARITHVAR_SENTINEL ){
+ d_foundAConflict = true;
+ }
+ }
+ }
+
if(Debug.isOn("tableau")){
d_tableau.printTableau();
}
}else{
slack = nonbasic; break;
}
- }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){if(d_pivotStage){
+ }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
+ if(d_pivotStage){
if(d_tableau.getRowCount(nonbasic) < numRows){
slack = nonbasic;
numRows = d_tableau.getRowCount(nonbasic);
ArithVar x_i = (*i).first;
d_griggioRuleQueue.push(*i);
- DeltaRational beta_i = d_partialModel.getAssignment(x_i);
+ Node possibleConflict = checkBasicForConflict(x_i);
+ if(!possibleConflict.isNull()){
+ Node better = betterConflict(bestConflict, possibleConflict);
- if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
- DeltaRational l_i = d_partialModel.getLowerBound(x_i);
- ArithVar x_j = selectSlackBelow(x_i);
- if(x_j == ARITHVAR_SENTINEL ){
- Node better = betterConflict(bestConflict, generateConflictBelow(x_i));
- if(better != bestConflict) ++conflictChanges;
- bestConflict = better;
- ++(d_statistics.d_statEarlyConflicts);
- }
- }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
- DeltaRational u_i = d_partialModel.getUpperBound(x_i);
- ArithVar x_j = selectSlackAbove(x_i);
- if(x_j == ARITHVAR_SENTINEL ){
- Node better = betterConflict(bestConflict, generateConflictAbove(x_i));
- if(better != bestConflict) ++conflictChanges;
- bestConflict = better;
- ++(d_statistics.d_statEarlyConflicts);
+ if(better != bestConflict){
+ ++conflictChanges;
}
+ bestConflict = better;
+ ++(d_statistics.d_statEarlyConflicts);
}
}
if(conflictChanges > 1) ++(d_statistics.d_statEarlyConflictImprovements);
Node SimplexDecisionProcedure::updateInconsistentVars(){
if(d_griggioRuleQueue.empty()) return Node::null();
- Node possibleConflict = selectInitialConflict();
+ d_foundAConflict = false;
+ d_pivotsSinceConflict = 0;
+
+ Node possibleConflict = Node::null();
+ if(d_griggioRuleQueue.size() > 1){
+ possibleConflict = selectInitialConflict();
+ }
if(possibleConflict.isNull()){
possibleConflict = privateUpdateInconsistentVars();
}
return possibleConflict;
}
+Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
+
+ Assert(d_basicManager.isMember(basic));
+ const DeltaRational& beta = d_partialModel.getAssignment(basic);
+
+ if(d_partialModel.belowLowerBound(basic, beta, true)){
+ ArithVar x_j = selectSlackBelow(basic);
+ if(x_j == ARITHVAR_SENTINEL ){
+ return generateConflictBelow(basic);
+ }
+ }else if(d_partialModel.aboveUpperBound(basic, beta, true)){
+ ArithVar x_j = selectSlackAbove(basic);
+ if(x_j == ARITHVAR_SENTINEL ){
+ return generateConflictAbove(basic);
+ }
+ }
+ return Node::null();
+}
+
//corresponds to Check() in dM06
Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
Assert(d_pivotStage || d_griggioRuleQueue.empty());
if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
ArithVar x_i = selectSmallestInconsistentVar();
- Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
+ Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
if(x_i == ARITHVAR_SENTINEL){
Debug("arith_update") << "No inconsistent variables" << endl;
return Node::null(); //sat
ejectInactiveVariables();
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);
- ArithVar x_j = selectSlackBelow(x_i);
+ x_j = selectSlackBelow(x_i);
if(x_j == ARITHVAR_SENTINEL ){
++(d_statistics.d_statUpdateConflicts);
return generateConflictBelow(x_i); //unsat
}else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
DeltaRational u_i = d_partialModel.getUpperBound(x_i);
- ArithVar x_j = selectSlackAbove(x_i);
+ x_j = selectSlackAbove(x_i);
if(x_j == ARITHVAR_SENTINEL ){
++(d_statistics.d_statUpdateConflicts);
return generateConflictAbove(x_i); //unsat
}
pivotAndUpdate(x_i, x_j, u_i);
}
+ Assert(x_j != ARITHVAR_SENTINEL);
+ //Check to see if we already have a conflict with x_j to prevent wasteful work
+ Node earlyConflict = checkBasicForConflict(x_j);
+ if(!earlyConflict.isNull()){
+ return earlyConflict;
+ }
}
if(d_pivotStage && iteratationNum >= d_numVariables){
#define __CVC4__THEORY__ARITH__SIMPLEX_H
#include "theory/arith/arith_utilities.h"
-#include "theory/arith/arithvar_dense_set.h"
+#include "theory/arith/arithvar_set.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/tableau.h"
#include "theory/arith/partial_model.h"
*/
ArithPartialModel& d_partialModel;
- ArithVarDenseSet& d_basicManager;
+ ArithVarSet& d_basicManager;
ActivityMonitor& d_activityMonitor;
OutputChannel* d_out;
public:
SimplexDecisionProcedure(const ArithConstants& constants,
ArithPartialModel& pm,
- ArithVarDenseSet& bm,
+ ArithVarSet& bm,
OutputChannel* out,
ActivityMonitor& am,
Tableau& tableau) :
/** 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.
+ * If a conflict is discovered a node summarizing the conflict is returned.
+ * Otherwise, Node::null() is returned.
+ */
+ Node checkBasicForConflict(ArithVar b);
+
+ bool d_foundAConflict;
+ unsigned d_pivotsSinceConflict;
/** These fields are designed to be accessable to TheoryArith methods. */
class Statistics {
IntStat d_statEjections, d_statUnEjections;
IntStat d_statEarlyConflicts, d_statEarlyConflictImprovements;
+
TimerStat d_selectInitialConflictTime;
+
+ IntStat d_pivotsAfterConflict, d_checksWithWastefulPivots;
+ TimerStat d_pivotTime;
Statistics();
~Statistics();
};
//The new basic variable cannot already be a basic variable
Assert(!isActiveBasicVariable(basicVar));
- d_activeBasicVars.insert(basicVar);
+ d_activeBasicVars.add(basicVar);
ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount);
d_rowsTable[basicVar] = row_current;
d_rowsTable[x_s] = row_s;
d_rowsTable[x_r] = NULL;
- d_activeBasicVars.erase(x_r);
+ d_activeBasicVars.remove(x_r);
d_basicManager.remove(x_r);
- d_activeBasicVars.insert(x_s);
+ d_activeBasicVars.add(x_s);
d_basicManager.add(x_s);
row_s->pivot(x_s);
#include "expr/attribute.h"
#include "theory/arith/arith_utilities.h"
-#include "theory/arith/arithvar_dense_set.h"
+#include "theory/arith/arithvar_set.h"
#include "theory/arith/normal_form.h"
#include "theory/arith/row_vector.h"
namespace theory {
namespace arith {
-class ArithVarSet {
-private:
- typedef std::list<ArithVar> VarList;
-
-public:
- typedef VarList::const_iterator iterator;
-
-private:
- VarList d_list;
- std::vector< VarList::iterator > d_posVector;
-
-public:
- ArithVarSet() : d_list(), d_posVector() {}
-
- iterator begin() const{ return d_list.begin(); }
- iterator end() const{ return d_list.end(); }
-
- void insert(ArithVar av){
- Assert(inRange(av) );
- Assert(!inSet(av) );
-
- d_posVector[av] = d_list.insert(d_list.end(), av);
- }
-
- void erase(ArithVar var){
- Assert( inRange(var) );
- Assert( inSet(var) );
-
- d_list.erase(d_posVector[var]);
- d_posVector[var] = d_list.end();
- }
-
- void increaseSize(){
- d_posVector.push_back(d_list.end());
- }
-
- bool inSet(ArithVar v) const{
- Assert(inRange(v) );
-
- return d_posVector[v] != d_list.end();
- }
-
-private:
- bool inRange(ArithVar v) const{
- return v < d_posVector.size();
- }
-};
-
class Tableau {
private:
ActivityMonitor& d_activityMonitor;
- ArithVarDenseSet& d_basicManager;
+ ArithVarSet& d_basicManager;
std::vector<uint32_t> d_rowCount;
/**
* Constructs an empty tableau.
*/
- Tableau(ActivityMonitor &am, ArithVarDenseSet& bm) :
+ Tableau(ActivityMonitor &am, ArithVarSet& bm) :
d_activeBasicVars(),
d_rowsTable(),
d_activityMonitor(am),
Assert(d_basicManager.isMember(basic));
Assert(isActiveBasicVariable(basic));
- d_activeBasicVars.erase(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.insert(basic);
+ d_activeBasicVars.add(basic);
updateRow(row);
}
private:
inline bool isActiveBasicVariable(ArithVar var){
- return d_activeBasicVars.inSet(var);
+ return d_activeBasicVars.isMember(var);
}
void updateRow(ReducedRowVector* row);
#include "theory/arith/delta_rational.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/tableau.h"
-#include "theory/arith/arithvar_dense_set.h"
+#include "theory/arith/arithvar_set.h"
#include "theory/arith/arith_rewriter.h"
#include "theory/arith/unate_propagator.h"
d_constants(NodeManager::currentNM()),
d_partialModel(c),
d_basicManager(),
+ d_userVariables(),
d_activityMonitor(),
d_diseq(c),
d_tableau(d_activityMonitor, d_basicManager),
d_statSlackVariables("theory::arith::SlackVariables", 0),
d_statDisequalitySplits("theory::arith::DisequalitySplits", 0),
d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0),
- d_staticLearningTimer("theory::arith::staticLearningTimer")
+ d_staticLearningTimer("theory::arith::staticLearningTimer"),
+ d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
+ d_presolveTime("theory::arith::presolveTime")
{
StatisticsRegistry::registerStat(&d_statUserVariables);
StatisticsRegistry::registerStat(&d_statSlackVariables);
StatisticsRegistry::registerStat(&d_statDisequalitySplits);
StatisticsRegistry::registerStat(&d_statDisequalityConflicts);
StatisticsRegistry::registerStat(&d_staticLearningTimer);
+
+ StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
+ StatisticsRegistry::registerStat(&d_presolveTime);
}
TheoryArith::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_statDisequalitySplits);
StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts);
StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
+
+ StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
+ StatisticsRegistry::unregisterStat(&d_presolveTime);
}
void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1];
if((t == cright) && (e == cleft)){
- TNode tmp = t;
- t = e;
- e = tmp;
- k = reverseRelationKind(k);
+ TNode tmp = t;
+ t = e;
+ e = tmp;
+ k = reverseRelationKind(k);
}
if(t == cleft && e == cright){
- // t == cleft && e == cright
- Assert( t == cleft );
- Assert( e == cright );
- switch(k){
- case LT: // (ite (< x y) x y)
- case LEQ: { // (ite (<= x y) x y)
- Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
- Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
- Debug("arith::mins") << n << "is a min =>" << nLeqX << nLeqY << endl;
- learned << nLeqX << nLeqY;
- break;
- }
- case GT: // (ite (> x y) x y)
- case GEQ: { // (ite (>= x y) x y)
- Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
- Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
- Debug("arith::mins") << n << "is a max =>" << nGeqX << nGeqY << endl;
- learned << nGeqX << nGeqY;
- break;
- }
- default: Unreachable();
- }
+ // t == cleft && e == cright
+ Assert( t == cleft );
+ Assert( e == cright );
+ switch(k){
+ case LT: // (ite (< x y) x y)
+ case LEQ: { // (ite (<= x y) x y)
+ Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
+ Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
+ Debug("arith::mins") << n << "is a min =>" << nLeqX << nLeqY << endl;
+ learned << nLeqX << nLeqY;
+ break;
+ }
+ case GT: // (ite (> x y) x y)
+ case GEQ: { // (ite (>= x y) x y)
+ Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
+ Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
+ Debug("arith::mins") << n << "is a max =>" << nGeqX << nGeqY << endl;
+ learned << nGeqX << nGeqY;
+ break;
+ }
+ default: Unreachable();
+ }
}
}
// == 2-CONSTANTS ==
Debug("arith::mins") << n << " is a constant sandwich" << nGeqMin << nLeqMax << endl;
learned << nGeqMin << nLeqMax;
}
-
- // // binary OR of binary ANDs of EQUALities
- // if(n.getKind() == kind::OR && n.getNumChildren() == 2 &&
- // n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 &&
- // n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 &&
- // (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) &&
- // (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) &&
- // (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) &&
- // (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) {
- // // now we have (a = b && c = d) || (e = f && g = h)
-
- // Debug("diamonds") << "has form of a diamond!" << endl;
-
- // TNode
- // a = n[0][0][0], b = n[0][0][1],
- // c = n[0][1][0], d = n[0][1][1],
- // e = n[1][0][0], f = n[1][0][1],
- // g = n[1][1][0], h = n[1][1][1];
-
- // // test that one of {a, b} = one of {c, d}, and make "b" the
- // // shared node (i.e. put in the form (a = b && b = d))
- // // note we don't actually care about the shared ones, so the
- // // "swaps" below are one-sided, ignoring b and c
- // if(a == c) {
- // a = b;
- // } else if(a == d) {
- // a = b;
- // d = c;
- // } else if(b == c) {
- // // nothing to do
- // } else if(b == d) {
- // d = c;
- // } else {
- // // condition not satisfied
- // Debug("diamonds") << "+ A fails" << endl;
- // continue;
- // }
-
- // Debug("diamonds") << "+ A holds" << endl;
-
- // // same: one of {e, f} = one of {g, h}, and make "f" the
- // // shared node (i.e. put in the form (e = f && f = h))
- // if(e == g) {
- // e = f;
- // } else if(e == h) {
- // e = f;
- // h = g;
- // } else if(f == g) {
- // // nothing to do
- // } else if(f == h) {
- // h = g;
- // } else {
- // // condition not satisfied
- // Debug("diamonds") << "+ B fails" << endl;
- // continue;
- // }
-
- // Debug("diamonds") << "+ B holds" << endl;
-
- // // now we have (a = b && b = d) || (e = f && f = h)
- // // test that {a, d} == {e, h}
- // if( (a == e && d == h) ||
- // (a == h && d == e) ) {
- // // learn: n implies a == d
- // Debug("diamonds") << "+ C holds" << endl;
- // Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d);
- // Debug("diamonds") << " ==> " << newEquality << endl;
- // learned << n.impNode(newEquality);
- // } else {
- // Debug("diamonds") << "+ C fails" << endl;
- // }
- // }
}
}
-ArithVar TheoryArith::findBasicRow(ArithVar variable){
+ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){
+ ArithVar bestBasic = ARITHVAR_SENTINEL;
+ unsigned rowLength = 0;
+
for(ArithVarSet::iterator basicIter = d_tableau.begin();
basicIter != d_tableau.end();
++basicIter){
ReducedRowVector* row_j = d_tableau.lookup(x_j);
if(row_j->has(variable)){
- return x_j;
+ if((bestBasic == ARITHVAR_SENTINEL) ||
+ (bestBasic != ARITHVAR_SENTINEL && row_j->size() < rowLength)){
+ bestBasic = x_j;
+ rowLength = row_j->size();
+ }
}
}
- return ARITHVAR_SENTINEL;
+ return bestBasic;
}
d_out->setIncomplete();
}
- if(isLeaf(n) || isStrictlyVarList){
+ if(Variable::isMember(n) || isStrictlyVarList){
++(d_statistics.d_statUserVariables);
ArithVar varN = requestArithVar(n,false);
setupInitialValue(varN);
d_activityMonitor.push_back(0);
d_basicManager.init(varX,basic);
+ d_userVariables.init(varX, !basic);
d_tableau.increaseSize();
Debug("arith::arithvar") << x << " |-> " << varX << endl;
void TheoryArith::notifyEq(TNode lhs, TNode rhs) {
}
+
+bool TheoryArith::entireStateIsConsistent(){
+ typedef std::vector<Node>::const_iterator VarIter;
+ for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
+ ArithVar var = asArithVar(*i);
+ if(!d_partialModel.assignmentIsConsistent(var)){
+ d_partialModel.printModel(var);
+ cerr << "Assignment is not consistent for " << var << *i << endl;
+ return false;
+ }
+ }
+ return true;
+}
+
+void TheoryArith::permanentlyRemoveVariable(ArithVar v){
+ //There are 3 cases
+ // 1) v is non-basic and is contained in a row
+ // 2) v is basic
+ // 3) v is non-basic and is not contained in a row
+ // It appears that this can happen after other variables have been removed!
+ // Tread carefullty with this one.
+
+ if(!d_basicManager.isMember(v)){
+ ArithVar basic = findShortestBasicRow(v);
+
+ if(basic == ARITHVAR_SENTINEL){
+ //Case 3) do nothing else.
+ //TODO think hard about if this is okay...
+ return;
+ }
+
+ AlwaysAssert(basic != ARITHVAR_SENTINEL);
+ d_tableau.pivot(basic, v);
+ }
+
+ Assert(d_basicManager.isMember(v));
+
+ d_tableau.ejectBasic(v);
+ //remove the row from the tableau
+ //TODO: It would be better to remove the row from the tableau
+ //and store this row in another data structure
+
+
+ Debug("arith::permanentlyRemoveVariable") << v << " died an ignoble death."<< endl;
+ ++(d_statistics.d_permanentlyRemovedVariables);
+}
+
+void TheoryArith::presolve(){
+ TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
+
+ typedef std::vector<Node>::const_iterator VarIter;
+ for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
+ Node variableNode = *i;
+ ArithVar var = asArithVar(variableNode);
+ if(d_userVariables.isMember(var) && !d_propagator.hasAnyAtoms(variableNode)){
+ //The user variable is unconstrained.
+ //Remove this variable permanently
+ permanentlyRemoveVariable(var);
+ }
+ }
+
+ //Assert(entireStateIsConsistent()); //Boy is this paranoid
+ if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+
+ static int callCount = 0;
+ Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
+ check(FULL_EFFORT);
+}
#include "expr/node.h"
#include "theory/arith/arith_utilities.h"
-#include "theory/arith/arithvar_dense_set.h"
+#include "theory/arith/arithvar_set.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/tableau.h"
#include "theory/arith/arith_rewriter.h"
#include "util/stats.h"
#include <vector>
+#include <map>
#include <queue>
namespace CVC4 {
std::vector<Node> d_variables;
+ std::map<ArithVar, ReducedRowVector*> d_removedRows;
+
/**
* Priority Queue of the basic variables that may be inconsistent.
*
*/
ArithPartialModel d_partialModel;
- ArithVarDenseSet d_basicManager;
+ ArithVarSet d_basicManager;
+ ArithVarSet d_userVariables;
ActivityMonitor d_activityMonitor;
/**
void shutdown(){ }
- void presolve(){
- static int callCount = 0;
- Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
- check(FULL_EFFORT);
- }
+ void presolve();
void staticLearning(TNode in, NodeBuilder<>& learned);
void setupSlack(TNode left);
-
-
/**
* Handles the case splitting for check() for a new assertion.
* returns true if their is a conflict.
*/
bool assertionCases(TNode assertion);
- ArithVar findBasicRow(ArithVar variable);
+ /**
+ * Returns the basic variable with the shorted row containg a non-basic variable.
+ * If no such row exists, return ARITHVAR_SENTINEL.
+ */
+ ArithVar findShortestBasicRow(ArithVar variable);
+
+ /**
+ * Debugging only routine!
+ * Returns true iff every variable is consistent in the partial model.
+ */
+ bool entireStateIsConsistent();
+
+ /**
+ * Permanently removes a variable from the problem.
+ * The caller guarentees the saftey of this removal!
+ */
+ void permanentlyRemoveVariable(ArithVar v);
+
void asVectors(Polynomial& p,
std::vector<Rational>& coeffs,
IntStat d_statDisequalityConflicts;
TimerStat d_staticLearningTimer;
+ IntStat d_permanentlyRemovedVariables;
+ TimerStat d_presolveTime;
Statistics();
~Statistics();
};
return left.hasAttribute(PropagatorEqSet());
}
+bool ArithUnatePropagator::hasAnyAtoms(TNode v){
+ Assert(!leftIsSetup(v)
+ || !v.getAttribute(PropagatorEqSet())->empty()
+ || !v.getAttribute(PropagatorLeqSet())->empty()
+ || !v.getAttribute(PropagatorGeqSet())->empty());
+
+ return leftIsSetup(v);
+}
+
void ArithUnatePropagator::setupLefthand(TNode left){
Assert(!leftIsSetup(left));
*/
void addAtom(TNode atom);
+ /** Returns true if v has been added as a left hand side in an atom */
+ bool hasAnyAtoms(TNode v);
+
private:
/** Sends an implication (=> a b) to the PropEngine via d_arithOut. */
void addImplication(TNode a, TNode b);
projects / cvc5.git / commitdiff