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 /src/theory/arith | |
parent | 8d5aa1c32c047ec023375284fac40d41347fe643 (diff) |
Delay QuantifiersEngine and UF strong solver initialization until after final options/logic are set.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 11 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 3 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 3 |
4 files changed, 18 insertions, 7 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 395d51d3e..239385bfc 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -25,9 +25,9 @@ namespace CVC4 { namespace theory { namespace arith { -TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe) - , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, qe)) +TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) + : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) + , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) {} TheoryArith::~TheoryArith(){ @@ -42,6 +42,11 @@ void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_internal->setMasterEqualityEngine(eq); } +void TheoryArith::setQuantifiersEngine(QuantifiersEngine* qe) { + this->Theory::setQuantifiersEngine(qe); + d_internal->setQuantifiersEngine(qe); +} + void TheoryArith::addSharedTerm(TNode n){ d_internal->addSharedTerm(n); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 2408094d8..428c101a6 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -45,7 +45,7 @@ private: KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer"); public: - TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); virtual ~TheoryArith(); /** @@ -54,6 +54,7 @@ public: void preRegisterTerm(TNode n); void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setQuantifiersEngine(QuantifiersEngine* qe); void check(Effort e); void propagate(Effort e); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 002d503d0..40a336a4a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -82,7 +82,7 @@ namespace CVC4 { namespace theory { namespace arith { -TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : +TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : d_containing(containing), d_nlIncomplete( false), d_rowTracking(), @@ -91,7 +91,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), d_learner(u), - d_quantEngine(qe), + d_quantEngine(NULL), d_assertionsThatDoNotMatchTheirLiterals(c), d_nextIntegerCheckVar(0), d_constantIntegerVariables(c), @@ -132,6 +132,10 @@ void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_congruenceManager.setMasterEqualityEngine(eq); } +void TheoryArithPrivate::setQuantifiersEngine(QuantifiersEngine* qe) { + d_quantEngine = qe; +} + Node TheoryArithPrivate::getRealDivideBy0Func(){ Assert(!getLogicInfo().isLinear()); Assert(getLogicInfo().areRealsUsed()); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 710610346..7ff93b021 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -350,7 +350,7 @@ private: Node ppRewriteTerms(TNode atom); public: - TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryArithPrivate(); /** @@ -359,6 +359,7 @@ public: void preRegisterTerm(TNode n); void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setQuantifiersEngine(QuantifiersEngine* qe); void check(Theory::Effort e); void propagate(Theory::Effort e); |