diff options
Diffstat (limited to 'src/theory/uf/theory_uf.h')
-rw-r--r-- | src/theory/uf/theory_uf.h | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 8495e6c9c..5863a31fc 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -38,7 +38,7 @@ namespace CVC4 { namespace theory { namespace uf { -class TheoryUF : public TheoryImpl<TheoryUF> { +class TheoryUF : public Theory { private: @@ -176,31 +176,30 @@ private: /** Constructs a conflict from an inconsistent disequality. */ Node constructConflict(TNode diseq); -}; +};/* class TheoryUF */ /** * Cleanup function for ECData. This will be used for called whenever * a ECAttr is being destructed. */ -struct ECCleanupStrategy{ - static void cleanup(ECData* ec){ +struct ECCleanupStrategy { + static void cleanup(ECData* ec) { Debug("ufgc") << "cleaning up ECData " << ec << "\n"; ec->deleteSelf(); } -}; +};/* struct ECCleanupStrategy */ /** Unique name to use for constructing ECAttr. */ -struct EquivClass; +struct ECAttrTag {}; /** * ECAttr is the attribute that maps a node to an equivalence class. */ -typedef expr::Attribute<EquivClass, ECData*, ECCleanupStrategy > ECAttr; - -} /* CVC4::theory::uf namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr; +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__THEORY__UF__THEORY_UF_H */ |