From: Tim King <taking@cs.nyu.edu>
Date: Mon, 14 Feb 2011 02:47:01 +0000 (+0000)
Subject: Reverses the order of the d_possiblyInconsistent queue. (It is that old termination... 
X-Git-Tag: cvc5-1.0.0~8713
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=806e7bb725d8fecf7d7da87c05fdf19037d565a6;p=cvc5.git

Reverses the order of the d_possiblyInconsistent queue. (It is that old termination bug again. *le sigh*)
---

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index d8997af93..2ae6b091d 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -28,8 +28,9 @@ private:
       return a.second > b.second;
     }
   };
+  typedef std::priority_queue<VarDRatPair, std::vector<VarDRatPair>, VarDRatPairCompare> GriggioPQueue;
 
-  std::priority_queue<VarDRatPair, std::vector<VarDRatPair>, VarDRatPairCompare> d_griggioRuleQueue;
+  GriggioPQueue d_griggioRuleQueue;
 
   /**
    * Priority Queue of the basic variables that may be inconsistent.
@@ -37,8 +38,13 @@ private:
    * This is required to contain at least 1 instance of every inconsistent
    * basic variable. This is only required to be a superset though so its
    * contents must be checked to still be basic and inconsistent.
+   *
+   * This is also required to agree with the row on variable order for termination.
+   * Effectively this means that this must be a min-heap.
    */
-  std::priority_queue<ArithVar> d_possiblyInconsistent;
+  typedef std::priority_queue<ArithVar, vector<ArithVar>, std::greater<ArithVar> > PQueue;
+
+  PQueue d_possiblyInconsistent;
 
   /** Stores system wide constants to avoid unnessecary reconstruction. */
   const ArithConstants& d_constants;