diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-16 15:52:36 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-16 15:52:36 +0000 |
commit | 25396f93b7df85c80a39ed207483e28a8c86ff26 (patch) | |
tree | f271c1e856379810a14b4d0b476e716e8b6854ef | |
parent | aaa6a0b8d9807804a76db3eb6e9a218da55cf844 (diff) |
found a bug in the initialization order of UF, EqualityEngine, and the UF strong solver; fixed
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 11 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 2 |
2 files changed, 6 insertions, 7 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index ac194d5ed..d24878a62 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -31,6 +31,9 @@ using namespace CVC4::theory::uf; TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : Theory(THEORY_UF, c, u, out, valuation, logicInfo, qe), d_notify(*this), + /* The strong theory solver can be notified by EqualityEngine::init(), + * so make sure it's initialized first. */ + d_thss(Options::current()->finiteModelFind ? new StrongSolverTheoryUf(c, u, out, this) : NULL), d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"), d_conflict(c, false), d_literalsToPropagate(c), @@ -39,13 +42,7 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); - - if (Options::current()->finiteModelFind) { - d_thss = new StrongSolverTheoryUf(c, u, out, this); - } else { - d_thss = NULL; - } -}/* TheoryUF::TheoryUF() */ +} static Node mkAnd(const std::vector<TNode>& conjunctions) { Assert(conjunctions.size() > 0); diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index e2dd55174..e5cb7e4f8 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1062,6 +1062,8 @@ Node StrongSolverTheoryUf::ConflictFind::getCardinalityLemma(){ StrongSolverTheoryUf::StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) : d_out( &out ), d_th( th ), +d_conf_find(), +d_conf_types(), d_conf_find_init( c ) { |