Fixed computation of infinitesimals for arithmetic model generation.

1 files changed, 14 insertions, 85 deletions

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index bec703369..256a6b931 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -34,90 +34,6 @@ namespace CVC4 {
 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 AssignmentAttrID {};
-// typedef expr::Attribute<AssignmentAttrID,
-//                         DeltaRational*,
-//                         DeltaRationalCleanupStrategy> Assignment;
-
-
-// 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;
-/* 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
- * framework do not provide a terribly satisfying answer.
- * - Suppose the type of the attribute is CD and maps to type DeltaRational.
- *   Well it can't map to a DeltaRational, and it thus it will be a
- *   DeltaRational*
- *   However being context dependent means givening up cleanup functions.
- *   So this leaks memory.
- * - Suppose the type of the attribute is CD and the type mapped to
- *   was a Node wrapping a CONST_DELTA_RATIONAL.
- *   This was rejected for inefficiency, and uglyness.
- *   Inefficiency: Every lookup and comparison will require going through the
- *   massaging in between a node and the constant being wrapped. Every update
- *   requires going through the additional expense of creating at least 1 node.
- *   The Uglyness: If this was chosen it would also suggest using comparisons
- *   against DeltaRationals for the tracking the constraints for conflict
- *   analysis. This seems to invite misuse and introducing Nodes that should
- *   probably not escape arith.
- * - Suppose that the of the attribute was not CD and mapped to a
- *   CDO<DeltaRational*> or similarly a ContextObj that wraps a DeltaRational*.
- *   This is currently rejected just because this is difficult to get right,
- *   and maintain. However with enough effort this the best solution is
- *   probably of this form.
- */
-
-
-/**
- * This is the literal that was asserted in the current context to the theory
- * that asserted the tightest lower bound on a variable.
- * For example: for a variable x this could be the constraint
- *    (>= x 4) or (not (<= x 50))
- * Note the strong correspondence between this and LowerBoundMap.
- * This is used during conflict analysis.
- */
-// struct LowerConstraintAttrID {};
-// typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint;
-
-/**
- * See the documentation for LowerConstraint.
- */
-// struct UpperConstraintAttrID {};
-// typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint;
-
-// struct TheoryArithPropagatedID {};
-// typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
-
-// struct HasHadABoundID {};
-// typedef expr::Attribute<HasHadABoundID, bool> HasHadABound;
-
-}; /*namespace partial_model*/
-
-
-
 class ArithPartialModel {
 private:
 
@@ -135,6 +51,8 @@ private:
   context::CDVector<TNode> d_upperConstraint;
   context::CDVector<TNode> d_lowerConstraint;
 
+  bool d_deltaIsSafe;
+  Rational d_delta;
 
   /**
    * List contains all of the variables that have an unsafe assignment.
@@ -154,6 +72,8 @@ public:
     d_lowerBound(c, false),
     d_upperConstraint(c,false),
     d_lowerConstraint(c,false),
+    d_deltaIsSafe(false),
+    d_delta(-1,1),
     d_history()
   { }
 
@@ -163,7 +83,6 @@ public:
   TNode getUpperConstraint(ArithVar x);
 
 
-
   /* Initializes a variable to a safe value.*/
   void initialize(ArithVar x, const DeltaRational& r);
 
@@ -211,14 +130,24 @@ public:
 
   void printModel(ArithVar x);
 
+  /** returns true iff x has both a lower and upper bound. */
   bool hasBounds(ArithVar x);
 
   bool hasEverHadABound(ArithVar var){
     return d_hasHadABound[var];
   }
 
+  const Rational& getDelta(){
+    if(!d_deltaIsSafe){
+      computeDelta();
+    }
+    return d_delta;
+  }
+
 private:
 
+  void computeDelta();
+
   /**
    * This function implements the mostly identical:
    * revertAssignmentChanges() and commitAssignmentChanges().