From 37c20e30239e8ce86e9fc7106afcf5a7b896e7c3 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 2 Oct 2010 05:52:51 +0000 Subject: [PATCH] branches/arith-indexed-variables merged into the main trunk. --- src/context/cdmap.h | 16 +- src/theory/arith/Makefile.am | 1 + src/theory/arith/arith_activity.h | 49 +-- src/theory/arith/arith_utilities.h | 16 + src/theory/arith/basic.h | 42 ++- src/theory/arith/normal_form.cpp | 4 +- src/theory/arith/partial_model.cpp | 455 +++++++++++++++--------- src/theory/arith/partial_model.h | 137 ++++--- src/theory/arith/tableau.cpp | 184 ++++++++++ src/theory/arith/tableau.h | 203 ++--------- src/theory/arith/theory_arith.cpp | 237 +++++++----- src/theory/arith/theory_arith.h | 58 +-- test/regress/regress0/arith/Makefile.am | 3 +- test/regress/regress0/arith/leq.01.smt | 6 + 14 files changed, 859 insertions(+), 552 deletions(-) create mode 100644 src/theory/arith/tableau.cpp create mode 100644 test/regress/regress0/arith/leq.01.smt diff --git a/src/context/cdmap.h b/src/context/cdmap.h index d9cc5b1a3..b7fc5dcc6 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -340,19 +340,17 @@ public: } 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(); diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index ead39082c..665b9be4b 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -22,6 +22,7 @@ libarith_la_SOURCES = \ basic.h \ slack.h \ tableau.h \ + tableau.cpp \ arith_propagator.h \ arith_propagator.cpp \ theory_arith.h \ diff --git a/src/theory/arith/arith_activity.h b/src/theory/arith/arith_activity.h index f336237a4..7db3d7d8f 100644 --- a/src/theory/arith/arith_activity.h +++ b/src/theory/arith/arith_activity.h @@ -30,27 +30,34 @@ namespace theory { namespace arith { -struct ArithActivityID {}; -typedef expr::Attribute 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 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 */ diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index d2c07900d..4ae0e44ef 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -24,11 +24,27 @@ #include "util/rational.h" #include "expr/node.h" +#include "expr/attribute.h" +#include +#include namespace CVC4 { namespace theory { namespace arith { + +typedef uint64_t ArithVar; +//static const ArithVar ARITHVAR_SENTINEL = std::numeric_limits::max(); +#define ARITHVAR_SENTINEL std::numeric_limits::max() + +struct ArithVarAttrID{}; +typedef expr::Attribute ArithVarAttr; + +inline ArithVar asArithVar(TNode x){ + Assert(x.hasAttribute(ArithVarAttr())); + return x.getAttribute(ArithVarAttr()); +} + inline Node mkRationalNode(const Rational& q){ return NodeManager::currentNM()->mkConst(q); } diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h index 11f0f71f0..c52e0881d 100644 --- a/src/theory/arith/basic.h +++ b/src/theory/arith/basic.h @@ -29,22 +29,32 @@ namespace CVC4 { namespace theory { namespace arith { -struct IsBasicAttrID; - -typedef expr::Attribute 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 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 */ diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 7baacd4f5..14c525267 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -244,8 +244,8 @@ Comparison Comparison::parseNormalForm(TNode n) { Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Constant& right) { Assert(isRelationOperator(k)); if(left.isConstant()) { - const Rational& rConst = left.getNode().getConst(); - const Rational& lConst = right.getNode().getConst(); + const Rational& lConst = left.getNode().getConst(); + const Rational& rConst = right.getNode().getConst(); bool res = evaluateConstantPredicate(k, lConst, rConst); return Comparison(res); } else { diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 18993c748..6f0ded9e5 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -28,267 +28,368 @@ using namespace CVC4::theory; 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 < \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(); @@ -301,26 +402,38 @@ void ArithPartialModel::commitAssignmentChanges(){ 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; } diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index bd945002e..bec703369 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -19,7 +19,8 @@ #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" @@ -34,32 +35,35 @@ namespace theory { 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 Assignment; -struct AssignmentAttrID {}; -typedef expr::Attribute Assignment; + +// struct SafeAssignmentAttrID {}; +// typedef expr::Attribute SafeAssignment; -struct SafeAssignmentAttrID {}; -typedef expr::Attribute 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 CDDRationalMap; +//typedef context::CDMap 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 @@ -95,20 +99,20 @@ typedef context::CDMap CDDRationalMap; * Note the strong correspondence between this and LowerBoundMap. * This is used during conflict analysis. */ -struct LowerConstraintAttrID {}; -typedef expr::CDAttribute LowerConstraint; +// struct LowerConstraintAttrID {}; +// typedef expr::CDAttribute LowerConstraint; /** * See the documentation for LowerConstraint. */ -struct UpperConstraintAttrID {}; -typedef expr::CDAttribute UpperConstraint; +// struct UpperConstraintAttrID {}; +// typedef expr::CDAttribute UpperConstraint; -struct TheoryArithPropagatedID {}; -typedef expr::CDAttribute TheoryArithPropagated; +// struct TheoryArithPropagatedID {}; +// typedef expr::CDAttribute TheoryArithPropagated; -struct HasHadABoundID {}; -typedef expr::Attribute HasHadABound; +// struct HasHadABoundID {}; +// typedef expr::Attribute HasHadABound; }; /*namespace partial_model*/ @@ -116,36 +120,55 @@ typedef expr::Attribute HasHadABound; class ArithPartialModel { private: - partial_model::CDDRationalMap d_LowerBoundMap; - partial_model::CDDRationalMap d_UpperBoundMap; + + unsigned d_mapSize; + //Maps from ArithVar -> T + + std::vector d_hasHadABound; + + std::vector d_hasSafeAssignment; + std::vector d_assignment; + std::vector d_safeAssignment; + + context::CDVector d_upperBound; + context::CDVector d_lowerBound; + context::CDVector d_upperConstraint; + context::CDVector d_lowerConstraint; /** * List contains all of the variables that have an unsafe assignment. */ - typedef std::vector HistoryList; + typedef std::vector 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(); @@ -156,41 +179,42 @@ public: - 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: @@ -200,6 +224,13 @@ private: * revertAssignmentChanges() and commitAssignmentChanges(). */ void clearSafeAssignments(bool revert); + + bool equalSizes(); + + bool inMaps(ArithVar x) const{ + return 0 <= x && x < d_mapSize; + } + }; diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp new file mode 100644 index 000000000..e43458a23 --- /dev/null +++ b/src/theory/arith/tableau.cpp @@ -0,0 +1,184 @@ + +#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::const_iterator coeffIter = coefficients.begin(); + std::vector::const_iterator coeffEnd = coefficients.end(); + std::vector::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& coeffs, + const std::vector& 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::const_iterator coeffsIter = coeffs.begin(); + std::vector::const_iterator coeffsEnd = coeffs.end(); + + std::vector::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(); + } + } +} diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 768d9f39d..dc2c19936 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -21,8 +21,9 @@ #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 @@ -38,9 +39,9 @@ namespace arith { class Row { - TNode d_x_i; + ArithVar d_x_i; - typedef std::map CoefficientTable; + typedef std::map > CoefficientTable; CoefficientTable d_coeffs; @@ -52,28 +53,10 @@ public: * 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(); - Assert(coeff.getConst() != Rational(0,1)); - Assert(d_coeffs[var_i] != Rational(0,1)); - } - } iterator begin(){ return d_coeffs.begin(); @@ -83,93 +66,53 @@ public: 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 VarSet; + typedef std::set VarSet; private: - typedef __gnu_cxx::hash_map RowsTable; + typedef __gnu_cxx::hash_map 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(); @@ -179,45 +122,19 @@ public: 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& coeffs, const std::vector& variables); /** * preconditions: @@ -225,47 +142,16 @@ public: * 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); @@ -275,7 +161,8 @@ public: 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); @@ -287,25 +174,11 @@ public: 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 */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 41882e87c..be40472b6 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -56,14 +56,15 @@ TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) : 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::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){ Node var = *i; @@ -76,13 +77,17 @@ TheoryArith::Statistics::Statistics(): 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(){ @@ -91,6 +96,8 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts); StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts); StatisticsRegistry::unregisterStat(&d_statUpdateConflicts); + StatisticsRegistry::unregisterStat(&d_statUserVariables); + StatisticsRegistry::unregisterStat(&d_statSlackVariables); } @@ -117,40 +124,40 @@ bool isNormalAtom(TNode n){ } -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::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); } @@ -158,7 +165,7 @@ void TheoryArith::ejectInactiveVariables(){ } } -void TheoryArith::reinjectVariable(TNode x){ +void TheoryArith::reinjectVariable(ArithVar x){ d_tableau.reinjectBasic(x); @@ -184,9 +191,9 @@ void TheoryArith::preRegisterTerm(TNode n) { d_out->augmentingLemma(eagerSplit); } - if(n.getMetaKind() == metakind::VARIABLE){ - - setupVariable(n); + if(isTheoryLeaf(n)){ + ArithVar varN = requestArithVar(n,false); + setupInitialValue(varN); } @@ -210,38 +217,81 @@ void TheoryArith::preRegisterTerm(TNode n) { 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& coeffs, std::vector& 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 variables; + vector 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 @@ -270,13 +320,13 @@ void TheoryArith::setupVariable(TNode x){ /** * 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); @@ -287,13 +337,13 @@ DeltaRational TheoryArith::computeRowValueUsingAssignment(TNode x){ /** * 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); @@ -311,13 +361,14 @@ void TheoryArith::registerTerm(TNode tn){ /* 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(), 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); } @@ -336,9 +387,9 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){ 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); } @@ -351,13 +402,14 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){ /* 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(),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); } @@ -375,9 +427,9 @@ bool TheoryArith::AssertLower(TNode n, TNode original){ 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); } @@ -391,12 +443,13 @@ bool TheoryArith::AssertLower(TNode n, TNode original){ /* 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()); 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); } @@ -428,9 +481,9 @@ bool TheoryArith::AssertEquality(TNode n, TNode original){ 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); } @@ -440,8 +493,8 @@ bool TheoryArith::AssertEquality(TNode n, TNode original){ 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); @@ -452,7 +505,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){ 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)){ @@ -462,7 +515,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){ 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); } @@ -475,7 +528,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){ } } -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); @@ -496,7 +549,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){ 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)){ @@ -504,7 +557,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){ 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); } @@ -520,15 +573,15 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){ } } -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; } @@ -541,7 +594,7 @@ TNode TheoryArith::selectSmallestInconsistentVar(){ basicIter != d_tableau.end(); ++basicIter){ - TNode basic = *basicIter; + ArithVar basic = *basicIter; Assert(d_partialModel.assignmentIsConsistent(basic)); if(!d_partialModel.assignmentIsConsistent(basic)){ return basic; @@ -549,15 +602,15 @@ TNode TheoryArith::selectSmallestInconsistentVar(){ } } - return TNode::null(); + return ARITHVAR_SENTINEL; } template -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 @@ -574,7 +627,7 @@ TNode TheoryArith::selectSlack(TNode x_i){ } } } - return TNode::null(); + return ARITHVAR_SENTINEL; } @@ -586,9 +639,9 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 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 } @@ -601,8 +654,8 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 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 } @@ -610,8 +663,8 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 }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 } @@ -620,7 +673,8 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 } } -Node TheoryArith::generateConflictAbove(TNode conflictVar){ +Node TheoryArith::generateConflictAbove(ArithVar conflictVar){ + Row* row_i = d_tableau.lookup(conflictVar); NodeBuilder<> nb(kind::AND); @@ -634,7 +688,7 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){ 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); @@ -657,7 +711,7 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){ return conflict; } -Node TheoryArith::generateConflictBelow(TNode conflictVar){ +Node TheoryArith::generateConflictBelow(ArithVar conflictVar){ Row* row_i = d_tableau.lookup(conflictVar); NodeBuilder<> nb(kind::AND); @@ -670,7 +724,7 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){ 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); @@ -801,26 +855,23 @@ void TheoryArith::check(Effort level){ 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; + } } } @@ -836,14 +887,14 @@ void TheoryArith::checkTableau(){ 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< d_splits; //This stores the eager splits sent out of the theory. - std::vector d_variables; - // Currently forces every variable and skolem constant that - // can hit the tableau to stay alive forever! - /* Chopping block ends */ + std::vector d_variables; /** * Priority Queue of the basic variables that may be inconsistent. @@ -69,7 +69,7 @@ private: * 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 d_possiblyInconsistent; + std::priority_queue d_possiblyInconsistent; /** Stores system wide constants to avoid unnessecary reconstruction. */ ArithConstants d_constants; @@ -80,6 +80,8 @@ private: */ ArithPartialModel d_partialModel; + IsBasicManager d_basicManager; + ActivityMonitor d_activityMonitor; /** * List of all of the inequalities asserted in the current context. @@ -131,6 +133,9 @@ public: 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 @@ -155,14 +160,14 @@ private: * 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 @@ -193,45 +198,51 @@ private: * - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j) * - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j) */ - template - TNode selectSlack(TNode x_i); + template ArithVar selectSlack(ArithVar x_i); - TNode selectSlackBelow(TNode x_i) { return selectSlack(x_i); } - TNode selectSlackAbove(TNode x_i) { return selectSlack(x_i); } + ArithVar selectSlackBelow(ArithVar x_i) { return selectSlack(x_i); } + ArithVar selectSlackAbove(ArithVar x_i) { return selectSlack(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. @@ -239,20 +250,25 @@ private: */ 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& coeffs, + std::vector& 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(); diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 18ca5fe86..f38413d95 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -6,7 +6,8 @@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 TESTS = \ arith.01.cvc \ arith.02.cvc \ - arith.03.cvc + arith.03.cvc \ + leq.01.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/arith/leq.01.smt b/test/regress/regress0/arith/leq.01.smt new file mode 100644 index 000000000..8cb08848b --- /dev/null +++ b/test/regress/regress0/arith/leq.01.smt @@ -0,0 +1,6 @@ +(benchmark fuzzsmt +:logic QF_LRA +:status unsat +:formula +(<= 3 (~ 3)) +) -- 2.30.2