Delay QuantifiersEngine and UF strong solver initialization until after final options...

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 395d51d3e9f87177d88fc4a8e8682b7f5f04bbbd..239385bfc35f208fa7b6813943945abf5445d997 100644 (file)
--- 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 2408094d84ffbc86feed963510cc474ec186ebf0..428c101a6399d3499da8c55221b726d96c9ac29f 100644 (file)
--- 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 002d503d080f7a226adcd79a192e4d7fd90603cc..40a336a4ae86818835b7cfc75a5f1fde6fbd7b6e 100644 (file)
--- 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 71061034677a827ebb8a631841df5f068d4989aa..7ff93b02189b6bc9ac7cc39c78d965cdcc685245 100644 (file)
--- 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);

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3aee023167ce66793c0f68c3a318e49e62e70fa4..b82216378e400d72e40d537ba42cd2c0c74882b7 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -49,8 +49,8 @@ const bool d_solveWrite2 = false;
   //bool d_lazyRIntro1 = true;
   //bool d_eagerIndexSplitting = false;
 
-TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
-  Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, qe),
+TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+  Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo),
   d_numRow("theory::arrays::number of Row lemmas", 0),
   d_numExt("theory::arrays::number of Ext lemmas", 0),
   d_numProp("theory::arrays::number of propagations", 0),

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index e0191ccc940f7f1442f4280c914854e7bef686a5..a4029dc2e0a822d13d5f5bb55a079b693471b584 100644 (file)
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -128,7 +128,7 @@ class TheoryArrays : public Theory {
 
   public:
 
-  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
   ~TheoryArrays();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);

diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 49bf905c09c8b1a7f4157f544c33f1943df750bb..a8c904fe32dffe3fe37b8cb0930358e65c2977fb 100644 (file)
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -28,8 +28,8 @@ namespace booleans {
 
 class TheoryBool : public Theory {
 public:
-  TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
-    Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, qe) {
+  TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+    Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) {
   }
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);

diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index b49147c91e1dcc4dab860081a827cc0af96c4c2f..3bc0a2ce13f6efc9b7e5daf11a4818c827f0f07b 100644 (file)
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -27,8 +27,8 @@ namespace builtin {
 
 class TheoryBuiltin : public Theory {
 public:
-  TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
-    Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, qe) {}
+  TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+    Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {}
   std::string identify() const { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */
 

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 14a19f2d0c8f8fdc057f14b31cac7d345d6f91aa..6daf99c8b3bee9e7e864e71a2ce2d51213d381fc 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -35,8 +35,8 @@ using namespace CVC4::context;
 using namespace std;
 using namespace CVC4::theory::bv::utils;
 
-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
-  : Theory(THEORY_BV, c, u, out, valuation, logicInfo, qe),
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
+  : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
     d_context(c),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 90093edfd38c9e043cb39da1293c6d7d8d52e86d..3d093c86128e50da010d1f34ab557ecfea1be847 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -48,7 +48,7 @@ class TheoryBV : public Theory {
   __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; 
 public:
 
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
   ~TheoryBV();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 3c9fd7bd24f2dd9c68cebd85afab6413d612f40f..a3339f9a9bfb73219e7224aaf4df3d7df700b43e 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -39,8 +39,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::datatypes;
 
 
-TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
-  Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, qe),
+TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+  Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
   d_cycle_check(c),
   d_hasSeenCycle(c, false),
   d_infer(c),

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 4f061507c0660ef7b249a8c58bf5c1dc263f9f5b..d094451b892262884484a3bb03fa62603a66ce16 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -181,8 +181,9 @@ protected:
   /** compute care graph */
   void computeCareGraph();
 public:
-  TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation,
-                  const LogicInfo& logicInfo, QuantifiersEngine* qe);
+  TheoryDatatypes(context::Context* c, context::UserContext* u,
+                  OutputChannel& out, Valuation valuation,
+                  const LogicInfo& logicInfo);
   ~TheoryDatatypes();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);

diff --git a/src/theory/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp
index 03748d567eb1238df2056212274be9a677d52dd7..20f190486c71f7034681b3cb97a2f70e60637a7f 100644 (file)
--- a/src/theory/example/theory_uf_tim.cpp
+++ b/src/theory/example/theory_uf_tim.cpp
@@ -25,8 +25,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 using namespace CVC4::theory::uf::tim;
 
