diff options
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/ecdata.h | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_def.h | 31 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 7 |
4 files changed, 32 insertions, 10 deletions
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h index 9b87aa6cb..5bb3a57bd 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/ecdata.h @@ -14,6 +14,8 @@ ** Currently keeps a context dependent watch list. **/ +#include "cvc4_private.h" + #ifndef __CVC4__THEORY__UF__ECDATA_H #define __CVC4__THEORY__UF__ECDATA_H diff --git a/src/theory/uf/theory_def.h b/src/theory/uf/theory_def.h index 8e3f5e9f1..b5cdda4ec 100644 --- a/src/theory/uf/theory_def.h +++ b/src/theory/uf/theory_def.h @@ -1,7 +1,24 @@ -namespace CVC4 { - namespace theory { - namespace uf { - class TheoryUF; - } - } -} +/********************* */ +/** theory_def.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Definition for TheoryUF (for purposes of linking to the + ** theory-code-finding mechanisms in the parent directory). + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__UF__THEORY_DEF_H +#define __CVC4__THEORY__UF__THEORY_DEF_H + +#include "theory/uf/theory_uf.h" + +#endif /* __CVC4__THEORY__UF__THEORY_DEF_H */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 0c58d45e4..0c0559bb0 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -43,7 +43,9 @@ void TheoryUF::preRegisterTerm(TNode n){ void TheoryUF::registerTerm(TNode n){ d_registered.push_back(n); +#ifdef CVC4_DEBUG n.printAst(Warning()); +#endif /* CVC4_DEBUG */ ECData* ecN; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 34b6719d7..6efdf27c0 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -13,9 +13,10 @@ ** **/ +#include "cvc4_private.h" -#ifndef __CVC4__THEORY__THEORY_UF_H -#define __CVC4__THEORY__THEORY_UF_H +#ifndef __CVC4__THEORY__UF__THEORY_UF_H +#define __CVC4__THEORY__UF__THEORY_UF_H #include "expr/node.h" #include "expr/attribute.h" @@ -150,4 +151,4 @@ typedef expr::Attribute<EquivClass, ECData* /*, ECCleanupFcn*/> ECAttr; } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__THEORY_UF_H */ +#endif /* __CVC4__THEORY__UF__THEORY_UF_H */ |