diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-01-22 10:06:04 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-01-22 11:29:58 -0500 |
| commit | 02efc4635cc200deb7884e55bf62feb7f19248b8 (patch) | |
| tree | 3bd688f325b3f0f8fab0e1a105b1d5aae4b22019 /test/unit | |
| parent | 8d5aa1c32c047ec023375284fac40d41347fe643 (diff) | |
Delay QuantifiersEngine and UF strong solver initialization until after final options/logic are set.
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/theory/theory_arith_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/theory_engine_white.h | 4 | ||||
| -rw-r--r-- | test/unit/theory/theory_white.h | 6 |
3 files changed, 6 insertions, 6 deletions
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 3247b8c73..c99c66fff 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -115,7 +115,7 @@ public: d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL; d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL; - d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_smt->d_theoryEngine->d_quantEngine); + d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo); preregistered = new std::set<Node>(); diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 99dc17594..803b24527 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -120,8 +120,8 @@ class FakeTheory : public Theory { // static std::deque<RewriteItem> s_expected; public: - FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : - Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, qe) + FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo) { } /** Register an expected rewrite call */ diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index a824a3f68..e2dfcc464 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -119,8 +119,8 @@ public: set<Node> d_registered; vector<Node> d_getSequence; - DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : - Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, qe) { + DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo) { } void registerTerm(TNode n) { @@ -196,7 +196,7 @@ public: d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL; d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL; - d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo, NULL); + d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo); d_outputChannel.clear(); atom0 = d_nm->mkConst(true); atom1 = d_nm->mkConst(false); |