summaryrefslogtreecommitdiff
path: root/src/theory/registrar.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/registrar.h')
-rw-r--r--src/theory/registrar.h31
1 files changed, 31 insertions, 0 deletions
diff --git a/src/theory/registrar.h b/src/theory/registrar.h
new file mode 100644
index 000000000..ce3a301d7
--- /dev/null
+++ b/src/theory/registrar.h
@@ -0,0 +1,31 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_REGISTRAR_H
+#define __CVC4__THEORY_REGISTRAR_H
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+class Registrar {
+private:
+ TheoryEngine* d_theoryEngine;
+
+public:
+ Registrar() : d_theoryEngine(NULL){ }
+
+ Registrar(TheoryEngine* te) : d_theoryEngine(te){ }
+
+ void preRegister(Node n){
+ if(d_theoryEngine != NULL){
+ d_theoryEngine->preRegister(n);
+ }
+ }
+
+};/* class Registrar */
+
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY_REGISTRAR_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback