diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
commit | f9a4fe48a4ec2355f8fec93d3f47242577df2511 (patch) | |
tree | eb49b7760b16aa17666d59464c96979b445fbcc8 /src/smt | |
parent | eecc1e4f301711dbb2bf1508ea0ba6cd20acd593 (diff) |
Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6bfdda079..273b2322a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -36,6 +36,15 @@ #include "util/exception.h" #include "util/options.h" #include "util/output.h" +#include "theory/builtin/theory_builtin.h" +#include "theory/booleans/theory_bool.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/morgan/theory_uf_morgan.h" +#include "theory/uf/tim/theory_uf_tim.h" +#include "theory/arith/theory_arith.h" +#include "theory/arrays/theory_arrays.h" +#include "theory/bv/theory_bv.h" + using namespace std; using namespace CVC4; @@ -133,6 +142,24 @@ void SmtEngine::init(const Options& opts) throw() { // We have mutual dependancy here, so we add the prop engine to the theory // engine later (it is non-essential there) d_theoryEngine = new TheoryEngine(d_context, opts); + + // Add the theories + d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(); + d_theoryEngine->addTheory<theory::booleans::TheoryBool>(); + d_theoryEngine->addTheory<theory::arith::TheoryArith>(); + d_theoryEngine->addTheory<theory::arrays::TheoryArrays>(); + d_theoryEngine->addTheory<theory::bv::TheoryBV>(); + switch(opts.uf_implementation) { + case Options::TIM: + d_theoryEngine->addTheory<theory::uf::tim::TheoryUFTim>(); + break; + case Options::MORGAN: + d_theoryEngine->addTheory<theory::uf::morgan::TheoryUFMorgan>(); + break; + default: + Unhandled(opts.uf_implementation); + } + d_propEngine = new PropEngine(d_theoryEngine, d_context, opts); d_theoryEngine->setPropEngine(d_propEngine); |