declare-sort, define-sort working but not thoroughly tested; define-fun half working...
[cvc5.git] / src / context / cdmap.h
index 76c05fd4df5eb33df9f414f7d27bb633cfa45015..1e7e931da259f6ea939aafaac65fa985be1a20f0 100644 (file)
 #ifndef __CVC4__CONTEXT__CDMAP_H
 #define __CVC4__CONTEXT__CDMAP_H
 
-#include "context/context.h"
-#include "util/Assert.h"
-
 #include <vector>
 #include <iterator>
 #include <ext/hash_map>
 
+#include "context/context.h"
+#include "util/Assert.h"
+#include "context/cdmap_forward.h"
+
 namespace CVC4 {
 namespace context {
 
 // Auxiliary class: almost the same as CDO (see cdo.h)
 
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
-
 template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
 class CDOmap : public ContextObj {
   friend class CDMap<Key, Data, HashFcn>;