Changed how assignments are saved during check. These are now backed by an attribute. There is now a priority queue for selecting the smallest inconsistent basic variable. normal.h has been removed. A large chunk of the registerTerm() stuff has been moved into preregister. The lazy splitting code is now been commented out so that it stops showing up in profiling.

1 files changed, 32 insertions, 17 deletions

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 36567e86e..d04d8dd8c 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -37,7 +37,9 @@ namespace partial_model {
 struct DeltaRationalCleanupStrategy{
   static void cleanup(DeltaRational* dq){
     Debug("arithgc") << "cleaning up  " << dq << "\n";
-    delete dq;
+    if(dq != NULL){
+      delete dq;
+    }
   }
 };
 
@@ -46,6 +48,12 @@ 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
@@ -108,12 +116,11 @@ private:
   partial_model::CDDRationalMap d_LowerBoundMap;
   partial_model::CDDRationalMap d_UpperBoundMap;
 
-  typedef std::pair<TNode, DeltaRational> HistoryPair;
-  typedef std::deque< HistoryPair > HistoryStack;
 
-  HistoryStack d_history;
+  typedef std::vector<TNode> HistoryList;
+  HistoryList d_history;
 
-  bool d_savingAssignments;
+  bool d_unsafeMode;
 
 public:
 
@@ -121,7 +128,7 @@ public:
     d_LowerBoundMap(c),
     d_UpperBoundMap(c),
     d_history(),
-    d_savingAssignments(false)
+    d_unsafeMode(false)
   { }
 
   void setLowerConstraint(TNode x, TNode constraint);
@@ -130,11 +137,21 @@ public:
   TNode getUpperConstraint(TNode x);
 
 
-  void beginRecordingAssignments();
 
-  /* */
-  void stopRecordingAssignments(bool revert);
-  bool isRecording() { return d_savingAssignments;  }
+  void initialize(TNode x, const DeltaRational& r);
+
+  DeltaRational getSafeAssignment(TNode x) const;
+
+  bool isInUnsafeMode() { return d_unsafeMode;  }
+
+  void turnOnUnsafeMode();
+  void turnOffUnsafeMode();
+
+  void revertAssignmentChanges();
+  void commitAssignmentChanges();
+
+
+
 
   void setUpperBound(TNode x, const DeltaRational& r);
   void setLowerBound(TNode x, const DeltaRational& r);
@@ -143,20 +160,20 @@ public:
   /** Must know that the bound exists before calling this! */
   DeltaRational getUpperBound(TNode x) const;
   DeltaRational getLowerBound(TNode x) const;
-  DeltaRational getAssignment(TNode x) const;
+  const DeltaRational& getAssignment(TNode x) const;
 
 
   /**
    * x <= l
    * ? c < l
    */
-  bool belowLowerBound(TNode x, DeltaRational& c, bool strict);
+  bool belowLowerBound(TNode x, const DeltaRational& c, bool strict);
 
   /**
    * x <= u
    * ? c < u
    */
-  bool aboveUpperBound(TNode x, DeltaRational& c, bool strict);
+  bool aboveUpperBound(TNode x, const DeltaRational& c, bool strict);
 
   bool strictlyBelowUpperBound(TNode x);
   bool strictlyAboveLowerBound(TNode x);
@@ -164,10 +181,8 @@ public:
 
   void printModel(TNode x);
 
-  void initialize(TNode x, const DeltaRational& r);
-  
-  DeltaRational getSavedAssignment(TNode x) const;
-
+private:
+  void clearSafeAssignments(bool revert);
 };