merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version

9 files changed, 176 insertions, 755 deletions

diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index b8446761c..61330bbde 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -19,11 +19,9 @@ libuf_la_SOURCES = \
 	theory_uf_instantiator.cpp \
 	theory_uf_strong_solver.h \
 	theory_uf_strong_solver.cpp \
-	theory_uf_candidate_generator.h \
-	theory_uf_candidate_generator.cpp \
 	inst_strategy.h \
 	inst_strategy.cpp \
 	theory_uf_model.h \
-	theory_uf_model.cpp
+	theory_uf_model.cpp 
 
 EXTRA_DIST = kinds
diff --git a/src/theory/uf/theory_uf_candidate_generator.cpp b/src/theory/uf/theory_uf_candidate_generator.cpp
deleted file mode 100644
index 80151d1e1..000000000
--- a/src/theory/uf/theory_uf_candidate_generator.cpp
+++ /dev/null
@@ -1,182 +0,0 @@
-/*********************                                                        */
-/*! \file theory_uf_candidate_generator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory uf candidate generator class
- **/
-
-#include "theory/uf/theory_uf_candidate_generator.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/quantifiers/term_database.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
-
-namespace CVC4{
-namespace theory{
-namespace uf{
-namespace inst{
-
-CandidateGeneratorTheoryUf::CandidateGeneratorTheoryUf( InstantiatorTheoryUf* ith, Node op ) :
-  d_op( op ), d_ith( ith ), d_term_iter( -2 ){
-  Assert( !d_op.isNull() );
-}
-void CandidateGeneratorTheoryUf::resetInstantiationRound(){
-  d_term_iter_limit = d_ith->getQuantifiersEngine()->getTermDatabase()->d_op_map[d_op].size();
-}
-
-void CandidateGeneratorTheoryUf::reset( Node eqc ){
-  if( eqc.isNull() ){
-    d_term_iter = 0;
-  }else{
-    //create an equivalence class iterator in eq class eqc
-    if( ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->hasTerm( eqc ) ){
-      eqc = ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->getRepresentative( eqc );
-      d_eqc = eq::EqClassIterator( eqc, ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() );
-      d_retNode = Node::null();
-    }else{
-      d_retNode = eqc;
-
-    }
-    d_term_iter = -1;
-  }
-}
-
-Node CandidateGeneratorTheoryUf::getNextCandidate(){
-  if( d_term_iter>=0 ){
-    //get next candidate term in the uf term database
-    while( d_term_iter<d_term_iter_limit ){
-      Node n = d_ith->getQuantifiersEngine()->getTermDatabase()->d_op_map[d_op][d_term_iter];
-      d_term_iter++;
-      if( isLegalCandidate( n ) ){
-        return n;
-      }
-    }
-  }else if( d_term_iter==-1 ){
-    if( d_retNode.isNull() ){
-      //get next candidate term in equivalence class
-      while( !d_eqc.isFinished() ){
-        Node n = (*d_eqc);
-        ++d_eqc;
-        if( n.getKind()==APPLY_UF && n.getOperator()==d_op ){
-          if( isLegalCandidate( n ) ){
-            return n;
-          }
-        }
-      }
-    }else{
-      Node ret;
-      if( d_retNode.hasOperator() && d_retNode.getOperator()==d_op ){
-        ret = d_retNode;
-      }
-      d_term_iter = -2; //done returning matches
-      return ret;
-    }
-  }
-  return Node::null();
-}
-
-
-//CandidateGeneratorTheoryUfDisequal::CandidateGeneratorTheoryUfDisequal( InstantiatorTheoryUf* ith, Node eqc ) :
-//  d_ith( ith ), d_eq_class( eqc ){
-//  d_eci = NULL;
-//}
-//void CandidateGeneratorTheoryUfDisequal::resetInstantiationRound(){
-//
-//}
-////we will iterate over all terms that are disequal from eqc
-//void CandidateGeneratorTheoryUfDisequal::reset( Node eqc ){
-//  //Assert( !eqc.isNull() );
-//  ////begin iterating over equivalence classes that are disequal from eqc
-//  //d_eci = d_ith->getEquivalenceClassInfo( eqc );
-//  //if( d_eci ){
-//  //  d_eqci_iter = d_eci->d_disequal.begin();
-//  //}
-//}
-//Node CandidateGeneratorTheoryUfDisequal::getNextCandidate(){
-//  //if( d_eci ){
-//  //  while( d_eqci_iter != d_eci->d_disequal.end() ){
-//  //    if( (*d_eqci_iter).second ){
-//  //      //we have an equivalence class that is disequal from eqc
-//  //      d_cg->reset( (*d_eqci_iter).first );
-//  //      Node n = d_cg->getNextCandidate();
-//  //      //if there is a candidate in this equivalence class, return it
-//  //      if( !n.isNull() ){
-//  //        return n;
-//  //      }
-//  //    }
-//  //    ++d_eqci_iter;
-//  //  }
-//  //}
-//  return Node::null();
-//}
-
-
-CandidateGeneratorTheoryUfLitEq::CandidateGeneratorTheoryUfLitEq( InstantiatorTheoryUf* ith, Node mpat ) :
-  d_match_pattern( mpat ), d_ith( ith ){
-
-}
-void CandidateGeneratorTheoryUfLitEq::resetInstantiationRound(){
-
-}
-void CandidateGeneratorTheoryUfLitEq::reset( Node eqc ){
-  d_eq = eq::EqClassesIterator( ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() );
-}
-Node CandidateGeneratorTheoryUfLitEq::getNextCandidate(){
-  while( d_eq.isFinished() ){
-    Node n = (*d_eq);
-    ++d_eq;
-    if( n.getType()==d_match_pattern[0].getType() ){
-      //an equivalence class with the same type as the pattern, return reflexive equality
-      return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
-    }
-  }
-  return Node::null();
-}
-
-
-CandidateGeneratorTheoryUfLitDeq::CandidateGeneratorTheoryUfLitDeq( InstantiatorTheoryUf* ith, Node mpat ) :
-  d_match_pattern( mpat ), d_ith( ith ){
-
-}
-void CandidateGeneratorTheoryUfLitDeq::resetInstantiationRound(){
-
-}
-void CandidateGeneratorTheoryUfLitDeq::reset( Node eqc ){
-  Node false_term = ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->getRepresentative(
-                      NodeManager::currentNM()->mkConst<bool>(false) );
-  d_eqc_false = eq::EqClassIterator( false_term, ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() );
-}
-Node CandidateGeneratorTheoryUfLitDeq::getNextCandidate(){
-  //get next candidate term in equivalence class
-  while( !d_eqc_false.isFinished() ){
-    Node n = (*d_eqc_false);
-    ++d_eqc_false;
-    if( n.getKind()==d_match_pattern.getKind() ){
-      //found an iff or equality, try to match it
-      //DO_THIS: cache to avoid redundancies?
-      //DO_THIS: do we need to try the symmetric equality for n?  or will it also exist in the eq class of false?
-      return n;
-    }
-  }
-  return Node::null();
-}
-
-}
-}
-}
-}
diff --git a/src/theory/uf/theory_uf_candidate_generator.h b/src/theory/uf/theory_uf_candidate_generator.h
deleted file mode 100644
index a06f04f99..000000000
--- a/src/theory/uf/theory_uf_candidate_generator.h
+++ /dev/null
@@ -1,260 +0,0 @@
-/*********************                                                        */
-/*! \file theory_uf_candidate_generator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Theory uf candidate generator
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H
-#define __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/uf/theory_uf_instantiator.h"
-#include "theory/rr_inst_match.h"
-
-using namespace CVC4::theory::quantifiers;
-
-namespace CVC4 {
-namespace theory {
-namespace eq {
-
-namespace rrinst{
-typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
-
-//New CandidateGenerator. They have a simpler semantic than the old one
-
-// Just iterate amoung the equivalence classes
-// node::Null() must be given to reset
-class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{
-private:
-  //the equality classes iterator
-  eq::EqClassesIterator d_eq;
-  //equalityengine pointer
-  EqualityEngine* d_ee;
-public:
-  CandidateGeneratorTheoryEeClasses( EqualityEngine * ee): d_ee( ee ){}
-  ~CandidateGeneratorTheoryEeClasses(){}
-  void resetInstantiationRound(){};
-  void reset( TNode eqc ){
-    Assert(eqc.isNull());
-    d_eq = eq::EqClassesIterator( d_ee );
-  }; //* the argument is not used
-  TNode getNextCandidate(){
-    if( !d_eq.isFinished() ) return (*(d_eq++));
-    else return Node::null();
-  };
-};
-
-// Just iterate amoung the equivalence class of the given node
-// node::Null() *can't* be given to reset
-class CandidateGeneratorTheoryEeClass : public CandidateGenerator{
-private:
-  //instantiator pointer
-  EqualityEngine* d_ee;
-  //the equality class iterator
-  eq::EqClassIterator d_eqc;
-  /* For the case where the given term doesn't exists in uf */
-  Node d_retNode;
-public:
-  CandidateGeneratorTheoryEeClass( EqualityEngine* ee): d_ee( ee ){}
-  ~CandidateGeneratorTheoryEeClass(){}
-  void resetInstantiationRound(){};
-  void reset( TNode eqc ){
-    Assert(!eqc.isNull());
-    if( d_ee->hasTerm( eqc ) ){
-      /* eqc is in uf  */
-      eqc = d_ee->getRepresentative( eqc );
-      d_eqc = eq::EqClassIterator( eqc, d_ee );
-      d_retNode = Node::null();
-    }else{
-      /* If eqc if not a term known by uf, it is the only one in its
-         equivalence class. So we will return only it */
-      d_retNode = eqc;
-      d_eqc = eq::EqClassIterator();
-    }
-  }; //* the argument is not used
-  TNode getNextCandidate(){
-    if(d_retNode.isNull()){
-      if( !d_eqc.isFinished() ) return (*(d_eqc++));
-      else return Node::null();
-    }else{
-      /* the case where eqc not in uf */
-      Node ret = d_retNode;
-      d_retNode = Node::null(); /* d_eqc.isFinished() must be true */
-      return ret;
-    }
-  };
-};
-
-
-} /* namespace rrinst */
-} /* namespace eq */
-
-namespace uf {
-namespace rrinst {
-
-typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
-
-class CandidateGeneratorTheoryUfOp : public CandidateGenerator{
-private:
-  Node d_op;
-  //instantiator pointer
-  TermDb* d_tdb;
-  // Since new term can appears we restrict ourself to the one that
-  // exists at resetInstantiationRound
-  size_t d_term_iter_limit;
-  size_t d_term_iter;
-public:
-  CandidateGeneratorTheoryUfOp(Node op, TermDb* tdb): d_op(op), d_tdb( tdb ){}
-  ~CandidateGeneratorTheoryUfOp(){}
-  void resetInstantiationRound(){
-    d_term_iter_limit = d_tdb->d_op_map[d_op].size();
-  };
-  void reset( TNode eqc ){
-    Assert(eqc.isNull());
-    d_term_iter = 0;
-  }; //* the argument is not used
-  TNode getNextCandidate(){
-    if( d_term_iter<d_term_iter_limit ){
-      TNode n = d_tdb->d_op_map[d_op][d_term_iter];
-      ++d_term_iter;
-      return n;
-    } else return Node::null();
-  };
-};
-
-class CandidateGeneratorTheoryUfType : public CandidateGenerator{
-private:
-  TypeNode d_type;
-  //instantiator pointer
-  TermDb* d_tdb;
-  // Since new term can appears we restrict ourself to the one that
-  // exists at resetInstantiationRound
-  size_t d_term_iter_limit;
-  size_t d_term_iter;
-public:
-  CandidateGeneratorTheoryUfType(TypeNode type, TermDb* tdb): d_type(type), d_tdb( tdb ){}
-  ~CandidateGeneratorTheoryUfType(){}
-  void resetInstantiationRound(){
-    d_term_iter_limit = d_tdb->d_type_map[d_type].size();
-  };
-  void reset( TNode eqc ){
-    Assert(eqc.isNull());
-    d_term_iter = 0;
-  }; //* the argument is not used
-  TNode getNextCandidate(){
-    if( d_term_iter<d_term_iter_limit ){
-      TNode n = d_tdb->d_type_map[d_type][d_term_iter];
-      ++d_term_iter;
-      return n;
-    } else return Node::null();
-  };
-};
-
-} /* namespace rrinst */
-
-namespace inst{
-typedef CVC4::theory::inst::CandidateGenerator CandidateGenerator;
-
-//Old CandidateGenerator
-
-class CandidateGeneratorTheoryUfDisequal;
-
-class CandidateGeneratorTheoryUf : public CandidateGenerator
-{
-  friend class CandidateGeneratorTheoryUfDisequal;
-private:
-  //operator you are looking for
-  Node d_op;
-  //instantiator pointer
-  InstantiatorTheoryUf* d_ith;
-  //the equality class iterator
-  eq::EqClassIterator d_eqc;
-  int d_term_iter;
-  int d_term_iter_limit;
-private:
-  Node d_retNode;
-public:
-  CandidateGeneratorTheoryUf( InstantiatorTheoryUf* ith, Node op );
-  ~CandidateGeneratorTheoryUf(){}
-
-  void resetInstantiationRound();
-  void reset( Node eqc );
-  Node getNextCandidate();
-};
-
-//class CandidateGeneratorTheoryUfDisequal : public CandidateGenerator
-//{
-//private:
-//  //equivalence class 
-//  Node d_eq_class;
-//  //equivalence class info
-//  EqClassInfo* d_eci;
-//  //equivalence class iterator
-//  EqClassInfo::BoolMap::const_iterator d_eqci_iter;
-//  //instantiator pointer
-//  InstantiatorTheoryUf* d_ith;
-//public:
-//  CandidateGeneratorTheoryUfDisequal( InstantiatorTheoryUf* ith, Node eqc );
-//  ~CandidateGeneratorTheoryUfDisequal(){}
-//
-//  void resetInstantiationRound();
-//  void reset( Node eqc );   //should be what you want to be disequal from
-//  Node getNextCandidate();
-//};
-
-class CandidateGeneratorTheoryUfLitEq : public CandidateGenerator
-{
-private:
-  //the equality classes iterator
-  eq::EqClassesIterator d_eq;
-  //equality you are trying to match equalities for
-  Node d_match_pattern;
-  //einstantiator pointer
-  InstantiatorTheoryUf* d_ith;
-public:
-  CandidateGeneratorTheoryUfLitEq( InstantiatorTheoryUf* ith, Node mpat );
-  ~CandidateGeneratorTheoryUfLitEq(){}
-
-  void resetInstantiationRound();
-  void reset( Node eqc );
-  Node getNextCandidate();
-};
-
-class CandidateGeneratorTheoryUfLitDeq : public CandidateGenerator
-{
-private:
-  //the equality class iterator for false
-  eq::EqClassIterator d_eqc_false;
-  //equality you are trying to match disequalities for
-  Node d_match_pattern;
-  //einstantiator pointer
-  InstantiatorTheoryUf* d_ith;
-public:
-  CandidateGeneratorTheoryUfLitDeq( InstantiatorTheoryUf* ith, Node mpat );
-  ~CandidateGeneratorTheoryUfLitDeq(){}
-
-  void resetInstantiationRound();
-  void reset( Node eqc );
-  Node getNextCandidate();
-};
-
-
-}/* CVC4::theory::uf::inst namespace */
-}/* CVC4::theory::uf namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
index 257bed0a2..48092b340 100644
--- a/src/theory/uf/theory_uf_instantiator.cpp
+++ b/src/theory/uf/theory_uf_instantiator.cpp
@@ -17,7 +17,7 @@
 #include "theory/uf/theory_uf_instantiator.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/theory_uf.h"
-#include "theory/uf/theory_uf_candidate_generator.h"
+#include "theory/rr_candidate_generator.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/quantifiers/term_database.h"
 
@@ -160,15 +160,19 @@ bool InstantiatorTheoryUf::hasTerm( Node a ){
 }
 
 bool InstantiatorTheoryUf::areEqual( Node a, Node b ){
-  if( hasTerm( a ) && hasTerm( b ) ){
+  if( a==b ){
+    return true;
+  }else if( hasTerm( a ) && hasTerm( b ) ){
     return ((TheoryUF*)d_th)->d_equalityEngine.areEqual( a, b );
   }else{
-    return a==b;
+    return false;
   }
 }
 
 bool InstantiatorTheoryUf::areDisequal( Node a, Node b ){
-  if( hasTerm( a ) && hasTerm( b ) ){
+  if( a==b ){
+    return false;
+  }else if( hasTerm( a ) && hasTerm( b ) ){
     return ((TheoryUF*)d_th)->d_equalityEngine.areDisequal( a, b, false );
   }else{
     return false;
@@ -195,7 +199,7 @@ Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
         return rep;
       }else{
         //otherwise, must search eq class
-        eq::EqClassIterator eqc_iter( rep, &((TheoryUF*)d_th)->d_equalityEngine );
+        eq::EqClassIterator eqc_iter( rep, getEqualityEngine() );
         rep = Node::null();
         while( !eqc_iter.isFinished() ){
           if( !(*eqc_iter).hasAttribute(InstConstantAttribute()) ){
@@ -211,6 +215,23 @@ Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
   return d_ground_reps[a];
 }
 
+eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){
+  return &((TheoryUF*)d_th)->d_equalityEngine;
+}
+
+void InstantiatorTheoryUf::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
+  if( hasTerm( a ) ){
+    a = getEqualityEngine()->getRepresentative( a );
+    eq::EqClassIterator eqc_iter( a, getEqualityEngine() );
+    while( !eqc_iter.isFinished() ){
+      if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){
+        eqc.push_back( *eqc_iter );
+      }
+      eqc_iter++;
+    }
+  }
+}
+
 InstantiatorTheoryUf::Statistics::Statistics():
   //d_instantiations("InstantiatorTheoryUf::Total_Instantiations", 0),
   d_instantiations_ce_solved("InstantiatorTheoryUf::Instantiations_CE-Solved", 0),
@@ -527,7 +548,7 @@ void InstantiatorTheoryUf::collectTermsIps( Ips& ips, SetNode& terms, int index
 
 bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, SetNode & terms, bool addRep, bool modEq ){ //modEq default true
   bool addedTerm = false;
-  
+
   if( modEq && ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n )){
     Assert( getRepresentative( n )==n );
     //collect modulo equality
@@ -731,7 +752,7 @@ void InstantiatorTheoryUf::registerEfficientHandler( EfficientHandler& handler,
     d_pat_cand_gens[pats[i]].first->addPcDispatcher(&handler,i);
     d_pat_cand_gens[pats[i]].second->addPpDispatcher(&handler,i,i);
     d_cand_gens[op].addNewTermDispatcher(&handler,i);
-    
+
     combineMultiPpIpsMap(pp_ips_map,multi_pp_ips_map,handler,i,pats);
 
     pp_ips_map.clear();
diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h
index 3a2a5cc0e..d15c0103b 100644
--- a/src/theory/uf/theory_uf_instantiator.h
+++ b/src/theory/uf/theory_uf_instantiator.h
@@ -431,6 +431,8 @@ public:
   bool areDisequal( Node a, Node b );
   Node getRepresentative( Node a );
   Node getInternalRepresentative( Node a );
+  eq::EqualityEngine* getEqualityEngine();
+  void getEquivalenceClass( Node a, std::vector< Node >& eqc );
   /** general creators of candidate generators */
   rrinst::CandidateGenerator* getRRCanGenClasses();
   rrinst::CandidateGenerator* getRRCanGenClass();
