diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-09 01:38:48 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-09 01:38:48 +0000 |
| commit | 878f71272c06cf605fb3d2f4e66eaea55aa32127 (patch) | |
| tree | 162ac5a74e14bae02ae74cec8f621174c22323e2 /src/smt | |
| parent | 86f2a3e111137fecaf942050dfd7ade0c881d6eb (diff) | |
surprize surprize
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 13 |
1 files changed, 1 insertions, 12 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4185765a8..d85f28b23 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -45,8 +45,6 @@ #include "theory/booleans/theory_bool.h" #include "theory/booleans/circuit_propagator.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" @@ -199,16 +197,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_theoryEngine->addTheory<theory::arrays::TheoryArrays>(); d_theoryEngine->addTheory<theory::bv::TheoryBV>(); d_theoryEngine->addTheory<theory::datatypes::TheoryDatatypes>(); - switch(Options::current()->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(Options::current()->uf_implementation); - } + d_theoryEngine->addTheory<theory::uf::TheoryUF>(); d_propEngine = new PropEngine(d_theoryEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); |