From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 28 Feb 2012 19:51:10 +0000 (+0000)
Subject: Replace the sequence of hardcoded addTheory() calls with a use of the theory traits... 
X-Git-Tag: cvc5-1.0.0~8301
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c492f41a58c1299105d58a3561afccd09e0532bc;p=cvc5.git

Replace the sequence of hardcoded addTheory() calls with a use of the theory traits---with the effect that everything with a kinds file is registered as a theory.  Eventually we may want a more dynamic way of selecting theory implementations, but for now we don't have a need for this.  Expected performance impact: none.  (This commit addresses and re-closes the reopened bug #307.)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5a7209c40..7bf22c2c0 100644
--- 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);