diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 388167e00..384e2fdd6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -21,6 +21,7 @@ #include "expr/attribute.h" #include "theory/theory.h" #include "expr/node_builder.h" +#include "smt/options.h" #include <vector> #include <list> @@ -116,6 +117,57 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { } } +TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) : + d_propEngine(NULL), + d_theoryOut(this, ctxt), + d_hasShutDown(false), + d_statistics() { + + d_sharedTermManager = new SharedTermManager(this, ctxt); + + d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut); + d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut); + switch(opts->uf_implementation) { + case Options::TIM: + d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut); + break; + case Options::MORGAN: + d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut); + break; + default: + Unhandled(opts->uf_implementation); + } + d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut); + d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut); + d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut); + + d_sharedTermManager->registerTheory(d_builtin); + d_sharedTermManager->registerTheory(d_bool); + d_sharedTermManager->registerTheory(d_uf); + d_sharedTermManager->registerTheory(d_arith); + d_sharedTermManager->registerTheory(d_arrays); + d_sharedTermManager->registerTheory(d_bv); + + d_theoryOfTable.registerTheory(d_builtin); + d_theoryOfTable.registerTheory(d_bool); + d_theoryOfTable.registerTheory(d_uf); + d_theoryOfTable.registerTheory(d_arith); + d_theoryOfTable.registerTheory(d_arrays); + d_theoryOfTable.registerTheory(d_bv); +} + +TheoryEngine::~TheoryEngine() { + Assert(d_hasShutDown); + + delete d_bv; + delete d_arrays; + delete d_arith; + delete d_uf; + delete d_bool; + delete d_builtin; + + delete d_sharedTermManager; +} Theory* TheoryEngine::theoryOf(TypeNode t) { // FIXME: we don't yet have a Type-to-Theory map. When we do, |