From: Tim King <taking@cs.nyu.edu>
Date: Wed, 5 Dec 2012 19:47:31 +0000 (+0000)
Subject: Cleanup of arithmetic, and some new utility functions for the coming fcsimplex code.
X-Git-Tag: cvc5-1.0.0~7480
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=356a8b6e5ea2622d0fef5cf209159caf08ba5297;p=cvc5.git

Cleanup of arithmetic, and some new utility functions for the coming fcsimplex code.
---

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:
 
   /**