diff options
author | Tim King <taking@cs.nyu.edu> | 2012-12-05 19:47:31 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-12-05 19:47:31 +0000 |
commit | 356a8b6e5ea2622d0fef5cf209159caf08ba5297 (patch) | |
tree | 80bd9eb27f163bcca74f5e44be23e9bccd4abcc7 /src | |
parent | 7f52115ab0dcba4c8ba9403a5f25b8e8c588911a (diff) |
Cleanup of arithmetic, and some new utility functions for the coming fcsimplex code.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/arith_utilities.h | 53 | ||||
-rw-r--r-- | src/theory/arith/arithvar.h | 10 | ||||
-rw-r--r-- | src/theory/arith/partial_model.cpp | 23 | ||||
-rw-r--r-- | src/theory/arith/partial_model.h | 25 |
4 files changed, 56 insertions, 55 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index c7f511a98..76210fc7c 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -168,59 +168,6 @@ inline int deltaCoeff(Kind k){ } } - -// template <bool selectLeft> -// inline TNode getSide(TNode assertion, Kind simpleKind){ -// switch(simpleKind){ -// case kind::LT: -// case kind::GT: -// case kind::DISTINCT: -// return selectLeft ? (assertion[0])[0] : (assertion[0])[1]; -// case kind::LEQ: -// case kind::GEQ: -// case kind::EQUAL: -// return selectLeft ? assertion[0] : assertion[1]; -// default: -// Unreachable(); -// return TNode::null(); -// } -// } - -// inline DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){ -// TNode right = getSide<false>(assertion, simpleKind); - -// Assert(right.getKind() == kind::CONST_RATIONAL); -// const Rational& noninf = right.getConst<Rational>(); - -// Rational inf = Rational(Integer(deltaCoeff(simpleKind))); -// return DeltaRational(noninf, inf); -// } - -// inline DeltaRational asDeltaRational(TNode n){ -// Kind simp = simplifiedKind(n); -// return determineRightConstant(n, simp); -// } - -// /** -// * Takes two nodes with exactly 2 children, -// * the second child of both are of kind CONST_RATIONAL, -// * and compares value of the two children. -// * This is for comparing inequality nodes. -// * RightHandRationalLT((<= x 50), (< x 75)) == true -// */ -// struct RightHandRationalLT -// { -// bool operator()(TNode s1, TNode s2) const -// { -// TNode rh1 = s1[1]; -// TNode rh2 = s2[1]; -// const Rational& c1 = rh1.getConst<Rational>(); -// const Rational& c2 = rh2.getConst<Rational>(); -// int cmpRes = c1.cmp(c2); -// return cmpRes < 0; -// } -// }; - inline Node negateConjunctionAsClause(TNode conjunction){ Assert(conjunction.getKind() == kind::AND); NodeBuilder<> orBuilder(kind::OR); diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h index 7cb6c6e99..eac238cba 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/arithvar.h @@ -50,6 +50,16 @@ public: virtual void operator()(ArithVar x) = 0; }; +/** + * Requests arithmetic variables for internal use, + * and releases arithmetic variables that are no longer being used. + */ +class ArithVarMalloc { +public: + virtual ArithVar request() = 0; + virtual void release(ArithVar v) = 0; +}; + class TNodeCallBack { public: virtual void operator()(TNode n) = 0; diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 0ffe67763..5dccd8747 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -72,7 +72,9 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, con Debug("partial_model") << "pm: updating the assignment to" << x << " now " << r <<endl; if(safe == r){ - d_hasSafeAssignment[x] = false; + if(d_hasSafeAssignment[x]){ + d_safeAssignment[x] = safe; + } }else{ d_safeAssignment[x] = safe; @@ -177,6 +179,25 @@ void ArithPartialModel::setUpperBoundConstraint(Constraint c){ d_ubc.set(x, c); } +void ArithPartialModel::forceRelaxLowerBound(ArithVar v){ + AssertArgument(inMaps(v), "Calling forceRelaxLowerBound on a variable that is not properly setup."); + AssertArgument(hasLowerBound(v), "Calling forceRelaxLowerBound on a variable without a lowerbound."); + + Debug("partial_model") << "forceRelaxLowerBound(" << v << ") dropping :" << getLowerBoundConstraint(v) << endl; + + d_lbc.set(v, NullConstraint); +} + + +void ArithPartialModel::forceRelaxUpperBound(ArithVar v){ + AssertArgument(inMaps(v), "Calling forceRelaxUpperBound on a variable that is not properly setup."); + AssertArgument(hasUpperBound(v), "Calling forceRelaxUpperBound on a variable without an upper bound."); + + Debug("partial_model") << "forceRelaxUpperBound(" << v << ") dropping :" << getUpperBoundConstraint(v) << endl; + + d_ubc.set(v, NullConstraint); +} + int ArithPartialModel::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{ if(!hasLowerBound(x)){ // l = -\intfy diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 49cfd44a1..9a41d8d23 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -68,16 +68,40 @@ public: ArithPartialModel(context::Context* c, RationalCallBack& deltaComputation); + /** + * This sets the lower bound for a variable in the current context. + * This must be stronger the previous constraint. + */ void setLowerBoundConstraint(Constraint lb); + + /** + * This sets the upper bound for a variable in the current context. + * This must be stronger the previous constraint. + */ void setUpperBoundConstraint(Constraint ub); + /** Returns the constraint for the upper bound of a variable. */ inline Constraint getUpperBoundConstraint(ArithVar x) const{ return d_ubc[x]; } + /** Returns the constraint for the lower bound of a variable. */ inline Constraint getLowerBoundConstraint(ArithVar x) const{ return d_lbc[x]; } + /** + * This forces the lower bound for a variable to be relaxed in the current context. + * This is done by forcing the lower bound to be NullConstraint. + * This is an expert only operation! (See primal simplex for an example.) + */ + void forceRelaxLowerBound(ArithVar x); + + /** + * This forces the upper bound for a variable to be relaxed in the current context. + * This is done by forcing the upper bound to be NullConstraint. + * This is an expert only operation! (See primal simplex for an example.) + */ + void forceRelaxUpperBound(ArithVar x); /* Initializes a variable to a safe value.*/ void initialize(ArithVar x, const DeltaRational& r); @@ -190,7 +214,6 @@ public: d_deltaIsSafe = true; } - private: /** |