}
void clear() throw(AssertionException) {
- Debug("gc") << "clearing cdmap " << this << std::endl;
-
- Debug("gc") << "cdmap " << this << " cleared, emptying trash" << std::endl;
+ Debug("gc") << "clearing cdmap " << this << ", emptying trash" << std::endl;
emptyTrash();
Debug("gc") << "done emptying trash for " << this << std::endl;
- for(typename table_type::iterator i = d_map.begin();
- i != d_map.end();
- ++i) {
+ for(Element* i = d_first; i != NULL;) {
// mark it as being a destruction (short-circuit restore())
- (*i).second->d_map = NULL;
- if(!(*i).second->d_noTrash) {
- (*i).second->deleteSelf();
+ Element* thisOne = i;
+ i = i->next();
+ thisOne->d_map = NULL;
+ if(!thisOne->d_noTrash) {
+ thisOne->deleteSelf();
}
}
d_map.clear();
basic.h \
slack.h \
tableau.h \
+ tableau.cpp \
arith_propagator.h \
arith_propagator.cpp \
theory_arith.h \
namespace arith {
-struct ArithActivityID {};
-typedef expr::Attribute<ArithActivityID, uint64_t> ArithActivity;
-
-inline void resetActivity(TNode var){
- var.setAttribute(ArithActivity(), 0);
-}
-inline void initActivity(TNode var){
- resetActivity(var);
-}
-
-inline uint64_t getActivity(TNode var){
- return var.getAttribute(ArithActivity());
-}
-
-inline void increaseActivity(TNode var, uint64_t x){
- Assert(var.hasAttribute(ArithActivity()));
- uint64_t newValue = x + getActivity(var);
- var.setAttribute(ArithActivity(), newValue);
-}
-
-const static uint64_t ACTIVITY_THRESHOLD = 100;
+class ActivityMonitor {
+private:
+ std::vector<uint64_t> d_activities;
+
+public:
+ const static uint64_t ACTIVITY_THRESHOLD = 100;
+
+ ActivityMonitor() : d_activities() {}
+
+ void resetActivity(ArithVar var){
+ d_activities[var] = 0;
+ }
+
+ void initActivity(ArithVar var){
+ Assert(var == d_activities.size());
+ d_activities.push_back(0);
+ }
+
+ uint64_t getActivity(ArithVar var) const{
+ return d_activities[var];
+ }
+
+ inline void increaseActivity(ArithVar var, uint64_t x){
+ d_activities[var] += x;
+ }
+
+};
+
}; /* namesapce arith */
}; /* namespace theory */
#include "util/rational.h"
#include "expr/node.h"
+#include "expr/attribute.h"
+#include <stdint.h>
+#include <limits>
namespace CVC4 {
namespace theory {
namespace arith {
+
+typedef uint64_t ArithVar;
+//static const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
+#define ARITHVAR_SENTINEL std::numeric_limits<ArithVar>::max()
+
+struct ArithVarAttrID{};
+typedef expr::Attribute<ArithVarAttrID,ArithVar> ArithVarAttr;
+
+inline ArithVar asArithVar(TNode x){
+ Assert(x.hasAttribute(ArithVarAttr()));
+ return x.getAttribute(ArithVarAttr());
+}
+
inline Node mkRationalNode(const Rational& q){
return NodeManager::currentNM()->mkConst<Rational>(q);
}
namespace theory {
namespace arith {
-struct IsBasicAttrID;
-
-typedef expr::Attribute<IsBasicAttrID, bool> IsBasic;
-
-
-inline bool isBasic(TNode x){
- return x.getAttribute(IsBasic());
-}
-
-inline void makeBasic(TNode x){
- return x.setAttribute(IsBasic(), true);
-}
-
-inline void makeNonbasic(TNode x){
- return x.setAttribute(IsBasic(), false);
-}
+class IsBasicManager {
+private:
+ std::vector<bool> d_basic;
+
+public:
+ IsBasicManager() : d_basic() {}
+
+ void init(ArithVar var, bool value){
+ Assert(var == d_basic.size());
+ d_basic.push_back(value);
+ }
+
+ bool isBasic(ArithVar x) const{
+ return d_basic[x];
+ }
+
+ void makeBasic(ArithVar x){
+ Assert(!isBasic(x));
+ d_basic[x] = true;
+ }
+
+ void makeNonbasic(ArithVar x){
+ Assert(isBasic(x));
+ d_basic[x] = false;
+ }
+};
}; /* namespace arith */
}; /* namespace theory */
Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Constant& right) {
Assert(isRelationOperator(k));
if(left.isConstant()) {
- const Rational& rConst = left.getNode().getConst<Rational>();
- const Rational& lConst = right.getNode().getConst<Rational>();
+ const Rational& lConst = left.getNode().getConst<Rational>();
+ const Rational& rConst = right.getNode().getConst<Rational>();
bool res = evaluateConstantPredicate(k, lConst, rConst);
return Comparison(res);
} else {
using namespace CVC4::theory::arith;
using namespace CVC4::theory::arith::partial_model;
-void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& r){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+void ArithPartialModel::setUpperBound(ArithVar x, const DeltaRational& r){
+ //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl;
- x.setAttribute(partial_model::HasHadABound(), true);
+ //x.setAttribute(partial_model::HasHadABound(), true);
+ d_hasHadABound[x] = true;
- d_UpperBoundMap[x] = r;
+ d_upperBound.set(x,r);
}
-void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl;
- x.setAttribute(partial_model::HasHadABound(), true);
+void ArithPartialModel::setLowerBound(ArithVar x, const DeltaRational& r){
+ //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ // Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl;
+// x.setAttribute(partial_model::HasHadABound(), true);
- d_LowerBoundMap[x] = r;
+// d_LowerBoundMap[x] = r;
+ d_hasHadABound[x] = true;
+ d_lowerBound.set(x,r);
}
-void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- Assert(x.hasAttribute(partial_model::Assignment()));
- Assert(x.hasAttribute(partial_model::SafeAssignment()));
-
- DeltaRational* curr = x.getAttribute(partial_model::Assignment());
-
- DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
- if(saved == NULL){
- saved = new DeltaRational(*curr);
- x.setAttribute(partial_model::SafeAssignment(), saved);
+void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){
+ //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ //Assert(x.hasAttribute(partial_model::Assignment()));
+ //Assert(x.hasAttribute(partial_model::SafeAssignment()));
+
+// DeltaRational* curr = x.getAttribute(partial_model::Assignment());
+
+// DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
+// if(saved == NULL){
+// saved = new DeltaRational(*curr);
+// x.setAttribute(partial_model::SafeAssignment(), saved);
+// d_history.push_back(x);
+// }
+
+// *curr = r;
+ Debug("partial_model") << "pm: updating the assignment to" << x
+ << " now " << r <<endl;
+ if(!d_hasSafeAssignment[x]){
+ d_safeAssignment[x] = d_assignment[x];
+ d_hasSafeAssignment[x] = true;
d_history.push_back(x);
}
-
- *curr = r;
- Debug("partial_model") << "pm: updating the assignment to" << x
- << " now " << r <<endl;
+ d_assignment[x] = r;
}
-void ArithPartialModel::setAssignment(TNode x, const DeltaRational& safe, const DeltaRational& r){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- Assert(x.hasAttribute(partial_model::Assignment()));
- Assert(x.hasAttribute(partial_model::SafeAssignment()));
-
- DeltaRational* curr = x.getAttribute(partial_model::Assignment());
- DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
-
+void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
+ // Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+// Assert(x.hasAttribute(partial_model::Assignment()));
+// Assert(x.hasAttribute(partial_model::SafeAssignment()));
+
+// DeltaRational* curr = x.getAttribute(partial_model::Assignment());
+// DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
+
+
+
+// if(safe == r){
+// if(saved != NULL){
+// x.setAttribute(partial_model::SafeAssignment(), NULL);
+// delete saved;
+// }
+// }else{
+// if(saved == NULL){
+// saved = new DeltaRational(safe);
+// x.setAttribute(partial_model::SafeAssignment(), saved);
+// }else{
+// *saved = safe;
+// }
+// d_history.push_back(x);
+// }
+// *curr = r;
+
+ Debug("partial_model") << "pm: updating the assignment to" << x
+ << " now " << r <<endl;
if(safe == r){
- if(saved != NULL){
- x.setAttribute(partial_model::SafeAssignment(), NULL);
- delete saved;
- }
+ d_hasSafeAssignment[x] = false;
}else{
- if(saved == NULL){
- saved = new DeltaRational(safe);
- x.setAttribute(partial_model::SafeAssignment(), saved);
- }else{
- *saved = safe;
+ d_safeAssignment[x] = safe;
+
+ if(!d_hasSafeAssignment[x]){
+ d_hasSafeAssignment[x] = true;
+ d_history.push_back(x);
}
- d_history.push_back(x);
}
- *curr = r;
+ d_assignment[x] = r;
+}
- Debug("partial_model") << "pm: updating the assignment to" << x
- << " now " << r <<endl;
+bool ArithPartialModel::equalSizes(){
+ return d_mapSize == d_hasHadABound.size() &&
+ d_mapSize == d_hasSafeAssignment.size() &&
+ d_mapSize == d_assignment.size() &&
+ d_mapSize == d_safeAssignment.size() &&
+ d_mapSize == d_upperBound.size() &&
+ d_mapSize == d_lowerBound.size() &&
+ d_mapSize == d_upperConstraint.size() &&
+ d_mapSize == d_lowerConstraint.size();
}
-void ArithPartialModel::initialize(TNode x, const DeltaRational& r){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){
+// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+// Assert(!x.hasAttribute(partial_model::Assignment()));
+// Assert(!x.hasAttribute(partial_model::SafeAssignment()));
+
+// DeltaRational* c = new DeltaRational(r);
+// x.setAttribute(partial_model::Assignment(), c);
+// x.setAttribute(partial_model::SafeAssignment(), NULL);
+
+// Debug("partial_model") << "pm: constructing an assignment for " << x
+// << " initially " << (*c) <<endl;
- Assert(!x.hasAttribute(partial_model::Assignment()));
- Assert(!x.hasAttribute(partial_model::SafeAssignment()));
+ Assert(x == d_mapSize);
+ Assert(equalSizes());
+ ++d_mapSize;
- DeltaRational* c = new DeltaRational(r);
- x.setAttribute(partial_model::Assignment(), c);
- x.setAttribute(partial_model::SafeAssignment(), NULL);
- Debug("partial_model") << "pm: constructing an assignment for " << x
- << " initially " << (*c) <<endl;
+ d_hasHadABound.push_back( false );
+
+ d_hasSafeAssignment.push_back( false );
+ d_assignment.push_back( r );
+ d_safeAssignment.push_back( DeltaRational(0) );
+
+ d_upperBound.push_back( DeltaRational(0) );
+ d_lowerBound.push_back( DeltaRational(0) );
+
+ d_upperConstraint.push_back( TNode::null() );
+ d_lowerConstraint.push_back( TNode::null() );
}
/** Must know that the bound exists both calling this! */
-DeltaRational ArithPartialModel::getUpperBound(TNode x) const {
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) {
+ Assert(inMaps(x));
+ Assert(!d_upperConstraint[x].isNull());
- CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
- Assert(i != d_UpperBoundMap.end());
+ return d_upperBound[x];
- return DeltaRational((*i).second);
+// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+// CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+// Assert(i != d_UpperBoundMap.end());
+
+// return DeltaRational((*i).second);
}
-DeltaRational ArithPartialModel::getLowerBound(TNode x) const{
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) {
+ Assert(inMaps(x));
+ Assert(!d_lowerConstraint[x].isNull());
- CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
- Assert(i != d_LowerBoundMap.end());
+ return d_lowerBound[x];
- return DeltaRational((*i).second);
-}
+// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-DeltaRational ArithPartialModel::getSafeAssignment(TNode x) const{
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- Assert( x.hasAttribute(SafeAssignment()));
+// CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+// Assert(i != d_LowerBoundMap.end());
- DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
- if(safeAssignment != NULL){
- return *safeAssignment;
+// return DeltaRational((*i).second);
+}
+
+const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{
+ Assert(inMaps(x));
+ if(d_hasSafeAssignment[x]){
+ return d_safeAssignment[x];
}else{
- return getAssignment(x); //The current assignment is safe.
+ return d_assignment[x];
}
+// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+// Assert( x.hasAttribute(SafeAssignment()));
+
+// DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
+// if(safeAssignment != NULL){
+// return *safeAssignment;
+// }else{
+// return getAssignment(x); //The current assignment is safe.
+// }
}
-const DeltaRational& ArithPartialModel::getAssignment(TNode x) const{
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+const DeltaRational& ArithPartialModel::getAssignment(ArithVar x) const{
+// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
- return *assign;
+// DeltaRational* assign;
+// AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+// return *assign;
+ Assert(inMaps(x));
+ return d_assignment[x];
}
-void ArithPartialModel::setLowerConstraint(TNode x, TNode constraint){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+void ArithPartialModel::setLowerConstraint(ArithVar x, TNode constraint){
+// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
Debug("partial_model") << "setLowerConstraint("
<< x << ":" << constraint << ")" << endl;
- x.setAttribute(partial_model::LowerConstraint(),constraint);
-}
+// x.setAttribute(partial_model::LowerConstraint(),constraint);
-void ArithPartialModel::setUpperConstraint(TNode x, TNode constraint){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ Assert(inMaps(x));
+ d_lowerConstraint.set(x,constraint);
- Debug("partial_model") << "setUpperConstraint("
- << x << ":" << constraint << ")" << endl;
-
- x.setAttribute(partial_model::UpperConstraint(),constraint);
}
-TNode ArithPartialModel::getLowerConstraint(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
- TNode ret;
- AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
- return ret;
-}
+void ArithPartialModel::setUpperConstraint(ArithVar x, TNode constraint){
+// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-TNode ArithPartialModel::getUpperConstraint(TNode x){
- Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+ Debug("partial_model") << "setUpperConstraint("
+ << x << ":" << constraint << ")" << endl;
- TNode ret;
- AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
- return ret;
+// x.setAttribute(partial_model::UpperConstraint(),constraint);
+ Assert(inMaps(x));
+ d_upperConstraint.set(x, constraint);
}
-// TNode CVC4::theory::arith::getLowerConstraint(TNode x){
+TNode ArithPartialModel::getLowerConstraint(ArithVar x){
// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
// TNode ret;
// AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
// return ret;
-// }
-// TNode CVC4::theory::arith::getUpperConstraint(TNode x){
+ Assert(inMaps(x));
+ Assert(!d_lowerConstraint[x].isNull());
+ return d_lowerConstraint[x];
+}
+
+TNode ArithPartialModel::getUpperConstraint(ArithVar x){
// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
// TNode ret;
// AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
// return ret;
-// }
+ Assert(inMaps(x));
+ Assert(!d_upperConstraint[x].isNull());
+ return d_upperConstraint[x];
+}
-bool ArithPartialModel::belowLowerBound(TNode x, const DeltaRational& c, bool strict){
- CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
- if(i == d_LowerBoundMap.end()){
+
+bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){
+ if(d_lowerConstraint[x].isNull()){
// l = -\intfy
// ? c < -\infty |- _|_
return false;
}
-
- const DeltaRational& l = (*i).second;
-
if(strict){
- return c < l;
+ return c < d_lowerBound[x];
}else{
- return c <= l;
+ return c <= d_lowerBound[x];
}
+// CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+// if(i == d_LowerBoundMap.end()){
+// // l = -\intfy
+// // ? c < -\infty |- _|_
+// return false;
+// }
+
+// const DeltaRational& l = (*i).second;
+
+// if(strict){
+// return c < l;
+// }else{
+// return c <= l;
+// }
}
-bool ArithPartialModel::aboveUpperBound(TNode x, const DeltaRational& c, bool strict){
- CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
- if(i == d_UpperBoundMap.end()){
- // u = -\intfy
- // ? u < -\infty |- _|_
+bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
+ if(d_upperConstraint[x].isNull()){
+ // u = \intfy
+ // ? c > \infty |- _|_
return false;
}
- const DeltaRational& u = (*i).second;
-
if(strict){
- return c > u;
+ return c > d_upperBound[x];
}else{
- return c >= u;
+ return c >= d_upperBound[x];
}
+// CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+// if(i == d_UpperBoundMap.end()){
+// // u = -\intfy
+// // ? u < -\infty |- _|_
+// return false;
+// }
+// const DeltaRational& u = (*i).second;
+
+// if(strict){
+// return c > u;
+// }else{
+// return c >= u;
+// }
}
-bool ArithPartialModel::hasBounds(TNode x){
+bool ArithPartialModel::hasBounds(ArithVar x){
return
- d_UpperBoundMap.find(x) != d_UpperBoundMap.end() ||
- d_LowerBoundMap.find(x) != d_LowerBoundMap.end();
+ !d_lowerConstraint[x].isNull() || !d_upperConstraint[x].isNull();
+ // return
+// d_UpperBoundMap.find(x) != d_UpperBoundMap.end() ||
+// d_LowerBoundMap.find(x) != d_LowerBoundMap.end();
}
-bool ArithPartialModel::strictlyBelowUpperBound(TNode x){
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
-
- CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
- if(i == d_UpperBoundMap.end()){// u = \infty
+bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){
+ Assert(inMaps(x));
+ if(d_upperConstraint[x].isNull()){ // u = \infty
return true;
}
+ return d_assignment[x] < d_upperBound[x];
+// DeltaRational* assign;
+// AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
- const DeltaRational& u = (*i).second;
- return (*assign) < u;
-}
+// CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+// if(i == d_UpperBoundMap.end()){// u = \infty
+// return true;
+// }
-bool ArithPartialModel::strictlyAboveLowerBound(TNode x){
- DeltaRational* assign;
- AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+// const DeltaRational& u = (*i).second;
+// return (*assign) < u;
+}
- CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
- if(i == d_LowerBoundMap.end()){// l = \infty
+bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){
+ Assert(inMaps(x));
+ if(d_lowerConstraint[x].isNull()){ // l = -\infty
return true;
}
+ return d_lowerBound[x] < d_assignment[x];
+
+// DeltaRational* assign;
+// AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
- const DeltaRational& l = (*i).second;
- return l < *assign;
+// CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+// if(i == d_LowerBoundMap.end()){// l = \infty
+// return true;
+// }
+
+// const DeltaRational& l = (*i).second;
+// return l < *assign;
}
-bool ArithPartialModel::assignmentIsConsistent(TNode x){
+bool ArithPartialModel::assignmentIsConsistent(ArithVar x){
const DeltaRational& beta = getAssignment(x);
- bool above_li = !belowLowerBound(x,beta,true);
- bool below_ui = !aboveUpperBound(x,beta,true);
-
//l_i <= beta(x_i) <= u_i
- return above_li && below_ui;
+ return !belowLowerBound(x,beta,true) && !aboveUpperBound(x,beta,true);
}
void ArithPartialModel::clearSafeAssignments(bool revert){
for(HistoryList::iterator i = d_history.begin(); i != d_history.end(); ++i){
- TNode x = *i;
-
- Assert(x.hasAttribute(SafeAssignment()));
- Assert(x.hasAttribute(Assignment()));
-
- DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
+ ArithVar x = *i;
+ Assert(d_hasSafeAssignment[x]);
+ d_hasSafeAssignment[x] = false;
if(revert){
- DeltaRational* assign = x.getAttribute(Assignment());
- *assign = *safeAssignment;
+ d_assignment[x] = d_safeAssignment[x];
}
- x.setAttribute(partial_model::SafeAssignment(), NULL);
- delete safeAssignment;
+// Assert(x.hasAttribute(SafeAssignment()));
+// Assert(x.hasAttribute(Assignment()));
+
+// DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
+
+// if(revert){
+// DeltaRational* assign = x.getAttribute(Assignment());
+// *assign = *safeAssignment;
+// }
+// x.setAttribute(partial_model::SafeAssignment(), NULL);
+// delete safeAssignment;
}
d_history.clear();
clearSafeAssignments(false);
}
-void ArithPartialModel::printModel(TNode x){
-
+void ArithPartialModel::printModel(ArithVar x){
Debug("model") << "model" << x << ":"<< getAssignment(x) << " ";
-
- CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
- if(i != d_LowerBoundMap.end()){
- DeltaRational l = (*i).second;
- Debug("model") << l << " ";
- Debug("model") << getLowerConstraint(x) << " ";
- }else{
+ if(d_lowerConstraint[x].isNull()){
Debug("model") << "no lb ";
- }
-
- i = d_UpperBoundMap.find(x);
- if(i != d_UpperBoundMap.end()){
- DeltaRational u = (*i).second;
- Debug("model") << u << " ";
- Debug("model") << getUpperConstraint(x) << " ";
}else{
+ Debug("model") << getLowerBound(x) << " ";
+ Debug("model") << getLowerConstraint(x) << " ";
+ }
+ if(d_upperConstraint[x].isNull()){
Debug("model") << "no ub ";
+ }else{
+ Debug("model") << getUpperBound(x) << " ";
+ Debug("model") << getUpperConstraint(x) << " ";
}
- Debug("model") << endl;
+// Debug("model") << "model" << x << ":"<< getAssignment(x) << " ";
+
+// CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+// if(i != d_LowerBoundMap.end()){
+// DeltaRational l = (*i).second;
+// Debug("model") << l << " ";
+// Debug("model") << getLowerConstraint(x) << " ";
+// }else{
+// Debug("model") << "no lb ";
+// }
+
+// i = d_UpperBoundMap.find(x);
+// if(i != d_UpperBoundMap.end()){
+// DeltaRational u = (*i).second;
+// Debug("model") << u << " ";
+// Debug("model") << getUpperConstraint(x) << " ";
+// }else{
+// Debug("model") << "no ub ";
+// }
+// Debug("model") << endl;
}
#include "context/context.h"
-#include "context/cdmap.h"
+#include "context/cdvector.h"
+#include "theory/arith/arith_utilities.h"
#include "theory/arith/delta_rational.h"
#include "expr/attribute.h"
#include "expr/node.h"
namespace arith {
namespace partial_model {
-struct DeltaRationalCleanupStrategy{
- static void cleanup(DeltaRational* dq){
- Debug("arithgc") << "cleaning up " << dq << "\n";
- if(dq != NULL){
- delete dq;
- }
- }
-};
+// struct DeltaRationalCleanupStrategy{
+// static void cleanup(DeltaRational* dq){
+// Debug("arithgc") << "cleaning up " << dq << "\n";
+// if(dq != NULL){
+// delete dq;
+// }
+// }
+// };
+
+
+// struct AssignmentAttrID {};
+// typedef expr::Attribute<AssignmentAttrID,
+// DeltaRational*,
+// DeltaRationalCleanupStrategy> Assignment;
-struct AssignmentAttrID {};
-typedef expr::Attribute<AssignmentAttrID,
- DeltaRational*,
- DeltaRationalCleanupStrategy> Assignment;
+
+// struct SafeAssignmentAttrID {};
+// typedef expr::Attribute<SafeAssignmentAttrID,
+// DeltaRational*,
+// DeltaRationalCleanupStrategy> SafeAssignment;
-struct SafeAssignmentAttrID {};
-typedef expr::Attribute<SafeAssignmentAttrID,
- DeltaRational*,
- DeltaRationalCleanupStrategy> SafeAssignment;
/**
* This defines a context dependent delta rational map.
* This is used to keep track of the current lower and upper bounds on
* each variable. This information is conext dependent.
*/
-typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap;
+//typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap;
/* Side disucssion for why new tables are introduced instead of using the
* attribute framework.
* It comes down to that the obvious ways to use the current attribute
* Note the strong correspondence between this and LowerBoundMap.
* This is used during conflict analysis.
*/
-struct LowerConstraintAttrID {};
-typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint;
+// struct LowerConstraintAttrID {};
+// typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint;
/**
* See the documentation for LowerConstraint.
*/
-struct UpperConstraintAttrID {};
-typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint;
+// struct UpperConstraintAttrID {};
+// typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint;
-struct TheoryArithPropagatedID {};
-typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
+// struct TheoryArithPropagatedID {};
+// typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
-struct HasHadABoundID {};
-typedef expr::Attribute<HasHadABoundID, bool> HasHadABound;
+// struct HasHadABoundID {};
+// typedef expr::Attribute<HasHadABoundID, bool> HasHadABound;
}; /*namespace partial_model*/
class ArithPartialModel {
private:
- partial_model::CDDRationalMap d_LowerBoundMap;
- partial_model::CDDRationalMap d_UpperBoundMap;
+
+ unsigned d_mapSize;
+ //Maps from ArithVar -> T
+
+ std::vector<bool> d_hasHadABound;
+
+ std::vector<bool> d_hasSafeAssignment;
+ std::vector<DeltaRational> d_assignment;
+ std::vector<DeltaRational> d_safeAssignment;
+
+ context::CDVector<DeltaRational> d_upperBound;
+ context::CDVector<DeltaRational> d_lowerBound;
+ context::CDVector<TNode> d_upperConstraint;
+ context::CDVector<TNode> d_lowerConstraint;
/**
* List contains all of the variables that have an unsafe assignment.
*/
- typedef std::vector<TNode> HistoryList;
+ typedef std::vector<ArithVar> HistoryList;
HistoryList d_history;
public:
ArithPartialModel(context::Context* c):
- d_LowerBoundMap(c),
- d_UpperBoundMap(c),
+ d_mapSize(0),
+ d_hasHadABound(),
+ d_hasSafeAssignment(),
+ d_assignment(),
+ d_safeAssignment(),
+ d_upperBound(c, false),
+ d_lowerBound(c, false),
+ d_upperConstraint(c,false),
+ d_lowerConstraint(c,false),
d_history()
{ }
- void setLowerConstraint(TNode x, TNode constraint);
- void setUpperConstraint(TNode x, TNode constraint);
- TNode getLowerConstraint(TNode x);
- TNode getUpperConstraint(TNode x);
+ void setLowerConstraint(ArithVar x, TNode constraint);
+ void setUpperConstraint(ArithVar x, TNode constraint);
+ TNode getLowerConstraint(ArithVar x);
+ TNode getUpperConstraint(ArithVar x);
/* Initializes a variable to a safe value.*/
- void initialize(TNode x, const DeltaRational& r);
+ void initialize(ArithVar x, const DeltaRational& r);
/* Gets the last assignment to a variable that is known to be conistent. */
- DeltaRational getSafeAssignment(TNode x) const;
+ const DeltaRational& getSafeAssignment(ArithVar x) const;
/* Reverts all variable assignments to their safe values. */
void revertAssignmentChanges();
- void setUpperBound(TNode x, const DeltaRational& r);
- void setLowerBound(TNode x, const DeltaRational& r);
+ void setUpperBound(ArithVar x, const DeltaRational& r);
+ void setLowerBound(ArithVar x, const DeltaRational& r);
/* Sets an unsafe variable assignment */
- void setAssignment(TNode x, const DeltaRational& r);
- void setAssignment(TNode x, const DeltaRational& safe, const DeltaRational& r);
+ void setAssignment(ArithVar x, const DeltaRational& r);
+ void setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r);
/** Must know that the bound exists before calling this! */
- DeltaRational getUpperBound(TNode x) const;
- DeltaRational getLowerBound(TNode x) const;
- const DeltaRational& getAssignment(TNode x) const;
+ const DeltaRational& getUpperBound(ArithVar x);
+ const DeltaRational& getLowerBound(ArithVar x);
+ const DeltaRational& getAssignment(ArithVar x) const;
/**
* x <= l
* ? c < l
*/
- bool belowLowerBound(TNode x, const DeltaRational& c, bool strict);
+ bool belowLowerBound(ArithVar x, const DeltaRational& c, bool strict);
/**
* x <= u
* ? c < u
*/
- bool aboveUpperBound(TNode x, const DeltaRational& c, bool strict);
+ bool aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict);
- bool strictlyBelowUpperBound(TNode x);
- bool strictlyAboveLowerBound(TNode x);
- bool assignmentIsConsistent(TNode x);
+ bool strictlyBelowUpperBound(ArithVar x);
+ bool strictlyAboveLowerBound(ArithVar x);
+ bool assignmentIsConsistent(ArithVar x);
- void printModel(TNode x);
+ void printModel(ArithVar x);
- bool hasBounds(TNode x);
- bool hasEverHadABound(TNode var){
- return var.getAttribute(partial_model::HasHadABound());
+ bool hasBounds(ArithVar x);
+
+ bool hasEverHadABound(ArithVar var){
+ return d_hasHadABound[var];
}
private:
* revertAssignmentChanges() and commitAssignmentChanges().
*/
void clearSafeAssignments(bool revert);
+
+ bool equalSizes();
+
+ bool inMaps(ArithVar x) const{
+ return 0 <= x && x < d_mapSize;
+ }
+
};
--- /dev/null
+
+#include "theory/arith/tableau.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+Row::Row(ArithVar basic,
+ const std::vector< Rational >& coefficients,
+ const std::vector< ArithVar >& variables):
+ d_x_i(basic),
+ d_coeffs(){
+
+ Assert(coefficients.size() == variables.size() );
+
+ std::vector<Rational>::const_iterator coeffIter = coefficients.begin();
+ std::vector<Rational>::const_iterator coeffEnd = coefficients.end();
+ std::vector<ArithVar>::const_iterator varIter = variables.begin();
+
+ for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){
+ const Rational& coeff = *coeffIter;
+ ArithVar var_i = *varIter;
+
+ Assert(var_i != d_x_i);
+ Assert(!has(var_i));
+ Assert(coeff != Rational(0,1));
+
+ d_coeffs[var_i] = coeff;
+ Assert(d_coeffs[var_i] != Rational(0,1));
+ }
+}
+
+void Row::subsitute(Row& row_s){
+ ArithVar x_s = row_s.basicVar();
+
+ Assert(has(x_s));
+ Assert(x_s != d_x_i);
+
+ Rational zero(0,1);
+
+ Rational a_rs = lookup(x_s);
+ Assert(a_rs != zero);
+ d_coeffs.erase(x_s);
+
+ for(iterator iter = row_s.begin(), iter_end = row_s.end();
+ iter != iter_end; ++iter){
+ ArithVar x_j = iter->first;
+ Rational a_sj = iter->second;
+ a_sj *= a_rs;
+ CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j);
+
+ if(coeff_iter != d_coeffs.end()){
+ coeff_iter->second += a_sj;
+ if(coeff_iter->second == zero){
+ d_coeffs.erase(coeff_iter);
+ }
+ }else{
+ d_coeffs.insert(std::make_pair(x_j,a_sj));
+ }
+ }
+}
+
+void Row::pivot(ArithVar x_j){
+ Rational negInverseA_rs = -(lookup(x_j).inverse());
+ d_coeffs[d_x_i] = Rational(Integer(-1));
+ d_coeffs.erase(x_j);
+
+ d_x_i = x_j;
+
+ for(iterator nonbasicIter = begin(), nonbasicIter_end = end();
+ nonbasicIter != nonbasicIter_end; ++nonbasicIter){
+ nonbasicIter->second *= negInverseA_rs;
+ }
+
+}
+
+void Row::printRow(){
+ Debug("tableau") << d_x_i << " ";
+ for(iterator nonbasicIter = d_coeffs.begin();
+ nonbasicIter != d_coeffs.end();
+ ++nonbasicIter){
+ ArithVar nb = nonbasicIter->first;
+ Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}";
+ }
+ Debug("tableau") << std::endl;
+}
+
+void Tableau::addRow(ArithVar basicVar,
+ const std::vector<Rational>& coeffs,
+ const std::vector<ArithVar>& variables){
+
+ Assert(coeffs.size() == variables.size());
+ Assert(d_basicManager.isBasic(basicVar));
+
+ //The new basic variable cannot already be a basic variable
+ Assert(!isActiveBasicVariable(basicVar));
+ d_activeBasicVars.insert(basicVar);
+ Row* row_current = new Row(basicVar,coeffs,variables);
+ d_activeRows[basicVar] = row_current;
+
+ //A variable in the row may have been made non-basic already.
+ //If this is the case we fake pivoting this variable
+ std::vector<Rational>::const_iterator coeffsIter = coeffs.begin();
+ std::vector<Rational>::const_iterator coeffsEnd = coeffs.end();
+
+ std::vector<ArithVar>::const_iterator varsIter = variables.begin();
+
+ for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){
+ ArithVar var = *varsIter;
+
+ if(d_basicManager.isBasic(var)){
+ if(!isActiveBasicVariable(var)){
+ reinjectBasic(var);
+ }
+ Assert(isActiveBasicVariable(var));
+
+ Row* row_var = lookup(var);
+ row_current->subsitute(*row_var);
+ }
+ }
+}
+
+void Tableau::pivot(ArithVar x_r, ArithVar x_s){
+ Assert(d_basicManager.isBasic(x_r));
+ Assert(!d_basicManager.isBasic(x_s));
+
+ RowsTable::iterator ptrRow_r = d_activeRows.find(x_r);
+ Assert(ptrRow_r != d_activeRows.end());
+
+ Row* row_s = (*ptrRow_r).second;
+
+ Assert(row_s->has(x_s));
+ row_s->pivot(x_s);
+
+ d_activeRows.erase(ptrRow_r);
+ d_activeBasicVars.erase(x_r);
+ d_basicManager.makeNonbasic(x_r);
+
+ d_activeRows.insert(std::make_pair(x_s,row_s));
+ d_activeBasicVars.insert(x_s);
+ d_basicManager.makeBasic(x_s);
+
+ for(VarSet::iterator basicIter = begin(), endIter = end();
+ basicIter != endIter; ++basicIter){
+ ArithVar basic = *basicIter;
+ Row* row_k = lookup(basic);
+ if(row_k->has(x_s)){
+ d_activityMonitor.increaseActivity(basic, 30);
+ row_k->subsitute(*row_s);
+ }
+ }
+}
+
+void Tableau::printTableau(){
+ for(VarSet::iterator basicIter = begin(), endIter = end();
+ basicIter != endIter; ++basicIter){
+ ArithVar basic = *basicIter;
+ Row* row_k = lookup(basic);
+ row_k->printRow();
+ }
+ for(RowsTable::iterator basicIter = d_inactiveRows.begin(), endIter = d_inactiveRows.end();
+ basicIter != endIter; ++basicIter){
+ ArithVar basic = (*basicIter).first;
+ Row* row_k = lookupEjected(basic);
+ row_k->printRow();
+ }
+}
+
+
+void Tableau::updateRow(Row* row){
+ for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){
+ ArithVar var = i->first;
+ ++i;
+ if(d_basicManager.isBasic(var)){
+ Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
+
+ Assert(row_var != row);
+ row->subsitute(*row_var);
+
+ i = row->begin();
+ endIter = row->end();
+ }
+ }
+}
#include "expr/node.h"
#include "expr/attribute.h"
-#include "theory/arith/basic.h"
+#include "theory/arith/arith_utilities.h"
#include "theory/arith/arith_activity.h"
+#include "theory/arith/basic.h"
#include "theory/arith/normal_form.h"
#include <ext/hash_map>
class Row {
- TNode d_x_i;
+ ArithVar d_x_i;
- typedef std::map<TNode, Rational> CoefficientTable;
+ typedef std::map<ArithVar, Rational, std::greater<ArithVar> > CoefficientTable;
CoefficientTable d_coeffs;
* Construct a row equal to:
* basic = \sum_{x_i} c_i * x_i
*/
- Row(TNode basic, const Polynomial& sum):
- d_x_i(basic),
- d_coeffs(){
-
- Assert(d_x_i.getMetaKind() == kind::metakind::VARIABLE);
-
- for(Polynomial::iterator iter=sum.begin(), end = sum.end(); iter != end; ++iter){
- const Monomial& mono = *iter;
-
- Assert(!mono.isConstant());
-
- TNode coeff = mono.getConstant().getNode();
- TNode var_i = mono.getVarList().getNode();
-
- Assert(coeff.getKind() == kind::CONST_RATIONAL);
+ Row(ArithVar basic,
+ const std::vector< Rational >& coefficients,
+ const std::vector< ArithVar >& variables);
- Assert(!has(var_i));
- d_coeffs[var_i] = coeff.getConst<Rational>();
- Assert(coeff.getConst<Rational>() != Rational(0,1));
- Assert(d_coeffs[var_i] != Rational(0,1));
- }
- }
iterator begin(){
return d_coeffs.begin();
return d_coeffs.end();
}
- TNode basicVar(){
+ ArithVar basicVar(){
return d_x_i;
}
- bool has(TNode x_j){
+ bool has(ArithVar x_j){
CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
return x_jPos != d_coeffs.end();
}
- const Rational& lookup(TNode x_j){
+ const Rational& lookup(ArithVar x_j){
CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
Assert(x_jPos != d_coeffs.end());
return (*x_jPos).second;
}
- void pivot(TNode x_j){
- Rational negInverseA_rs = -(lookup(x_j).inverse());
- d_coeffs[d_x_i] = Rational(Integer(-1));
- d_coeffs.erase(x_j);
-
- d_x_i = x_j;
+ void pivot(ArithVar x_j);
- for(iterator nonbasicIter = begin(), nonbasicIter_end = end();
- nonbasicIter != nonbasicIter_end; ++nonbasicIter){
- nonbasicIter->second *= negInverseA_rs;
- }
-
- }
+ void subsitute(Row& row_s);
- void subsitute(Row& row_s){
- TNode x_s = row_s.basicVar();
-
- Assert(has(x_s));
- Assert(x_s != d_x_i);
-
- Rational zero(0,1);
-
- Rational a_rs = lookup(x_s);
- Assert(a_rs != zero);
- d_coeffs.erase(x_s);
-
- for(iterator iter = row_s.begin(), iter_end = row_s.end();
- iter != iter_end; ++iter){
- TNode x_j = iter->first;
- Rational a_sj = iter->second;
- a_sj *= a_rs;
- CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j);
-
- if(coeff_iter != d_coeffs.end()){
- coeff_iter->second += a_sj;
- if(coeff_iter->second == zero){
- d_coeffs.erase(coeff_iter);
- }
- }else{
- d_coeffs.insert(std::make_pair(x_j,a_sj));
- }
- }
- }
-
- void printRow(){
- Debug("tableau") << d_x_i << " ";
- for(iterator nonbasicIter = d_coeffs.begin();
- nonbasicIter != d_coeffs.end();
- ++nonbasicIter){
- TNode nb = nonbasicIter->first;
- Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}";
- }
- Debug("tableau") << std::endl;
- }
+ void printRow();
};
class Tableau {
public:
- typedef std::set<TNode> VarSet;
+ typedef std::set<ArithVar> VarSet;
private:
- typedef __gnu_cxx::hash_map<TNode, Row*, NodeHashFunction> RowsTable;
+ typedef __gnu_cxx::hash_map<ArithVar, Row*> RowsTable;
VarSet d_activeBasicVars;
RowsTable d_activeRows, d_inactiveRows;
+ ActivityMonitor& d_activityMonitor;
+ IsBasicManager& d_basicManager;
+
public:
/**
* Constructs an empty tableau.
*/
- Tableau() : d_activeBasicVars(), d_activeRows(), d_inactiveRows() {}
+ Tableau(ActivityMonitor &am, IsBasicManager& bm) :
+ d_activeBasicVars(),
+ d_activeRows(),
+ d_inactiveRows(),
+ d_activityMonitor(am),
+ d_basicManager(bm)
+ {}
VarSet::iterator begin(){
return d_activeBasicVars.begin();
return d_activeBasicVars.end();
}
- Row* lookup(TNode var){
+ Row* lookup(ArithVar var){
Assert(isActiveBasicVariable(var));
return d_activeRows[var];
}
private:
- Row* lookupEjected(TNode var){
+ Row* lookupEjected(ArithVar var){
Assert(isEjected(var));
return d_inactiveRows[var];
}
public:
- void addRow(TNode eq){
- TNode var = eq[0];
- TNode sumNode = eq[1];
-
- Assert(var.getAttribute(IsBasic()));
-
- Polynomial sum = Polynomial::parsePolynomial(sumNode);
-
- //The new basic variable cannot already be a basic variable
- Assert(!isActiveBasicVariable(var));
- d_activeBasicVars.insert(var);
- Row* row_var = new Row(var,sum);
- d_activeRows[var] = row_var;
-
- //A variable in the row may have been made non-basic already.
- //If this is the case we fake pivoting this variable
- for(Polynomial::iterator sumIter = sum.begin(); sumIter!= sum.end(); ++sumIter){
- const Monomial& child = *sumIter;
-
- Assert(!child.isConstant());
- TNode c = child.getVarList().getNode();
- if(isActiveBasicVariable(c)){
- Row* row_c = lookup(c);
- row_var->subsitute(*row_c);
- }
- }
- }
+ void addRow(ArithVar basicVar, const std::vector<Rational>& coeffs, const std::vector<ArithVar>& variables);
/**
* preconditions:
* x_s is non-basic, and
* a_rs != 0.
*/
- void pivot(TNode x_r, TNode x_s){
- RowsTable::iterator ptrRow_r = d_activeRows.find(x_r);
- Assert(ptrRow_r != d_activeRows.end());
-
- Row* row_s = (*ptrRow_r).second;
-
- Assert(row_s->has(x_s));
- row_s->pivot(x_s);
-
- d_activeRows.erase(ptrRow_r);
- d_activeBasicVars.erase(x_r);
- makeNonbasic(x_r);
-
- d_activeRows.insert(std::make_pair(x_s,row_s));
- d_activeBasicVars.insert(x_s);
- makeBasic(x_s);
-
- for(VarSet::iterator basicIter = begin(), endIter = end();
- basicIter != endIter; ++basicIter){
- TNode basic = *basicIter;
- Row* row_k = lookup(basic);
- if(row_k->has(x_s)){
- increaseActivity(basic, 30);
- row_k->subsitute(*row_s);
- }
- }
- }
- void printTableau(){
- for(VarSet::iterator basicIter = begin(), endIter = end();
- basicIter != endIter; ++basicIter){
- TNode basic = *basicIter;
- Row* row_k = lookup(basic);
- row_k->printRow();
- }
- }
+ void pivot(ArithVar x_r, ArithVar x_s);
+
+ void printTableau();
- bool isEjected(TNode var){
+ bool isEjected(ArithVar var){
return d_inactiveRows.find(var) != d_inactiveRows.end();
}
- void ejectBasic(TNode basic){
+ void ejectBasic(ArithVar basic){
+ Assert(d_basicManager.isBasic(basic));
Assert(isActiveBasicVariable(basic));
Row* row = lookup(basic);
d_inactiveRows.insert(std::make_pair(basic, row));
}
- void reinjectBasic(TNode basic){
+ void reinjectBasic(ArithVar basic){
+ Assert(d_basicManager.isBasic(basic));
Assert(isEjected(basic));
Row* row = lookupEjected(basic);
updateRow(row);
}
private:
- inline bool isActiveBasicVariable(TNode var){
+ inline bool isActiveBasicVariable(ArithVar var){
return d_activeBasicVars.find(var) != d_activeBasicVars.end();
}
- void updateRow(Row* row){
- for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){
- TNode var = i->first;
- ++i;
- if(isBasic(var)){
- Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
-
- Assert(row_var != row);
- row->subsitute(*row_var);
-
- i = row->begin();
- endIter = row->end();
- }
- }
- }
+ void updateRow(Row* row);
};
}; /* namespace arith */
Theory(id, c, out),
d_constants(NodeManager::currentNM()),
d_partialModel(c),
+ d_basicManager(),
+ d_activityMonitor(),
d_diseq(c),
+ d_tableau(d_activityMonitor, d_basicManager),
d_nextRewriter(&d_constants),
d_propagator(c),
d_statistics()
-{
- uint64_t ass_id = partial_model::Assignment::getId();
- Debug("arithsetup") << "Assignment: " << ass_id << std::endl;
-}
+{}
+
TheoryArith::~TheoryArith(){
for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){
Node var = *i;
d_statUpdates("theory::arith::updates",0),
d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
- d_statUpdateConflicts("theory::arith::UpdateConflicts", 0)
+ d_statUpdateConflicts("theory::arith::UpdateConflicts", 0),
+ d_statUserVariables("theory::arith::UserVariables", 0),
+ d_statSlackVariables("theory::arith::SlackVariables", 0)
{
StatisticsRegistry::registerStat(&d_statPivots);
StatisticsRegistry::registerStat(&d_statUpdates);
StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
StatisticsRegistry::registerStat(&d_statUpdateConflicts);
+ StatisticsRegistry::registerStat(&d_statUserVariables);
+ StatisticsRegistry::registerStat(&d_statSlackVariables);
}
TheoryArith::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
+ StatisticsRegistry::unregisterStat(&d_statUserVariables);
+ StatisticsRegistry::unregisterStat(&d_statSlackVariables);
}
}
-bool TheoryArith::shouldEject(TNode var){
+bool TheoryArith::shouldEject(ArithVar var){
if(d_partialModel.hasBounds(var)){
return false;
}else if(d_tableau.isEjected(var)) {
return false;
}else if(!d_partialModel.hasEverHadABound(var)){
return true;
- }else if(getActivity(var) >= ACTIVITY_THRESHOLD){
+ }else if(d_activityMonitor.getActivity(var) >= ActivityMonitor::ACTIVITY_THRESHOLD){
return true;
}
return false;
}
-TNode TheoryArith::findBasicRow(TNode variable){
+ArithVar TheoryArith::findBasicRow(ArithVar variable){
for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
basicIter != d_tableau.end();
++basicIter){
- TNode x_j = *basicIter;
+ ArithVar x_j = *basicIter;
Row* row_j = d_tableau.lookup(x_j);
if(row_j->has(variable)){
return x_j;
}
}
- return TNode::null();
+ return ARITHVAR_SENTINEL;
}
void TheoryArith::ejectInactiveVariables(){
Debug("decay") << "begin ejectInactiveVariables()" << endl;
- for(std::vector<Node>::iterator i = d_variables.begin(),
- end = d_variables.end(); i != end; ++i){
- TNode variable = *i;
+ for(ArithVar variable = 0, end = d_variables.size(); variable != end; ++variable){
+ //TNode var = *i;
+ //ArithVar variable = asArithVar(var);
if(shouldEject(variable)){
- if(isBasic(variable)){
+ if(d_basicManager.isBasic(variable)){
Debug("decay") << "ejecting basic " << variable << endl;;
d_tableau.ejectBasic(variable);
}
}
}
-void TheoryArith::reinjectVariable(TNode x){
+void TheoryArith::reinjectVariable(ArithVar x){
d_tableau.reinjectBasic(x);
d_out->augmentingLemma(eagerSplit);
}
- if(n.getMetaKind() == metakind::VARIABLE){
-
- setupVariable(n);
+ if(isTheoryLeaf(n)){
+ ArithVar varN = requestArithVar(n,false);
+ setupInitialValue(varN);
}
Debug("arith_preregister") << "end arith::preRegisterTerm("<< n <<")"<< endl;
}
+
+
+void TheoryArith::checkBasicVariable(ArithVar basic){
+ Assert(d_basicManager.isBasic(basic));
+ if(!d_partialModel.assignmentIsConsistent(basic)){
+ d_possiblyInconsistent.push(basic);
+ }
+}
+
+bool TheoryArith::isTheoryLeaf(TNode x) const{
+ return x.getMetaKind() == kind::metakind::VARIABLE;
+}
+
+ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
+ Assert(isTheoryLeaf(x));
+ Assert(!x.hasAttribute(ArithVarAttr()));
+
+ ArithVar varX = d_variables.size();
+ d_variables.push_back(Node(x));
+
+ x.setAttribute(ArithVarAttr(), varX);
+
+
+ d_activityMonitor.initActivity(varX);
+ d_basicManager.init(varX, basic);
+
+ Debug("arith::arithvar") << x << " |-> " << varX << endl;
+
+ return varX;
+}
+
+void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::vector<ArithVar>& variables) const{
+ for(Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i){
+ const Monomial& mono = *i;
+ const Constant& constant = mono.getConstant();
+ const VarList& variable = mono.getVarList();
+
+ Node n = variable.getNode();
+
+ Assert(isTheoryLeaf(n));
+ Assert(n.hasAttribute(ArithVarAttr()));
+
+ ArithVar av = n.getAttribute(ArithVarAttr());
+
+ coeffs.push_back(constant.getValue());
+ variables.push_back(av);
+ }
+}
+
void TheoryArith::setupSlack(TNode left){
+
TypeNode real_type = NodeManager::currentNM()->realType();
Node slack = NodeManager::currentNM()->mkVar(real_type);
-
left.setAttribute(Slack(), slack);
- makeBasic(slack);
- Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, slack, left);
+ ArithVar varSlack = requestArithVar(slack, true);
- d_tableau.addRow(eq);
+ Polynomial polyLeft = Polynomial::parsePolynomial(left);
- setupVariable(slack);
-}
+ vector<ArithVar> variables;
+ vector<Rational> coefficients;
+ asVectors(polyLeft, coefficients, variables);
-void TheoryArith::checkBasicVariable(TNode basic){
- Assert(isBasic(basic));
- if(!d_partialModel.assignmentIsConsistent(basic)){
- d_possiblyInconsistent.push(basic);
- }
+ d_tableau.addRow(varSlack, coefficients, variables);
+
+ setupInitialValue(varSlack);
}
/* Requirements:
* For basic variables the row must have been added to the tableau.
*/
-void TheoryArith::setupVariable(TNode x){
- Assert(x.getMetaKind() == kind::metakind::VARIABLE);
- d_variables.push_back(Node(x));
-
- initActivity(x);
+void TheoryArith::setupInitialValue(ArithVar x){
- if(!isBasic(x)){
+ if(!d_basicManager.isBasic(x)){
d_partialModel.initialize(x,d_constants.d_ZERO_DELTA);
}else{
//If the variable is basic, assertions may have already happened and updates
/**
* Computes the value of a basic variable using the current assignment.
*/
-DeltaRational TheoryArith::computeRowValueUsingAssignment(TNode x){
- Assert(isBasic(x));
+DeltaRational TheoryArith::computeRowValueUsingAssignment(ArithVar x){
+ Assert(d_basicManager.isBasic(x));
DeltaRational sum = d_constants.d_ZERO_DELTA;
Row* row = d_tableau.lookup(x);
for(Row::iterator i = row->begin(); i != row->end();++i){
- TNode nonbasic = i->first;
+ ArithVar nonbasic = i->first;
const Rational& coeff = i->second;
const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic);
sum = sum + (assignment * coeff);
/**
* Computes the value of a basic variable using the current assignment.
*/
-DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){
- Assert(isBasic(x));
+DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(ArithVar x){
+ Assert(d_basicManager.isBasic(x));
DeltaRational sum = d_constants.d_ZERO_DELTA;
Row* row = d_tableau.lookup(x);
for(Row::iterator i = row->begin(); i != row->end();++i){
- TNode nonbasic = i->first;
+ ArithVar nonbasic = i->first;
const Rational& coeff = i->second;
const DeltaRational& assignment = d_partialModel.getSafeAssignment(nonbasic);
sum = sum + (assignment * coeff);
/* procedure AssertUpper( x_i <= c_i) */
bool TheoryArith::AssertUpper(TNode n, TNode original){
- TNode x_i = n[0];
+ TNode nodeX_i = n[0];
+ ArithVar x_i = nodeX_i.getAttribute(ArithVarAttr());
Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
DeltaRational c_i(n[1].getConst<Rational>(), dcoeff);
Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
- if(isBasic(x_i) && d_tableau.isEjected(x_i)){
+ if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
reinjectVariable(x_i);
}
d_partialModel.setUpperConstraint(x_i,original);
d_partialModel.setUpperBound(x_i, c_i);
- resetActivity(x_i);
+ d_activityMonitor.resetActivity(x_i);
- if(!isBasic(x_i)){
+ if(!d_basicManager.isBasic(x_i)){
if(d_partialModel.getAssignment(x_i) > c_i){
update(x_i, c_i);
}
/* procedure AssertLower( x_i >= c_i ) */
bool TheoryArith::AssertLower(TNode n, TNode original){
- TNode x_i = n[0];
+ TNode nodeX_i = n[0];
+ ArithVar x_i = nodeX_i.getAttribute(ArithVarAttr());
Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
DeltaRational c_i(n[1].getConst<Rational>(),dcoeff);
Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
- if(isBasic(x_i) && d_tableau.isEjected(x_i)){
+ if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
reinjectVariable(x_i);
}
d_partialModel.setLowerConstraint(x_i,original);
d_partialModel.setLowerBound(x_i, c_i);
- resetActivity(x_i);
+ d_activityMonitor.resetActivity(x_i);
- if(!isBasic(x_i)){
+ if(!d_basicManager.isBasic(x_i)){
if(d_partialModel.getAssignment(x_i) < c_i){
update(x_i, c_i);
}
/* procedure AssertLower( x_i == c_i ) */
bool TheoryArith::AssertEquality(TNode n, TNode original){
Assert(n.getKind() == EQUAL);
- TNode x_i = n[0];
+ TNode nodeX_i = n[0];
+ ArithVar x_i = nodeX_i.getAttribute(ArithVarAttr());
DeltaRational c_i(n[1].getConst<Rational>());
Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
- if(isBasic(x_i) && d_tableau.isEjected(x_i)){
+ if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
reinjectVariable(x_i);
}
d_partialModel.setUpperConstraint(x_i,original);
d_partialModel.setUpperBound(x_i, c_i);
- resetActivity(x_i);
+ d_activityMonitor.resetActivity(x_i);
- if(!isBasic(x_i)){
+ if(!d_basicManager.isBasic(x_i)){
if(!(d_partialModel.getAssignment(x_i) == c_i)){
update(x_i, c_i);
}
return false;
}
-void TheoryArith::update(TNode x_i, DeltaRational& v){
- Assert(!isBasic(x_i));
+void TheoryArith::update(ArithVar x_i, DeltaRational& v){
+ Assert(!d_basicManager.isBasic(x_i));
DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
++(d_statistics.d_statUpdates);
for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
basicIter != d_tableau.end();
++basicIter){
- TNode x_j = *basicIter;
+ ArithVar x_j = *basicIter;
Row* row_j = d_tableau.lookup(x_j);
if(row_j->has(x_i)){
DeltaRational nAssignment = assignment+(diff * a_ji);
d_partialModel.setAssignment(x_j, nAssignment);
- increaseActivity(x_j, 1);
+ d_activityMonitor.increaseActivity(x_j, 1);
checkBasicVariable(x_j);
}
}
}
-void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
+void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
Assert(x_i != x_j);
Row* row_i = d_tableau.lookup(x_i);
for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
basicIter != d_tableau.end();
++basicIter){
- TNode x_k = *basicIter;
+ ArithVar x_k = *basicIter;
Row* row_k = d_tableau.lookup(x_k);
if(x_k != x_i && row_k->has(x_j)){
DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
d_partialModel.setAssignment(x_k, nextAssignment);
- increaseActivity(x_j, 1);
+ d_activityMonitor.increaseActivity(x_j, 1);
checkBasicVariable(x_k);
}
}
}
-TNode TheoryArith::selectSmallestInconsistentVar(){
+ArithVar TheoryArith::selectSmallestInconsistentVar(){
Debug("arith_update") << "selectSmallestInconsistentVar()" << endl;
Debug("arith_update") << "possiblyInconsistent.size()"
<< d_possiblyInconsistent.size() << endl;
while(!d_possiblyInconsistent.empty()){
- TNode var = d_possiblyInconsistent.top();
+ ArithVar var = d_possiblyInconsistent.top();
Debug("arith_update") << "possiblyInconsistent var" << var << endl;
- if(isBasic(var)){
+ if(d_basicManager.isBasic(var)){
if(!d_partialModel.assignmentIsConsistent(var)){
return var;
}
basicIter != d_tableau.end();
++basicIter){
- TNode basic = *basicIter;
+ ArithVar basic = *basicIter;
Assert(d_partialModel.assignmentIsConsistent(basic));
if(!d_partialModel.assignmentIsConsistent(basic)){
return basic;
}
}
- return TNode::null();
+ return ARITHVAR_SENTINEL;
}
template <bool above>
-TNode TheoryArith::selectSlack(TNode x_i){
+ArithVar TheoryArith::selectSlack(ArithVar x_i){
Row* row_i = d_tableau.lookup(x_i);
for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
- TNode nonbasic = nbi->first;
+ ArithVar nonbasic = nbi->first;
const Rational& a_ij = nbi->second;
int cmp = a_ij.cmp(d_constants.d_ZERO);
if(above){ // beta(x_i) > u_i
}
}
}
- return TNode::null();
+ return ARITHVAR_SENTINEL;
}
while(true){
if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
- TNode x_i = selectSmallestInconsistentVar();
+ ArithVar x_i = selectSmallestInconsistentVar();
Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
- if(x_i == Node::null()){
+ if(x_i == ARITHVAR_SENTINEL){
Debug("arith_update") << "No inconsistent variables" << endl;
return Node::null(); //sat
}
if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
DeltaRational l_i = d_partialModel.getLowerBound(x_i);
- TNode x_j = selectSlackBelow(x_i);
- if(x_j == TNode::null() ){
+ ArithVar 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);
- TNode x_j = selectSlackAbove(x_i);
- if(x_j == TNode::null() ){
+ ArithVar x_j = selectSlackAbove(x_i);
+ if(x_j == ARITHVAR_SENTINEL ){
++(d_statistics.d_statUpdateConflicts);
return generateConflictAbove(x_i); //unsat
}
}
}
-Node TheoryArith::generateConflictAbove(TNode conflictVar){
+Node TheoryArith::generateConflictAbove(ArithVar conflictVar){
+
Row* row_i = d_tableau.lookup(conflictVar);
NodeBuilder<> nb(kind::AND);
nb << bound;
for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
- TNode nonbasic = nbi->first;
+ ArithVar nonbasic = nbi->first;
const Rational& a_ij = nbi->second;
Assert(a_ij != d_constants.d_ZERO);
return conflict;
}
-Node TheoryArith::generateConflictBelow(TNode conflictVar){
+Node TheoryArith::generateConflictBelow(ArithVar conflictVar){
Row* row_i = d_tableau.lookup(conflictVar);
NodeBuilder<> nb(kind::AND);
nb << bound;
for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
- TNode nonbasic = nbi->first;
+ ArithVar nonbasic = nbi->first;
const Rational& a_ij = nbi->second;
Assert(a_ij != d_constants.d_ZERO);
if(Debug.isOn("arith::print_model")) {
Debug("arith::print_model") << "Model:" << endl;
- for (unsigned i = 0; i < d_variables.size(); ++ i) {
+ for (ArithVar i = 0; i < d_variables.size(); ++ i) {
Debug("arith::print_model") << d_variables[i] << " : " <<
- d_partialModel.getAssignment(d_variables[i]);
- if(isBasic(d_variables[i]))
+ d_partialModel.getAssignment(i);
+ if(d_basicManager.isBasic(i))
Debug("arith::print_model") << " (basic)";
Debug("arith::print_model") << endl;
}
}
if(Debug.isOn("arith::print_assertions")) {
Debug("arith::print_assertions") << "Assertions:" << endl;
- for (unsigned i = 0; i < d_variables.size(); ++ i) {
- Node x = d_variables[i];
- if (x.hasAttribute(partial_model::LowerConstraint())) {
- Node constr = d_partialModel.getLowerConstraint(x);
- Debug("arith::print_assertions") << constr.toString() << endl;
- }
- if (x.hasAttribute(partial_model::UpperConstraint())) {
- Node constr = d_partialModel.getUpperConstraint(x);
- Debug("arith::print_assertions") << constr.toString() << endl;
- }
+ for (ArithVar i = 0; i < d_variables.size(); ++ i) {
+ Node lConstr = d_partialModel.getLowerConstraint(i);
+ Debug("arith::print_assertions") << lConstr.toString() << endl;
+
+ Node uConstr = d_partialModel.getUpperConstraint(i);
+ Debug("arith::print_assertions") << uConstr.toString() << endl;
+
}
}
}
for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
basicIter != d_tableau.end(); ++basicIter){
- TNode basic = *basicIter;
+ ArithVar basic = *basicIter;
Row* row_k = d_tableau.lookup(basic);
DeltaRational sum;
Debug("paranoid:check_tableau") << "starting row" << basic << endl;
for(Row::iterator nonbasicIter = row_k->begin();
nonbasicIter != row_k->end();
++nonbasicIter){
- TNode nonbasic = nonbasicIter->first;
+ ArithVar nonbasic = nonbasicIter->first;
const Rational& coeff = nonbasicIter->second;
DeltaRational beta = d_partialModel.getAssignment(nonbasic);
Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl;
#include "context/cdlist.h"
#include "expr/node.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/basic.h"
+#include "theory/arith/arith_activity.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/tableau.h"
#include "theory/arith/next_arith_rewriter.h"
std::vector<Node> d_splits;
//This stores the eager splits sent out of the theory.
- std::vector<Node> d_variables;
- // Currently forces every variable and skolem constant that
- // can hit the tableau to stay alive forever!
-
/* Chopping block ends */
+ std::vector<Node> d_variables;
/**
* Priority Queue of the basic variables that may be inconsistent.
* basic variable. This is only required to be a superset though so its
* contents must be checked to still be basic and inconsistent.
*/
- std::priority_queue<Node> d_possiblyInconsistent;
+ std::priority_queue<ArithVar> d_possiblyInconsistent;
/** Stores system wide constants to avoid unnessecary reconstruction. */
ArithConstants d_constants;
*/
ArithPartialModel d_partialModel;
+ IsBasicManager d_basicManager;
+ ActivityMonitor d_activityMonitor;
/**
* List of all of the inequalities asserted in the current context.
std::string identify() const { return std::string("TheoryArith"); }
private:
+
+ bool isTheoryLeaf(TNode x) const;
+
/**
* Assert*(n, orig) takes an bound n that is implied by orig.
* and asserts that as a new bound if it is tighter than the current bound
* Updates the assignment of a nonbasic variable x_i to v.
* Also updates the assignment of basic variables accordingly.
*/
- void update(TNode x_i, DeltaRational& v);
+ void update(ArithVar x_i, DeltaRational& v);
/**
* Updates the value of a basic variable x_i to v,
* and then pivots x_i with the nonbasic variable in its row x_j.
* Updates the assignment of the other basic variables accordingly.
*/
- void pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v);
+ void pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v);
/**
* Tries to update the assignments of variables such that all of the
* - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j)
* - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
*/
- template <bool above>
- TNode selectSlack(TNode x_i);
+ template <bool above> ArithVar selectSlack(ArithVar x_i);
- TNode selectSlackBelow(TNode x_i) { return selectSlack<false>(x_i); }
- TNode selectSlackAbove(TNode x_i) { return selectSlack<true>(x_i); }
+ ArithVar selectSlackBelow(ArithVar x_i) { return selectSlack<false>(x_i); }
+ ArithVar selectSlackAbove(ArithVar x_i) { return selectSlack<true>(x_i); }
/**
* Returns the smallest basic variable whose assignment is not consistent
* with its upper and lower bounds.
*/
- TNode selectSmallestInconsistentVar();
+ ArithVar selectSmallestInconsistentVar();
/**
* Given a non-basic variable that is know to not be updatable
* to a consistent value, construct and return a conflict.
* Follows section 4.2 in the CAV06 paper.
*/
- Node generateConflictAbove(TNode conflictVar);
- Node generateConflictBelow(TNode conflictVar);
+ Node generateConflictAbove(ArithVar conflictVar);
+ Node generateConflictBelow(ArithVar conflictVar);
+ /**
+ * This requests a new unique ArithVar value for x.
+ * This also does initial (not context dependent) set up for a variable,
+ * except for setting up the initial.
+ */
+ ArithVar requestArithVar(TNode x, bool basic);
+
/** Initial (not context dependent) sets up for a variable.*/
- void setupVariable(TNode x);
+ void setupInitialValue(ArithVar x);
/** Initial (not context dependent) sets up for a new slack variable.*/
void setupSlack(TNode left);
/** Computes the value of a row in the tableau using the current assignment.*/
- DeltaRational computeRowValueUsingAssignment(TNode x);
+ DeltaRational computeRowValueUsingAssignment(ArithVar x);
/** Computes the value of a row in the tableau using the safe assignment.*/
- DeltaRational computeRowValueUsingSavedAssignment(TNode x);
+ DeltaRational computeRowValueUsingSavedAssignment(ArithVar x);
/** Checks to make sure the assignment is consistent with the tableau. */
void checkTableau();
/** Check to make sure all of the basic variables are within their bounds. */
- void checkBasicVariable(TNode basic);
+ void checkBasicVariable(ArithVar basic);
/**
* Handles the case splitting for check() for a new assertion.
*/
bool assertionCases(TNode original, TNode assertion);
- TNode findBasicRow(TNode variable);
- bool shouldEject(TNode var);
+ ArithVar findBasicRow(ArithVar variable);
+ bool shouldEject(ArithVar var);
void ejectInactiveVariables();
- void reinjectVariable(TNode x);
+ void reinjectVariable(ArithVar x);
//TODO get rid of this!
Node simulatePreprocessing(TNode n);
+ void asVectors(Polynomial& p,
+ std::vector<Rational>& coeffs,
+ std::vector<ArithVar>& variables) const;
+
/** 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_statUserVariables, d_statSlackVariables;
Statistics();
~Statistics();
TESTS = \
arith.01.cvc \
arith.02.cvc \
- arith.03.cvc
+ arith.03.cvc \
+ leq.01.smt
EXTRA_DIST = $(TESTS)
--- /dev/null
+(benchmark fuzzsmt
+:logic QF_LRA
+:status unsat
+:formula
+(<= 3 (~ 3))
+)
projects / cvc5.git / commitdiff