-TheoryUFTim::TheoryUFTim(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, QuantifiersEngine* qe) :
-  Theory(THEORY_UF, c, u, out, valuation, qe),
+TheoryUFTim::TheoryUFTim(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
+  Theory(THEORY_UF, c, u, out, valuation),
   d_assertions(c),
   d_pending(c),
   d_currentPendingIdx(c,0),

diff --git a/src/theory/example/theory_uf_tim.h b/src/theory/example/theory_uf_tim.h
index 64639bbfa6600e7b7881aba86efe44e6ffcc8d54..d24c0787d70acb2a71aee1ab3b25d4319e51d3c2 100644 (file)
--- a/src/theory/example/theory_uf_tim.h
+++ b/src/theory/example/theory_uf_tim.h
@@ -83,7 +83,7 @@ private:
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUFTim(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, QuantifiersEngine* qe);
+  TheoryUFTim(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
 
   /** Destructor for the TheoryUF object. */
   ~TheoryUFTim();

diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index 987973bf3333dda5f32a93c8928c88ec6f4e5e77..11aa2d8a579d0bcc1726812310d9d17c865744c4 100644 (file)
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -29,8 +29,8 @@ using namespace theory;
 using namespace idl;
 
 TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
-                     Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
-: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe)
+                     Valuation valuation, const LogicInfo& logicInfo)
+: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
 , d_model(c)
 , d_assertionsDB(c)
 {}

diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h
index 4597d4c6abaf74a26a492095a23e031cd49b043a..1eea28069b65904151c74d7fec8356352973a14f 100644 (file)
--- a/src/theory/idl/theory_idl.h
+++ b/src/theory/idl/theory_idl.h
@@ -45,7 +45,7 @@ public:
 
   /** Theory constructor. */
   TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
-            Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+            Valuation valuation, const LogicInfo& logicInfo);
 
   /** Pre-processing of input atoms */
   Node ppRewrite(TNode atom);

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index e72242fe9c1f2088f049971312067316acfd0eb4..6a3a6fca1d2ea175769c5598e82b9c5ea58b589b 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -33,8 +33,8 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
-  Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, qe),
+TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+  Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
   d_numRestarts(0),
   d_masterEqualityEngine(0)
 {

diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 8ebde136d1e5dc3b711ff585347a31c2f912ca90..8ace5f181b15e1b30936aef0a39f37b69bce4092 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -54,7 +54,7 @@ private:
   eq::EqualityEngine* d_masterEqualityEngine;
 
 public:
-  TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+  TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
   ~TheoryQuantifiers();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);

diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
index 0a89e251850e6096fdfee07a17d268c078687be7..df74ea8b3316c3fda8f9d679d6c580ba56b33d66 100644 (file)
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules.cpp
@@ -129,12 +129,11 @@ TheoryRewriteRules::TheoryRewriteRules(context::Context* c,
                                        context::UserContext* u,
                                        OutputChannel& out,
                                        Valuation valuation,
-                                       const LogicInfo& logicInfo,
-                                       QuantifiersEngine* qe) :
-  Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo, qe),
+                                       const LogicInfo& logicInfo) :
+  Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo),
   d_rules(c), d_ruleinsts(c), d_guardeds(c), d_checkLevel(c,0),
   d_explanations(c), d_ruleinsts_to_add(), d_ppAssert_on(false)
-  {
+{
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 }

diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index a542214b26421d0b9186e8b459e45ef20380a0c3..ea9eb4769f27bbd0ad515ba62329bd8bf2558487 100644 (file)
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -198,8 +198,7 @@ private:
                      context::UserContext* u,
                      OutputChannel& out,
                      Valuation valuation,
-                     const LogicInfo& logicInfo,
-                     QuantifiersEngine* qe);
+                     const LogicInfo& logicInfo);
 
   /** Usual function for theories */
   void check(Theory::Effort e);

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 231173058625d9a94aa84553e27845455afde48e..dbda080cca31a1278541a969545a0a8e65730449 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -33,8 +33,8 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
-    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, qe),
+TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
+    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
     d_notify( *this ),
     d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"),
     d_conflict( c, false ),

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index c0a979cb02db4ecb37d63ff5eb018bb5e38d3fce..824dbcb37bdbbce63d7d5cd968c5d9456e4ad02c 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -42,7 +42,7 @@ class TheoryStrings : public Theory {
        typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
 
 public:
-       TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+       TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
        ~TheoryStrings();
 
        void setMasterEqualityEngine(eq::EqualityEngine* eq);

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 43d35ac9dc4d89eb1da6a20bb49f934ebdc0d3d1..2359d5d86f6a0f018938b447aee45a131d66ef66 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -239,8 +239,7 @@ protected:
    * Construct a Theory.
    */
   Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
-         OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
-         QuantifiersEngine* qe, eq::EqualityEngine* master = 0) throw()
+         OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) throw()
   : d_id(id)
   , d_satContext(satContext)
   , d_userContext(userContext)
@@ -248,8 +247,8 @@ protected:
   , d_facts(satContext)
   , d_factsHead(satContext, 0)
   , d_sharedTermsIndex(satContext, 0)
