Delay QuantifiersEngine and UF strong solver initialization until after final options/logic are set.

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);