Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

2 files changed, 3 insertions, 3 deletions

diff --git a/src/theory/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp
index 03787703a..638a03478 100644
--- a/src/theory/example/theory_uf_tim.cpp
+++ b/src/theory/example/theory_uf_tim.cpp
@@ -27,8 +27,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) :
-  Theory(THEORY_UF, c, u, out, valuation),
+TheoryUFTim::TheoryUFTim(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, QuantifiersEngine* qe) :
+  Theory(THEORY_UF, c, u, out, valuation, qe),
   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 b47536f07..41e58349a 100644
--- a/src/theory/example/theory_uf_tim.h
+++ b/src/theory/example/theory_uf_tim.h
@@ -85,7 +85,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);
+  TheoryUFTim(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, QuantifiersEngine* qe);
 
   /** Destructor for the TheoryUF object. */
   ~TheoryUFTim();