1 files changed, 85 insertions, 3 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 7583f8ee7..dc7bb7c92 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -18,6 +18,8 @@
  **/
 
 #include "theory/uf/theory_uf.h"
+#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/uf/theory_uf_strong_solver.h"
 
 using namespace std;
 using namespace CVC4;
@@ -25,8 +27,8 @@ 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) :
-  Theory(THEORY_UF, c, u, out, valuation, logicInfo),
+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),
   d_notify(*this),
   d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
   d_conflict(c, false),
@@ -36,6 +38,12 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel&
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
+
+  if (Options::current()->finiteModelFind) {
+    d_thss = new StrongSolverTheoryUf(c, u, out, this);
+  } else {
+    d_thss = NULL;
+  }
 }/* TheoryUF::TheoryUF() */
 
 static Node mkAnd(const std::vector<TNode>& conjunctions) {
@@ -62,29 +70,46 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) {
 
 void TheoryUF::check(Effort level) {
 
-  while (!done() && !d_conflict) 
+  while (!done() && !d_conflict)
   {
     // Get all the assertions
     Assertion assertion = get();
     TNode fact = assertion.assertion;
 
     Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
+    if (d_thss != NULL) {
+      bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
+      d_thss->assertNode(fact, isDecision);
+    }
 
     // Do the work
     bool polarity = fact.getKind() != kind::NOT;
     TNode atom = polarity ? fact : fact[0];
     if (atom.getKind() == kind::EQUAL) {
       d_equalityEngine.assertEquality(atom, polarity, fact);
+    } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT) {
+      // do nothing
     } else {
       d_equalityEngine.assertPredicate(atom, polarity, fact);
     }
   }
 
+
+  if (d_thss != NULL) {
+    if (! d_conflict) {
+      d_thss->check(level);
+    }
+  }
+
 }/* TheoryUF::check() */
 
 void TheoryUF::preRegisterTerm(TNode node) {
   Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
 
+  if (d_thss != NULL) {
+    d_thss->preRegisterTerm(node);
+  }
+
   switch (node.getKind()) {
   case kind::EQUAL:
     // Add the trigger for equality
@@ -124,6 +149,12 @@ bool TheoryUF::propagate(TNode literal) {
   return ok;
 }/* TheoryUF::propagate(TNode) */
 
+void TheoryUF::propagate(Effort effort) {
+  if (d_thss != NULL) {
+    return d_thss->propagate(effort);
+  }
+}
+
 void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;
@@ -395,3 +426,54 @@ void TheoryUF::conflict(TNode a, TNode b) {
   d_out->conflict(d_conflictNode);
   d_conflict = true;
 }
+
+void TheoryUF::eqNotifyNewClass(TNode t) {
+  if (d_thss != NULL) {
+    d_thss->newEqClass(t);
+  }
+  // this can be called very early, during initialization
+  if (!getLogicInfo().isLocked() || getLogicInfo().isQuantified()) {
+    ((InstantiatorTheoryUf*) getInstantiator())->newEqClass(t);
+  }
+}
+
+void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) {
+  if (getLogicInfo().isQuantified()) {
+    ((InstantiatorTheoryUf*) getInstantiator())->merge(t1, t2);
+  }
+}
+
+void TheoryUF::eqNotifyPostMerge(TNode t1, TNode t2) {
+  if (d_thss != NULL) {
+    d_thss->merge(t1, t2);
+  }
+}
+
+void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+  if (d_thss != NULL) {
+    d_thss->assertDisequal(t1, t2, reason);
+  }
+  if (getLogicInfo().isQuantified()) {
+    ((InstantiatorTheoryUf*) getInstantiator())->assertDisequal(t1, t2, reason);
+  }
+}
+
+Node TheoryUF::ppRewrite(TNode node) {
+
+  if (node.getKind() != kind::APPLY_UF) {
+    return node;
+  }
+
+  // perform the callbacks requested by TheoryUF::registerPpRewrite()
+  RegisterPpRewrites::iterator c = d_registeredPpRewrites.find(node.getOperator());
+  if (c == d_registeredPpRewrites.end()) {
+    return node;
+  } else {
+    Node res = c->second->ppRewrite(node);
+    if (res != node) {
+      return ppRewrite(res);
+    } else {
+      return res;
+    }
+  }
+}