From c492f41a58c1299105d58a3561afccd09e0532bc Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 28 Feb 2012 19:51:10 +0000 Subject: [PATCH] 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.) --- src/smt/smt_engine.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) 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::THEORY_BUILTIN); - d_theoryEngine->addTheory(theory::THEORY_BOOL); - d_theoryEngine->addTheory(theory::THEORY_ARITH); - d_theoryEngine->addTheory(theory::THEORY_ARRAY); - d_theoryEngine->addTheory(theory::THEORY_BV); - d_theoryEngine->addTheory(theory::THEORY_DATATYPES); - d_theoryEngine->addTheory(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_class>(THEORY); + CVC4_FOR_EACH_THEORY; d_propEngine = new PropEngine(d_theoryEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); -- 2.30.2