Add identifiers for extended function reductions (#6314)

[cvc5.git] / src / context / cdtrail_queue.h

diff --git a/src/context/cdtrail_queue.h b/src/context/cdtrail_queue.h
index d709ccbcb5e80008fdeae24dfc363653fe1a15f4..abdd83f99633b7663afb524708d22a28c6c00058 100644 (file)
--- a/src/context/cdtrail_queue.h
+++ b/src/context/cdtrail_queue.h
@@ -2,10 +2,10 @@
 /*! \file cdtrail_queue.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Paul Meng
+ **   Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -17,18 +17,18 @@
  ** The implementation is currently not full featured.
  **/
 
-
 #include "cvc4_private.h"
 
-#ifndef __CVC4__CONTEXT__CDTRAIL_QUEUE_H
-#define __CVC4__CONTEXT__CDTRAIL_QUEUE_H
+#ifndef CVC4__CONTEXT__CDTRAIL_QUEUE_H
+#define CVC4__CONTEXT__CDTRAIL_QUEUE_H
 
-#include "context/context.h"
 #include "context/cdlist.h"
+#include "context/cdo.h"
 
-namespace CVC4 {
+namespace cvc5 {
 namespace context {
 
+class Context;
 
 template <class T>
 class CDTrailQueue {
@@ -74,7 +74,7 @@ public:
 
   /** Moves the iterator for the queue forward. */
   void dequeue(){
-    Assert(!empty(), "Attempting to queue from an empty queue.");
+    Assert(!empty()) << "Attempting to queue from an empty queue.";
     d_iter = d_iter + 1;
   }
 
@@ -89,7 +89,7 @@ public:
 
 };/* class CDTrailQueue<> */
 
-}/* CVC4::context namespace */
-}/* CVC4 namespace */
+}  // namespace context
+}  // namespace cvc5
 
-#endif /* __CVC4__CONTEXT__CDTRAIL_QUEUE_H */
+#endif /* CVC4__CONTEXT__CDTRAIL_QUEUE_H */