Replace the sequence of hardcoded addTheory() calls with a use of the theory traits...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5a7209c409b4c73286375c3ee015c29376f098b6..7bf22c2c05d4175877e6543cc4532d2a7ac0c45e 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -51,6 +51,7 @@
 #include "theory/arrays/theory_arrays.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/datatypes/theory_datatypes.h"
+#include "theory/theory_traits.h"
 #include "util/ite_removal.h"
 
 using namespace std;
@@ -218,13 +219,12 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_theoryEngine = new TheoryEngine(d_context, d_userContext);
 
   // Add the theories
-  d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
-  d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL);
-  d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
-  d_theoryEngine->addTheory<theory::arrays::TheoryArrays>(theory::THEORY_ARRAY);
-  d_theoryEngine->addTheory<theory::bv::TheoryBV>(theory::THEORY_BV);
-  d_theoryEngine->addTheory<theory::datatypes::TheoryDatatypes>(theory::THEORY_DATATYPES);
-  d_theoryEngine->addTheory<theory::uf::TheoryUF>(theory::THEORY_UF);
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+    d_theoryEngine->addTheory<theory::TheoryTraits<THEORY>::theory_class>(THEORY);
+  CVC4_FOR_EACH_THEORY;
 
   d_propEngine = new PropEngine(d_theoryEngine, d_context);
   d_theoryEngine->setPropEngine(d_propEngine);