-  , d_careGraph(0)
-  , d_quantEngine(qe)
+  , d_careGraph(NULL)
+  , d_quantEngine(NULL)
   , d_computeCareGraphTime(statName(id, "computeCareGraphTime"))
   , d_sharedTerms(satContext)
   , d_out(&out)
@@ -473,6 +472,14 @@ public:
     return d_quantEngine;
   }
 
+  /**
+   * Finish theory initialization.  At this point, options and the logic
+   * setting are final, and the master equality engine and quantifiers
+   * engine (if any) are initialized.  This base class implementation
+   * does nothing.
+   */
+  virtual void finishInit() { }
+
   /**
    * Pre-register a term.  Done one time for a Node, ever.
    */
@@ -497,6 +504,13 @@ public:
    */
   virtual void setMasterEqualityEngine(eq::EqualityEngine* eq) { }
 
+  /**
+   * Called to set the quantifiers engine.
+   */
+  virtual void setQuantifiersEngine(QuantifiersEngine* qe) {
+    d_quantEngine = qe;
+  }
+
   /**
    * Return the current theory care graph. Theories should overload computeCareGraph to do
    * the actual computation, and use addCarePair to add pairs to the care graph.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ff84e63b7673909611278465322636cc9ea6150a..47ba50aadfa1839a9a31d6047222e27b4f06766e 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -60,6 +60,9 @@ using namespace CVC4;
 using namespace CVC4::theory;
 
 void TheoryEngine::finishInit() {
+  // initialize the quantifiers engine
+  d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
+
   if (d_logicInfo.isQuantified()) {
     d_quantEngine->finishInit();
     Assert(d_masterEqualityEngine == 0);
@@ -67,10 +70,17 @@ void TheoryEngine::finishInit() {
 
     for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
       if (d_theoryTable[theoryId]) {
+        d_theoryTable[theoryId]->setQuantifiersEngine(d_quantEngine);
         d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
       }
     }
   }
+
+  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
+    if (d_theoryTable[theoryId]) {
+      d_theoryTable[theoryId]->finishInit();
+    }
+  }
 }
 
 void TheoryEngine::eqNotifyNewClass(TNode t){
@@ -146,9 +156,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
     d_theoryOut[theoryId] = NULL;
   }
 
-  // initialize the quantifiers engine
-  d_quantEngine = new QuantifiersEngine(context, userContext, this);
-
   // build model information if applicable
   d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true);
   d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 8f292e0080a31f412ba176ed3fee3262c055832f..d5de8e3b2f96ba70b32c504c79d41149ca7c57b4 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -488,7 +488,7 @@ public:
   inline void addTheory(theory::TheoryId theoryId) {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
     d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
-    d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo, getQuantifiersEngine());
+    d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo);
   }
 
   inline void setPropEngine(prop::PropEngine* propEngine) {

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index fd46ed7f4197462c324538b6f955ca09439512d0..bb948d785d4d44e842f7b47cdf3b64b936c75d88 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -28,12 +28,12 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 
 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-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),
+TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+  Theory(THEORY_UF, c, u, out, valuation, logicInfo),
   d_notify(*this),
   /* The strong theory solver can be notified by EqualityEngine::init(),
    * so make sure it's initialized first. */
-  d_thss(options::finiteModelFind() ? new StrongSolverTheoryUF(c, u, out, this) : NULL),
+  d_thss(NULL),
   d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
   d_conflict(c, false),
   d_literalsToPropagate(c),
@@ -49,6 +49,13 @@ void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
 
+void TheoryUF::finishInit() {
+  // initialize the strong solver
+  if (options::finiteModelFind()) {
+    d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this);
+  }
+}
+
 static Node mkAnd(const std::vector<TNode>& conjunctions) {
   Assert(conjunctions.size() > 0);
 

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 2c9b4b7d5fbc7c5cf718c2f6e237f36d88b0da2b..b9ca171541e4b619362846044fd1f72a0ddedd07 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -174,7 +174,7 @@ private:
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+  TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
 
   ~TheoryUF() {
     // destruct all ppRewrite() callbacks
@@ -186,6 +186,7 @@ public:
   }
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
+  void finishInit();
 
   void check(Effort);
   void preRegisterTerm(TNode term);

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 3247b8c736f44c13d2d15820b93be47f83d4745c..c99c66fff3d916426be9049b2e20cf3b5c74dc8a 100644 (file)
--- 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 99dc17594bc00c72a783b3a560c36b6c76c291b9..803b245274786218d0c823063d836a3b2fa0e2ee 100644 (file)
--- 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 a824a3f68eec470dcccd9195f3daa87a6edd6572..e2dfcc46467042e5599f3cb9054f9b0973620df6 100644 (file)
--- 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);