1 files changed, 70 insertions, 3 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 5b8470567..a1500e084 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -23,6 +23,7 @@
 #include "theory/uf/theory_uf_instantiator.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/model.h"
+#include "theory/type_enumerator.h"
 
 using namespace std;
 using namespace CVC4;
@@ -80,6 +81,10 @@ void TheoryUF::check(Effort level) {
     if (d_thss != NULL) {
       bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
       d_thss->assertNode(fact, isDecision);
+      if( d_thss->isConflict() ){
+        d_conflict = true;
+        return;
+      }
     }
 
     // Do the work
@@ -98,6 +103,9 @@ void TheoryUF::check(Effort level) {
   if (d_thss != NULL) {
     if (! d_conflict) {
       d_thss->check(level);
+      if( d_thss->isConflict() ){
+        d_conflict = true;
+      }
     }
   }
 
@@ -127,6 +135,9 @@ void TheoryUF::preRegisterTerm(TNode node) {
     // Remember the function and predicate terms
     d_functionsTerms.push_back(node);
     break;
+  case kind::CARDINALITY_CONSTRAINT:
+    //do nothing
+    break;
   default:
     // Variables etc
     d_equalityEngine.addTerm(node);
@@ -150,8 +161,16 @@ bool TheoryUF::propagate(TNode literal) {
 }/* TheoryUF::propagate(TNode) */
 
 void TheoryUF::propagate(Effort effort) {
-  if (d_thss != NULL) {
-    return d_thss->propagate(effort);
+  //if (d_thss != NULL) {
+  //  return d_thss->propagate(effort);
+  //}
+}
+
+Node TheoryUF::getNextDecisionRequest(){
+  if (d_thss != NULL && !d_conflict) {
+    return d_thss->getNextDecisionRequest();
+  }else{
+    return Node::null();
   }
 }
 
@@ -173,8 +192,55 @@ Node TheoryUF::explain(TNode literal) {
   return mkAnd(assumptions);
 }
 
-void TheoryUF::collectModelInfo( TheoryModel* m ){
+void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){
   m->assertEqualityEngine( &d_equalityEngine );
+  if( fullModel ){
+#if 1
+    std::map< TypeNode, int > type_count;
+    //must choose proper representatives
+    // for each equivalence class, specify the constructor as a representative
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+    while( !eqcs_i.isFinished() ){
+      Node eqc = (*eqcs_i);
+      TypeNode tn = eqc.getType();
+      if( tn.isSort() ){
+        if( type_count.find( tn )==type_count.end() ){
+          type_count[tn] = 0;
+        }
+        std::stringstream ss;
+        ss << Expr::setlanguage(options::outputLanguage());
+        ss << "$t_" << tn << (type_count[tn]+1);
+        type_count[tn]++;
+        Node rep = NodeManager::currentNM()->mkSkolem( ss.str(), tn );
+        Trace("mkVar") << "TheoryUF::collectModelInfo:  make variable " << rep << " : " << tn << std::endl;
+        //specify the constant as the representative
+        m->assertEquality( eqc, rep, true );
+        m->assertRepresentative( rep );
+      }
+      ++eqcs_i;
+    }
+#else
+    std::map< TypeNode, TypeEnumerator* > type_enums;
+    //must choose proper representatives
+    // for each equivalence class, specify the constructor as a representative
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+    while( !eqcs_i.isFinished() ){
+      Node eqc = (*eqcs_i);
+      TypeNode tn = eqc.getType();
+      if( tn.isSort() ){
+        if( type_enums.find( tn )==type_enums.end() ){
+          type_enums[tn] = new TypeEnumerator( tn );
+        }
+        Node rep = *(*type_enums[tn]);
+        ++(*type_enums[tn]);
+        //specify the constant as the representative
+        m->assertEquality( eqc, rep, true );
+        m->assertRepresentative( rep );
+      }
+      ++eqcs_i;
+    }
+ #endif
+  }
 }
 
 void TheoryUF::presolve() {
@@ -481,3 +547,4 @@ Node TheoryUF::ppRewrite(TNode node) {
     }
   }
 }
+