diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-05 04:06:10 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-05 04:06:10 +0000 |
commit | bc3269ad3680436ede31a70803ff5879c9e4bf6e (patch) | |
tree | 867ea6d43ba8bf9d6f0906cd74a563f62f2c39b0 /src/theory | |
parent | 41dddac33ba0332a2ab52983b94044cbdc9e762e (diff) |
Minor adjustments to the Registrar commit in 1644, documentation.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/registrar.h | 39 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 8 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 6 |
3 files changed, 38 insertions, 15 deletions
diff --git a/src/theory/registrar.h b/src/theory/registrar.h index ce3a301d7..19315827e 100644 --- a/src/theory/registrar.h +++ b/src/theory/registrar.h @@ -1,7 +1,30 @@ +/********************* */ +/*! \file registrar.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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.\endverbatim + ** + ** \brief Class to encapsulate preregistration duties + ** + ** Class to encapsulate preregistration duties. This class permits the + ** CNF stream implementation to reach into the theory engine to + ** preregister only those terms with an associated SAT literal (at the + ** point when they get the SAT literal), without having to refer to the + ** TheoryEngine class directly. + **/ + #include "cvc4_private.h" -#ifndef __CVC4__THEORY_REGISTRAR_H -#define __CVC4__THEORY_REGISTRAR_H +#ifndef __CVC4__THEORY__REGISTRAR_H +#define __CVC4__THEORY__REGISTRAR_H + #include "theory/theory_engine.h" namespace CVC4 { @@ -12,20 +35,16 @@ private: TheoryEngine* d_theoryEngine; public: - Registrar() : d_theoryEngine(NULL){ } - Registrar(TheoryEngine* te) : d_theoryEngine(te){ } + Registrar(TheoryEngine* te) : d_theoryEngine(te) { } - void preRegister(Node n){ - if(d_theoryEngine != NULL){ - d_theoryEngine->preRegister(n); - } + void preRegister(Node n) { + d_theoryEngine->preRegister(n); } };/* class Registrar */ - }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY_REGISTRAR_H */ +#endif /* __CVC4__THEORY__REGISTRAR_H */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index aa70a9bda..cb29bb98e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -137,6 +137,10 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) : d_incomplete(ctxt, false), d_statistics() { + for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + d_theoryTable[theoryId] = NULL; + } + Rewriter::init(); d_sharedTermManager = new SharedTermManager(this, ctxt); @@ -145,8 +149,8 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) : TheoryEngine::~TheoryEngine() { Assert(d_hasShutDown); - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++ theoryId) { - if (d_theoryTable[theoryId]) { + for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + if(d_theoryTable[theoryId]) { delete d_theoryTable[theoryId]; } } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2e12d3a16..1cdae3810 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -85,7 +85,7 @@ class TheoryEngine { d_engine(engine), d_context(context), d_conflictNode(context), - d_explanationNode(context){ + d_explanationNode(context) { } void newFact(TNode n); @@ -212,8 +212,8 @@ public: d_hasShutDown = true; // Shutdown all the theories - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++ theoryId) { - if (d_theoryTable[theoryId]) { + for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + if(d_theoryTable[theoryId]) { d_theoryTable[theoryId]->shutdown(); } } |