@@ -520,6 +522,8 @@ public:
   bool areEqual( Node a, Node b ) { return d_ith->areEqual( a, b ); }
   bool areDisequal( Node a, Node b ) { return d_ith->areDisequal( a, b ); }
   Node getInternalRepresentative( Node a ) { return d_ith->getInternalRepresentative( a ); }
+  eq::EqualityEngine* getEngine() { return d_ith->getEqualityEngine(); }
+  void getEquivalenceClass( Node a, std::vector< Node >& eqc ) { d_ith->getEquivalenceClass( a, eqc ); }
 }; /* EqualityQueryInstantiatorTheoryUf */
 
 }
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index a85dea997..f68ab1429 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -34,12 +34,12 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::uf;

 

 //clear

-void UfModelTree::clear(){

+void UfModelTreeNode::clear(){

   d_data.clear();

   d_value = Node::null();

 }

 

-bool UfModelTree::hasConcreteArgumentDefinition(){

+bool UfModelTreeNode::hasConcreteArgumentDefinition(){

   if( d_data.size()>1 ){

     return true;

   }else if( d_data.empty() ){

@@ -51,16 +51,16 @@ bool UfModelTree::hasConcreteArgumentDefinition(){
 }

 

 //set value function

-void UfModelTree::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){

+void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){

   if( d_data.empty() ){

     d_value = v;

   }else if( !d_value.isNull() && d_value!=v ){

     d_value = Node::null();

   }

-  if( argIndex<(int)n.getNumChildren() ){

+  if( argIndex<(int)indexOrder.size() ){

     //take r = null when argument is the model basis

     Node r;

-    if( ground || !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ){

+    if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){

       r = m->getRepresentative( n[ indexOrder[argIndex] ] );

     }

     d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 );

@@ -68,7 +68,7 @@ void UfModelTree::setValue( TheoryModel* m, Node n, Node v, std::vector< int >&
 }

 

 //get value function

-Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){

+Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){

   if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){

     //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl;

     depIndex = argIndex;

@@ -82,7 +82,7 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd
       if( i==0 ){

         r = m->getRepresentative( n[ indexOrder[argIndex] ] );

       }

-      std::map< Node, UfModelTree >::iterator it = d_data.find( r );

+      std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );

       if( it!=d_data.end() ){

         val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 );

         if( !val.isNull() ){

@@ -101,7 +101,7 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd
   }

 }

 

-Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){

+Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){

   if( argIndex==(int)indexOrder.size() ){

     return d_value;

   }else{

@@ -113,7 +113,7 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd
       if( i==0 ){

         r = m->getRepresentative( n[ indexOrder[argIndex] ] );

       }

-      std::map< Node, UfModelTree >::iterator it = d_data.find( r );

+      std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );

       if( it!=d_data.end() ){

         val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 );

         //we have found a value

@@ -136,11 +136,11 @@ Node UfModelTree::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrd
   }

 }

 

-Node UfModelTree::getFunctionValue(){

+Node UfModelTreeNode::getFunctionValue(){

   if( !d_data.empty() ){

     Node defaultValue;

     std::vector< Node > caseValues;

-    for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){

+    for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){

       if( it->first.isNull() ){

         defaultValue = it->second.getFunctionValue();

       }else{

@@ -166,12 +166,12 @@ Node UfModelTree::getFunctionValue(){
 }

 

 //simplify function

-void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){

+void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){

   if( argIndex<(int)op.getType().getNumChildren()-1 ){

     std::vector< Node > eraseData;

     //first process the default argument

     Node r;

-    std::map< Node, UfModelTree >::iterator it = d_data.find( r );

+    std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );

     if( it!=d_data.end() ){

       if( !defaultVal.isNull() && it->second.d_value==defaultVal ){

         eraseData.push_back( r );

@@ -188,7 +188,7 @@ void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){
       }

     }

     //now see if any children can be removed, and simplify the ones that cannot

-    for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){

+    for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){

       if( !it->first.isNull() ){

         if( !defaultVal.isNull() && it->second.d_value==defaultVal ){

           eraseData.push_back( it->first );

@@ -207,12 +207,12 @@ void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){
 }

 

 //is total function

-bool UfModelTree::isTotal( Node op, int argIndex ){

+bool UfModelTreeNode::isTotal( Node op, int argIndex ){

   if( argIndex==(int)(op.getType().getNumChildren()-1) ){

     return !d_value.isNull();

   }else{

     Node r;

-    std::map< Node, UfModelTree >::iterator it = d_data.find( r );

+    std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );

     if( it!=d_data.end() ){

       return it->second.isTotal( op, argIndex+1 );

     }else{

@@ -221,7 +221,7 @@ bool UfModelTree::isTotal( Node op, int argIndex ){
   }

 }

 

-Node UfModelTree::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){

+Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){

   return d_value;

 }

 

@@ -231,9 +231,9 @@ void indent( std::ostream& out, int ind ){
   }

 }

 

-void UfModelTree::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){

+void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){

   if( !d_data.empty() ){

-    for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){

+    for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){

       if( !it->first.isNull() ){

         indent( out, ind );

         out << "if x_" << indexOrder[arg] << " == " << it->first << std::endl;

@@ -247,54 +247,36 @@ void UfModelTree::debugPrint( std::ostream& out, TheoryModel* m, std::vector< in
     indent( out, ind );

     out << "return ";

     m->printRepresentative( out, d_value );

-    //out << " { ";

-    //for( int i=0; i<(int)d_explicit.size(); i++ ){

-    //  out << d_explicit[i] << " ";

-    //}

-    //out << "}";

     out << std::endl;

   }

 }

 

-UfModel::UfModel( Node op, quantifiers::FirstOrderModel* m ) : d_model( m ), d_op( op ),

-d_model_constructed( false ){

-  d_tree = UfModelTreeOrdered( op );

-  TypeNode tn = d_op.getType();

-  tn = tn[(int)tn.getNumChildren()-1];

-  Assert( tn==NodeManager::currentNM()->booleanType() || tn.isDatatype() || uf::StrongSolverTheoryUf::isRelevantType( tn ) );

-  //look at ground assertions

-  for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ d_op ].size(); i++ ){

-    Node n = d_model->getTermDatabase()->d_op_map[ d_op ][i];

-    d_model->getTermDatabase()->computeModelBasisArgAttribute( n );

-    if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){

-      Node r = d_model->getRepresentative( n );

-      d_ground_asserts_reps.push_back( r );

-      d_ground_asserts.push_back( n );

-    }

-  }

-  //determine if it is constant

-  if( !d_ground_asserts.empty() ){

-    bool isConstant = true;

-    for( int i=1; i<(int)d_ground_asserts.size(); i++ ){

-      if( d_ground_asserts_reps[0]!=d_ground_asserts_reps[i] ){

-        isConstant = false;

-        break;

+

+Node UfModelTree::toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ){

+  if( fm_node.getKind()==FUNCTION_MODEL ){

+    if( fm_node[0].getKind()==FUNCTION_CASE_SPLIT ){

+      Node retNode;

+      Node childDefaultNode = defaultNode;

+      //get new default

+      if( fm_node.getNumChildren()==2 ){

+        childDefaultNode = toIte2( fm_node[1], args, index+1, defaultNode );

       }

+      retNode = childDefaultNode;

+      for( int i=(int)fm_node[0].getNumChildren()-1; i>=0; i-- ){

+        Node childNode = toIte2( fm_node[0][1], args, index+1, childDefaultNode );

+        retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( fm_node[0][0] ), childNode, retNode );

+      }

+      return retNode;

+    }else{

+      return toIte2( fm_node[0], args, index+1, defaultNode );

     }

-    if( isConstant ){

-      //set constant value

-      Node t = d_model->getTermDatabase()->getModelBasisOpTerm( d_op );

-      Node r = d_ground_asserts_reps[0];

-      setValue( t, r, false );

-      setModel();

-      Debug("fmf-model-cons") << "Function " << d_op << " is the constant function ";

-      d_model->printRepresentativeDebug( "fmf-model-cons", r );

-      Debug("fmf-model-cons") << std::endl;

-    }

+  }else{

+    return fm_node;

   }

 }

 

-Node UfModel::getIntersection( Node n1, Node n2, bool& isGround ){

+

+Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){

   //Notice() << "Get intersection " << n1 << " " << n2 << std::endl;

   isGround = true;

   std::vector< Node > children;

@@ -309,7 +291,7 @@ Node UfModel::getIntersection( Node n1, Node n2, bool& isGround ){
       children.push_back( n2[i] );

     }else if( n2[i].getAttribute(ModelBasisAttribute()) ){

       children.push_back( n1[i] );

-    }else if( d_model->areEqual( n1[i], n2[i] ) ){

+    }else if( m->areEqual( n1[i], n2[i] ) ){

       children.push_back( n1[i] );

     }else{

       return Node::null();

@@ -318,7 +300,7 @@ Node UfModel::getIntersection( Node n1, Node n2, bool& isGround ){
   return NodeManager::currentNM()->mkNode( APPLY_UF, children );

 }

 

-void UfModel::setValue( Node n, Node v, bool ground, bool isReq ){

+void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground, bool isReq ){

   Assert( !n.isNull() );

   Assert( !v.isNull() );

   d_set_values[ isReq ? 1 : 0 ][ ground ? 1 : 0 ][n] = v;

@@ -332,13 +314,13 @@ void UfModel::setValue( Node n, Node v, bool ground, bool isReq ){
         //  is also defined.

         //for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,

         //  then we must define f( b, a ).

-        Node ni = getIntersection( n, d_defaults[i], isGround );

+        Node ni = getIntersection( m, n, d_defaults[i], isGround );

         if( !ni.isNull() ){

           //if the intersection exists, and is not already defined

           if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&

               d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){

             //use the current value

-            setValue( ni, v, isGround, false );

+            setValue( m, ni, v, isGround, false );

           }

         }

       }

@@ -350,36 +332,21 @@ void UfModel::setValue( Node n, Node v, bool ground, bool isReq ){
   }

 }

 

-Node UfModel::getValue( Node n, int& depIndex ){

-  return d_tree.getValue( d_model, n, depIndex );

-}

-

-Node UfModel::getValue( Node n, std::vector< int >& depIndex ){

-  return d_tree.getValue( d_model, n, depIndex );

-}

-

-Node UfModel::getConstantValue( Node n ){

-  if( d_model_constructed ){

-    return d_tree.getConstantValue( d_model, n );

-  }else{

-    return Node::null();

+void UfModelTreeGenerator::makeModel( TheoryModel* m, UfModelTree& tree ){

+  for( int j=0; j<2; j++ ){

+    for( int k=0; k<2; k++ ){

+      for( std::map< Node, Node >::iterator it = d_set_values[j][k].begin(); it != d_set_values[j][k].end(); ++it ){

+        tree.setValue( m, it->first, it->second, k==1 );

+      }

+    }

   }

-}

-

-Node UfModel::getFunctionValue(){

-  if( d_func_value.isNull() && d_model_constructed ){

-    d_func_value = d_tree.getFunctionValue();

+  if( !d_default_value.isNull() ){

+    tree.setDefaultValue( m, d_default_value );

   }

-  return d_func_value;

-}

-

-bool UfModel::isConstant(){

-  Node gn = d_model->getTermDatabase()->getModelBasisOpTerm( d_op );

-  Node n = getConstantValue( gn );

-  return !n.isNull();

+  tree.simplify();

 }

 

-bool UfModel::optUsePartialDefaults(){

+bool UfModelTreeGenerator::optUsePartialDefaults(){

 #ifdef USE_PARTIAL_DEFAULT_VALUES

   return true;

 #else

@@ -387,114 +354,14 @@ bool UfModel::optUsePartialDefaults(){
 #endif

 }

 

-void UfModel::setModel(){

-  makeModel( d_tree );

-  d_model_constructed = true;

-  d_func_value = Node::null();

-

-  //for debugging, make sure model satisfies all ground assertions

-  for( size_t i=0; i<d_ground_asserts.size(); i++ ){

-    int depIndex;

-    Node n = d_tree.getValue( d_model, d_ground_asserts[i], depIndex );

-    if( n!=d_ground_asserts_reps[i] ){

-      Debug("fmf-bad") << "Bad model : " << d_ground_asserts[i] << " := ";

-      d_model->printRepresentativeDebug("fmf-bad", n );

-      Debug("fmf-bad") << " != ";

-      d_model->printRepresentativeDebug("fmf-bad", d_ground_asserts_reps[i] );

-      Debug("fmf-bad") << std::endl;

-    }

-  }

-}

-

-void UfModel::clearModel(){

+void UfModelTreeGenerator::clear(){

+  d_default_value = Node::null();

   for( int j=0; j<2; j++ ){

     for( int k=0; k<2; k++ ){

       d_set_values[j][k].clear();

     }

   }

-  d_tree.clear();

-  d_model_constructed = false;

-}

-

-void UfModel::makeModel( UfModelTreeOrdered& tree ){

-  for( int j=0; j<2; j++ ){

-    for( int k=0; k<2; k++ ){

-      for( std::map< Node, Node >::iterator it = d_set_values[j][k].begin(); it != d_set_values[j][k].end(); ++it ){

-        tree.setValue( d_model, it->first, it->second, k==1 );

-      }

-    }

-  }

-  tree.simplify();

-}

-

-void UfModel::toStream(std::ostream& out){

-  //out << "Function " << d_op << std::endl;

-  //out << "   Type: " << d_op.getType() << std::endl;

-  //out << "   Ground asserts:" << std::endl;

-  //for( int i=0; i<(int)d_ground_asserts.size(); i++ ){

-  //  out << "      " << d_ground_asserts[i] << " = ";

-  //  d_model->printRepresentative( out, d_ground_asserts[i] );

-  //  out << std::endl;

-  //}

-  //out << "   Model:" << std::endl;

-

-  TypeNode t = d_op.getType();

-  out << d_op << "( ";

-  for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){

-    out << "x_" << i << " : " << t[i];

-    if( i<(int)(t.getNumChildren()-2) ){

-      out << ", ";

-    }

-  }

-  out << " ) : " << t[(int)t.getNumChildren()-1] << std::endl;

-  if( d_tree.isEmpty() ){

-    out << "   [undefined]" << std::endl;

-  }else{

-    d_tree.debugPrint( out, d_model, 3 );

-    out << std::endl;

-  }

-  //out << "   Phase reqs:" << std::endl;  //for( int i=0; i<2; i++ ){

-  //  for( std::map< Node, std::vector< Node > >::iterator it = d_reqs[i].begin(); it != d_reqs[i].end(); ++it ){

-  //    out << "      " << it->first << std::endl;

-  //    for( int j=0; j<(int)it->second.size(); j++ ){

-  //      out << "         " << it->second[j] << " -> " << (i==1) << std::endl;

-  //    }

-  //  }

-  //}

-  //out << std::endl;

-  //for( int i=0; i<2; i++ ){

-  //  for( std::map< Node, std::map< Node, std::vector< Node > > >::iterator it = d_eq_reqs[i].begin(); it != d_eq_reqs[i].end(); ++it ){

-  //    out << "      " << "For " << it->first << ":" << std::endl;

-  //    for( std::map< Node, std::vector< Node > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){

-  //      for( int j=0; j<(int)it2->second.size(); j++ ){

-  //        out << "         " << it2->first << ( i==1 ? "==" : "!=" ) << it2->second[j] << std::endl;

-  //      }

-  //    }

-  //  }

-  //}

-}

-

-Node UfModel::toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ){

-  if( fm_node.getKind()==FUNCTION_MODEL ){

-    if( fm_node[0].getKind()==FUNCTION_CASE_SPLIT ){

-      Node retNode;

-      Node childDefaultNode = defaultNode;

-      //get new default

-      if( fm_node.getNumChildren()==2 ){

-        childDefaultNode = toIte2( fm_node[1], args, index+1, defaultNode );

-      }

-      retNode = childDefaultNode;

-      for( int i=(int)fm_node[0].getNumChildren()-1; i>=0; i-- ){

-        Node childNode = toIte2( fm_node[0][1], args, index+1, childDefaultNode );

-        retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( fm_node[0][0] ), childNode, retNode );

-      }

-      return retNode;

-    }else{

-      return toIte2( fm_node[0], args, index+1, defaultNode );

-    }

-  }else{

-    return fm_node;

-  }

+  d_defaults.clear();

 }

 

 

diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 406c7ff3c..47b149867 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -23,19 +23,14 @@
 

 namespace CVC4 {

 namespace theory {

-

-namespace quantifiers{

-  class FirstOrderModel;

-}

-

 namespace uf {

 

-class UfModelTree

+class UfModelTreeNode

 {

 public:

-  UfModelTree(){}

+  UfModelTreeNode(){}

   /** the data */

-  std::map< Node, UfModelTree > d_data;

+  std::map< Node, UfModelTreeNode > d_data;

   /** the value of this tree node (if all paths lead to same value) */

   Node d_value;

   /** has concrete argument defintion */

@@ -45,150 +40,137 @@ public:
   bool isEmpty() { return d_data.empty() && d_value.isNull(); }

   //clear

   void clear();

-  /** setValue function

-    *

-    * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false

-    *

-    */

+  /** setValue function */

   void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex );

-  /**  getValue function

-    *

-    *  returns $val, the value of ground term n

-    *  Say n is f( t_0...t_n )

-    *    depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to $val

-    *    for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c,

-    *      then g( a, a, a ) would return b with depIndex = 1

-    *  If ground = true, we are asking whether the term n is constant (assumes that all non-model basis arguments are ground)

-    *

-    */

+  /**  getValue function */

   Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex );

   Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex );

-  ///** getConstant Value function

-  //  *

-  //  * given term n, where n may contain model basis arguments

-  //  * if n is constant for its entire domain, then this function returns the value of its domain

-  //  * otherwise, it returns null

-  //  * for example, if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b,

-  //  *   then f( a, e ) would return b, while f( e, a ) would return null

-  //  *

-  //  */

+  /** getConstant Value function */

   Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex );

   /** getFunctionValue */

   Node getFunctionValue();

   /** simplify function */

   void simplify( Node op, Node defaultVal, int argIndex );

-  // is total ?

+  /** is total ? */

   bool isTotal( Node op, int argIndex );

 public:

   void debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind = 0, int arg = 0 );

 };

 

-class UfModelTreeOrdered

+class UfModelTree

 {

 private:

+  //the op this model is for

   Node d_op;

+  //the order we will treat the arguments

   std::vector< int > d_index_order;

-  UfModelTree d_tree;

+  //the data

+  UfModelTreeNode d_tree;

 public:

-  UfModelTreeOrdered(){}

-  UfModelTreeOrdered( Node op ) : d_op( op ){

+  //constructors

+  UfModelTree(){}

+  UfModelTree( Node op ) : d_op( op ){

     TypeNode tn = d_op.getType();

     for( int i=0; i<(int)(tn.getNumChildren()-1); i++ ){

       d_index_order.push_back( i );

     }

   }

-  UfModelTreeOrdered( Node op, std::vector< int >& indexOrder ) : d_op( op ){

+  UfModelTree( Node op, std::vector< int >& indexOrder ) : d_op( op ){

     d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() );

   }

-  bool isEmpty() { return d_tree.isEmpty(); }

+  /** clear/reset the function */

   void clear() { d_tree.clear(); }

+  /** setValue function

+    *

+    * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false

+    *

+    */

   void setValue( TheoryModel* m, Node n, Node v, bool ground = true ){

     d_tree.setValue( m, n, v, d_index_order, ground, 0 );

   }

+  /** setDefaultValue function */

+  void setDefaultValue( TheoryModel* m, Node v ){

+    d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 );

+  }

+  /**  getValue function

+    *

+    *  returns val, the value of ground term n

+    *  Say n is f( t_0...t_n )

+    *    depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to val

+    *    for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c,

+    *      then g( a, a, a ) would return b with depIndex = 1

+    *

+    */

   Node getValue( TheoryModel* m, Node n, int& depIndex ){

     return d_tree.getValue( m, n, d_index_order, depIndex, 0 );

   }

+  /** -> implementation incomplete */

   Node getValue( TheoryModel* m, Node n, std::vector< int >& depIndex ){

     return d_tree.getValue( m, n, d_index_order, depIndex, 0 );

   }

+  /** getConstantValue function

+    *

+    * given term n, where n may contain "all value" arguments, aka model basis arguments

+    *   if n is null, then every argument of n is considered "all value"

+    * if n is constant for the entire domain specified by n, then this function returns the value of its domain

+    * otherwise, it returns null

+    * for example, say the term e represents "all values"

+    *   if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b,

+    *     then f( a, e ) would return b, while f( e, a ) would return null

+    *  -> implementation incomplete

+    */

   Node getConstantValue( TheoryModel* m, Node n ) {

     return d_tree.getConstantValue( m, n, d_index_order, 0 );

   }

+  /** getFunctionValue

+    *   Returns a compact representation of this function, of kind FUNCTION_MODEL.

+    *   See documentation in theory/uf/kinds

+    */

   Node getFunctionValue(){

     return d_tree.getFunctionValue();

   }

+  /** simplify the tree */

   void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); }

+  /** is this tree total? */

   bool isTotal() { return d_tree.isTotal( d_op, 0 ); }

+  /** is this function constant? */

+  bool isConstant( TheoryModel* m ) { return !getConstantValue( m, Node::null() ).isNull(); }

+  /** is this tree empty? */

+  bool isEmpty() { return d_tree.isEmpty(); }

 public:

   void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){

     d_tree.debugPrint( out, m, d_index_order, ind );

   }

+private:

+  //helper for to ITE function.

+  static Node toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode );

+public:

+  /** to ITE function for function model nodes */

+  static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); }

 };

 

-class UfModel

+class UfModelTreeGenerator

 {

 private:

-  quantifiers::FirstOrderModel* d_model;

-  //the operator this model is for

-  Node d_op;

-  //is model constructed

-  bool d_model_constructed;

   //store for set values

+  Node d_default_value;

   std::map< Node, Node > d_set_values[2][2];

-private:

   // defaults

   std::vector< Node > d_defaults;

-  Node getIntersection( Node n1, Node n2, bool& isGround );

+  Node getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround );

 public:

-  UfModel(){}

-  UfModel( Node op, quantifiers::FirstOrderModel* m );

-  ~UfModel(){}

-  //ground terms for this operator

-  std::vector< Node > d_ground_asserts;

-  //the representatives they are equal to

-  std::vector< Node > d_ground_asserts_reps;

-  //data structure that stores the model

-  UfModelTreeOrdered d_tree;

-  //node equivalent of this model

-  Node d_func_value;

-public:

-  /** get operator */

-  Node getOperator() { return d_op; }

-  /** debug print */

-  void toStream( std::ostream& out );

+  UfModelTreeGenerator(){}

+  ~UfModelTreeGenerator(){}

+  /** set default value */

+  void setDefaultValue( Node v ) { d_default_value = v; }

   /** set value */

-  void setValue( Node n, Node v, bool ground = true, bool isReq = true );

-  /** get value, return arguments that the value depends on */

-  Node getValue( Node n, int& depIndex );

-  Node getValue( Node n, std::vector< int >& depIndex );

-  /** get constant value */

-  Node getConstantValue( Node n );

-  /** get function value for this function */

-  Node getFunctionValue();

-  /** is model constructed */

-  bool isModelConstructed() { return d_model_constructed; }

-  /** is empty */

-  bool isEmpty() { return d_ground_asserts.empty(); }

-  /** is constant */

-  bool isConstant();

+  void setValue( TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true );

+  /** make model */

+  void makeModel( TheoryModel* m, UfModelTree& tree );

   /** uses partial default values */

   bool optUsePartialDefaults();

-public:

-  /** set model */

-  void setModel();

-  /** clear model */

-  void clearModel();

-  /** make model */

-  void makeModel( UfModelTreeOrdered& tree );

-public:

-  /** set value preference */

-  void setValuePreference( Node f, Node n, bool isPro );

-private:

-  //helper for to ITE function.

-  static Node toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode );

-public:

-  /** to ITE function for function model nodes */

-  static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); }

+  /** reset */

+  void clear();

 };

 

 //this class stores temporary information useful to model engine for constructing model

@@ -197,6 +179,7 @@ class UfModelPreferenceData
 public:

   UfModelPreferenceData() : d_reconsiderModel( false ){}

   virtual ~UfModelPreferenceData(){}

+  Node d_const_val;

   // preferences for default values

   std::vector< Node > d_values;

   std::map< Node, std::vector< Node > > d_value_pro_con[2];

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index e5cb7e4f8..895a7d056 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1077,7 +1077,7 @@ void StrongSolverTheoryUf::newEqClass( Node n ){
     Debug("uf-ss-solver") << "StrongSolverTheoryUf: New eq class " << n << " " << tn << std::endl;
     c->newEqClass( n );
   }
-  //else if( isRelevantType( tn ) ){
+  //else if( tn.isSort() ){
   //  //Debug("uf-ss-solver") << "WAIT: StrongSolverTheoryUf: New eq class " << n << " " << tn << std::endl;
   //  //d_new_eq_class_waiting[tn].push_back( n );
   //}
@@ -1111,7 +1111,7 @@ void StrongSolverTheoryUf::assertNode( Node n, bool isDecision ){
   if( n.getKind()==CARDINALITY_CONSTRAINT ){
     TypeNode tn = n[0].getType();
     Assert( d_conf_find[tn]->getCardinality()>0 );
-    Assert( isRelevantType( tn ) );
+    Assert( tn.isSort() );
     Assert( d_conf_find[tn] );
     long nCard = n[1].getConst<Rational>().getNumerator().getLong();
     d_conf_find[tn]->assertCardinality( nCard, true );
@@ -1124,7 +1124,7 @@ void StrongSolverTheoryUf::assertNode( Node n, bool isDecision ){
     //must add new lemma
     Node nn = n[0];
     TypeNode tn = nn[0].getType();
-    Assert( isRelevantType( tn ) );
+    Assert( tn.isSort() );
     Assert( d_conf_find[tn] );
     long nCard = nn[1].getConst<Rational>().getNumerator().getLong();
     d_conf_find[tn]->assertCardinality( nCard, false );
@@ -1177,7 +1177,7 @@ void StrongSolverTheoryUf::propagate( Theory::Effort level ){
 void StrongSolverTheoryUf::preRegisterTerm( TNode n ){
   //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)  FIXME
   TypeNode tn = n.getType();
-  if( isRelevantType( tn ) ){
+  if( tn.isSort() ){
     preRegisterType( tn );
   }
 }
@@ -1187,9 +1187,10 @@ void StrongSolverTheoryUf::registerQuantifier( Node f ){
   //must ensure the quantifier does not quantify over arithmetic
   for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
     TypeNode tn = f[0][i].getType();
-    if( isRelevantType( tn ) ){
+    if( tn.isSort() ){
       preRegisterType( tn );
     }else{
+      /*
       if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
         Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier";
         Debug("uf-ss-na") << " (" << f << ")";
@@ -1201,6 +1202,7 @@ void StrongSolverTheoryUf::registerQuantifier( Node f ){
         Debug("uf-ss-na") << std::endl;
         Unimplemented("Cannot perform finite model finding on datatype quantifier");
       }
+      */
     }
   }
 }
@@ -1233,7 +1235,7 @@ StrongSolverTheoryUf::ConflictFind* StrongSolverTheoryUf::getConflictFind( TypeN
   std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.find( tn );
   //pre-register the type if not done already
   if( it==d_conf_find.end() ){
-    if( isRelevantType( tn ) ){
+    if( tn.isSort() ){
       preRegisterType( tn );
       it = d_conf_find.find( tn );
     }
@@ -1332,20 +1334,10 @@ StrongSolverTheoryUf::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_max_model_size);
 }
 
-bool StrongSolverTheoryUf::isRelevantType( TypeNode t ){
-  return t!=NodeManager::currentNM()->booleanType() &&
-         t!=NodeManager::currentNM()->integerType() &&
-         t!=NodeManager::currentNM()->realType() &&
-         t!=NodeManager::currentNM()->builtinOperatorType() &&
-         !t.isFunction() &&
-         !t.isDatatype() &&
-         !t.isArray();
-}
-
 bool StrongSolverTheoryUf::involvesRelevantType( Node n ){
   if( n.getKind()==APPLY_UF ){
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( isRelevantType( n[i].getType() ) ){
+      if( n[i].getType().isSort() ){
         return true;
       }
     }
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index bd4c4cb22..479fea05f 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -316,8 +316,6 @@ public:
   /** statistics class */
   Statistics d_statistics;
 
-  /** is relevant type */
-  static bool isRelevantType( TypeNode t );
   /** involves relevant type */
   static bool involvesRelevantType( Node n );
 };/* class StrongSolverTheoryUf */