Minor cleanup after today's commits:

* change some uses of "std::cout" to "Message()"

* change some files to use Unix newlines instead of DOS newlines

* fix compiler warning

2 files changed, 619 insertions, 619 deletions

diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index f68ab1429..0082f4840 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -1,421 +1,421 @@
-/*********************                                                        */

-/*! \file theory_uf_model.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 Model

- **/

-

-#include "theory/quantifiers/model_engine.h"

-#include "theory/theory_engine.h"

-#include "theory/uf/equality_engine.h"

-#include "theory/uf/theory_uf.h"

-#include "theory/uf/theory_uf_strong_solver.h"

-#include "theory/uf/theory_uf_instantiator.h"

-#include "theory/quantifiers/first_order_model.h"

-#include "theory/quantifiers/term_database.h"

-

-#define RECONSIDER_FUNC_DEFAULT_VALUE

-#define USE_PARTIAL_DEFAULT_VALUES

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-using namespace CVC4::theory::uf;

-

-//clear

-void UfModelTreeNode::clear(){

-  d_data.clear();

-  d_value = Node::null();

-}

-

-bool UfModelTreeNode::hasConcreteArgumentDefinition(){

-  if( d_data.size()>1 ){

-    return true;

-  }else if( d_data.empty() ){

-    return false;

-  }else{

-    Node r;

-    return d_data.find( r )==d_data.end();

-  }

-}

-

-//set value function

-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)indexOrder.size() ){

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

-    Node r;

-    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 );

-  }

-}

-

-//get value function

-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;

-    return d_value;

-  }else{

-    Node val;

-    int childDepIndex[2] = { argIndex, argIndex };

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

-      //first check the argument, then check default

-      Node r;

-      if( i==0 ){

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

-      }

-      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() ){

-          break;

-        }

-      }else{

-        //argument is not a defined argument: thus, it depends on this argument

-        childDepIndex[i] = argIndex+1;

-      }

-    }

-    //update depIndex

-    depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1];

-    //Notice() << "Return " << val << ", depIndex = " << depIndex;

-    //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl;

-    return val;

-  }

-}

-

-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{

-    Node val;

-    bool depArg = false;

-    //will try concrete value first, then default

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

-      Node r;

-      if( i==0 ){

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

-      }

-      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

-        if( !val.isNull() ){

-          if( i==0 ){

-            depArg = true;

-          }

-          break;

-        }

-      }

-    }

-    //it depends on this argument if we found it via concrete argument value,

-    // or if found by default/disequal from some concrete argument value(s).

-    if( depArg || hasConcreteArgumentDefinition() ){

-      if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){

-        depIndex.push_back( indexOrder[argIndex] );

-      }

-    }

-    return val;

-  }

-}

-

-Node UfModelTreeNode::getFunctionValue(){

-  if( !d_data.empty() ){

-    Node defaultValue;

-    std::vector< Node > caseValues;

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

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

-        defaultValue = it->second.getFunctionValue();

-      }else{

-        caseValues.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE, it->first, it->second.getFunctionValue() ) );

-      }

-    }

-    if( caseValues.empty() && defaultValue.getKind()!=FUNCTION_CASE_SPLIT && defaultValue.getKind()!=FUNCTION_MODEL ){

-      return defaultValue;

-    }else{

-      std::vector< Node > children;

-      if( !caseValues.empty() ){

-        children.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE_SPLIT, caseValues ) );

-      }

-      if( !defaultValue.isNull() ){

-        children.push_back( defaultValue );

-      }

-      return NodeManager::currentNM()->mkNode( FUNCTION_MODEL, children );

-    }

-  }else{

-    Assert( !d_value.isNull() );

-    return d_value;

-  }

-}

-

-//simplify function

-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, UfModelTreeNode >::iterator it = d_data.find( r );

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

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

-        eraseData.push_back( r );

-      }else{

-        it->second.simplify( op, defaultVal, argIndex+1 );

-        if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){

-          defaultVal = it->second.d_value;

-        }else{

-          defaultVal = Node::null();

-          if( it->second.isEmpty() ){

-            eraseData.push_back( r );

-          }

-        }

-      }

-    }

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

-    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 );

-        }else{

-          it->second.simplify( op, defaultVal, argIndex+1 );

-          if( it->second.isEmpty() ){

-            eraseData.push_back( it->first );

-          }

-        }

-      }

-    }

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

-      d_data.erase( eraseData[i] );

-    }

-  }

-}

-

-//is total function

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

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

-    return !d_value.isNull();

-  }else{

-    Node r;

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

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

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

-    }else{

-      return false;

-    }

-  }

-}

-

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

-  return d_value;

-}

-

-void indent( std::ostream& out, int ind ){

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

-    out << " ";

-  }

-}

-

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

-  if( !d_data.empty() ){

-    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;

-        it->second.debugPrint( out, m, indexOrder, ind+2, arg+1 );

-      }

-    }

-    if( d_data.find( Node::null() )!=d_data.end() ){

-      d_data[ Node::null() ].debugPrint( out, m, indexOrder, ind, arg+1 );

-    }

-  }else{

-    indent( out, ind );

-    out << "return ";

-    m->printRepresentative( out, d_value );

-    out << std::endl;

-  }

-}

-

-

-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 );

-    }

-  }else{

-    return fm_node;

-  }

-}

-

-

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

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

-  isGround = true;

-  std::vector< Node > children;

-  children.push_back( n1.getOperator() );

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

-    if( n1[i]==n2[i] ){

-      if( n1[i].getAttribute(ModelBasisAttribute()) ){

-        isGround = false;

-      }

-      children.push_back( n1[i] );

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

-      children.push_back( n2[i] );

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

-      children.push_back( n1[i] );

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

-      children.push_back( n1[i] );

-    }else{

-      return Node::null();

-    }

-  }

-  return NodeManager::currentNM()->mkNode( APPLY_UF, children );

-}

-

-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;

-  if( optUsePartialDefaults() ){

-    if( !ground ){

-      int defSize = (int)d_defaults.size();

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

-        bool isGround;

-        //for soundness, to allow variable order-independent function interpretations,

-        //  we must ensure that the intersection of all default terms

-        //  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( 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( m, ni, v, isGround, false );

-          }

-        }

-      }

-      d_defaults.push_back( n );

-    }

-    if( isReq && d_set_values[0][ ground ? 1 : 0 ].find( n )!=d_set_values[0][ ground ? 1 : 0 ].end()){

-      d_set_values[0][ ground ? 1 : 0 ].erase( n );

-    }

-  }

-}

-

-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 );

-      }

-    }

-  }

-  if( !d_default_value.isNull() ){

-    tree.setDefaultValue( m, d_default_value );

-  }

-  tree.simplify();

-}

-

-bool UfModelTreeGenerator::optUsePartialDefaults(){

-#ifdef USE_PARTIAL_DEFAULT_VALUES

-  return true;

-#else

-  return false;

-#endif

-}

-

-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_defaults.clear();

-}

-

-

-void UfModelPreferenceData::setValuePreference( Node f, Node n, Node r, bool isPro ){

-  if( std::find( d_values.begin(), d_values.end(), r )==d_values.end() ){

-    d_values.push_back( r );

-  }

-  int index = isPro ? 0 : 1;

-  if( std::find( d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), f )==d_value_pro_con[index][r].end() ){

-    d_value_pro_con[index][r].push_back( f );

-  }

-  d_term_pro_con[index][n].push_back( f );

-}

-

-Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* m ){

-  Node defaultVal;

-  double maxScore = -1;

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

-    Node v = d_values[i];

-    double score = ( 1.0 + (double)d_value_pro_con[0][v].size() )/( 1.0 + (double)d_value_pro_con[1][v].size() );

-    Debug("fmf-model-cons") << "  - score( ";

-    m->printRepresentativeDebug( "fmf-model-cons", v );

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

-    if( score>maxScore ){

-      defaultVal = v;

-      maxScore = score;

-    }

-  }

-#ifdef RECONSIDER_FUNC_DEFAULT_VALUE

-  if( maxScore<1.0 ){

-    //consider finding another value, if possible

-    Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl;

-    TypeNode tn = defaultTerm.getType();

-    Node newDefaultVal = m->getDomainValue( tn, d_values );

-    if( !newDefaultVal.isNull() ){

-      defaultVal = newDefaultVal;

-      Debug("fmf-model-cons-debug") << "-> Change default value to ";

-      m->printRepresentativeDebug( "fmf-model-cons-debug", defaultVal );

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

-    }else{

-      Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl;

-      Debug("fmf-model-cons-debug") << "      Excluding: ";

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

-        Debug("fmf-model-cons-debug") << d_values[i] << " ";

-      }

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

-    }

-  }

-#endif

-  //get the default term (this term must be defined non-ground in model)

-  Debug("fmf-model-cons") << "  Choose ";

-  m->printRepresentativeDebug("fmf-model-cons", defaultVal );

-  Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl;

-  Debug("fmf-model-cons") << "     # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl;

-  Debug("fmf-model-cons") << "     # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl;

-  return defaultVal;

+/*********************                                                        */
+/*! \file theory_uf_model.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 Model
+ **/
+
+#include "theory/quantifiers/model_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/theory_uf_strong_solver.h"
+#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
+
+#define RECONSIDER_FUNC_DEFAULT_VALUE
+#define USE_PARTIAL_DEFAULT_VALUES
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+
+//clear
+void UfModelTreeNode::clear(){
+  d_data.clear();
+  d_value = Node::null();
+}
+
+bool UfModelTreeNode::hasConcreteArgumentDefinition(){
+  if( d_data.size()>1 ){
+    return true;
+  }else if( d_data.empty() ){
+    return false;
+  }else{
+    Node r;
+    return d_data.find( r )==d_data.end();
+  }
+}
+
+//set value function
+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)indexOrder.size() ){
+    //take r = null when argument is the model basis
+    Node r;
+    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 );
+  }
+}
+
+//get value function
+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;
+    return d_value;
+  }else{
+    Node val;
+    int childDepIndex[2] = { argIndex, argIndex };
+    for( int i=0; i<2; i++ ){
+      //first check the argument, then check default
+      Node r;
+      if( i==0 ){
+        r = m->getRepresentative( n[ indexOrder[argIndex] ] );
+      }
+      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() ){
+          break;
+        }
+      }else{
+        //argument is not a defined argument: thus, it depends on this argument
+        childDepIndex[i] = argIndex+1;
+      }
+    }
+    //update depIndex
+    depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1];
+    //Notice() << "Return " << val << ", depIndex = " << depIndex;
+    //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl;
+    return val;
+  }
+}
+
+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{
+    Node val;
+    bool depArg = false;
+    //will try concrete value first, then default
+    for( int i=0; i<2; i++ ){
+      Node r;
+      if( i==0 ){
+        r = m->getRepresentative( n[ indexOrder[argIndex] ] );
+      }
+      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
+        if( !val.isNull() ){
+          if( i==0 ){
+            depArg = true;
+          }
+          break;
+        }
+      }
+    }
+    //it depends on this argument if we found it via concrete argument value,
+    // or if found by default/disequal from some concrete argument value(s).
+    if( depArg || hasConcreteArgumentDefinition() ){
+      if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){
+        depIndex.push_back( indexOrder[argIndex] );
+      }
+    }
+    return val;
+  }
+}
+
+Node UfModelTreeNode::getFunctionValue(){
+  if( !d_data.empty() ){
+    Node defaultValue;
+    std::vector< Node > caseValues;
+    for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
+      if( it->first.isNull() ){
+        defaultValue = it->second.getFunctionValue();
+      }else{
+        caseValues.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE, it->first, it->second.getFunctionValue() ) );
+      }
+    }
+    if( caseValues.empty() && defaultValue.getKind()!=FUNCTION_CASE_SPLIT && defaultValue.getKind()!=FUNCTION_MODEL ){
+      return defaultValue;
+    }else{
+      std::vector< Node > children;
+      if( !caseValues.empty() ){
+        children.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE_SPLIT, caseValues ) );
+      }
+      if( !defaultValue.isNull() ){
+        children.push_back( defaultValue );
+      }
+      return NodeManager::currentNM()->mkNode( FUNCTION_MODEL, children );
+    }
+  }else{
+    Assert( !d_value.isNull() );
+    return d_value;
+  }
+}
+
+//simplify function
+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, UfModelTreeNode >::iterator it = d_data.find( r );
+    if( it!=d_data.end() ){
+      if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
+        eraseData.push_back( r );
+      }else{
+        it->second.simplify( op, defaultVal, argIndex+1 );
+        if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){
+          defaultVal = it->second.d_value;
+        }else{
+          defaultVal = Node::null();
+          if( it->second.isEmpty() ){
+            eraseData.push_back( r );
+          }
+        }
+      }
+    }
+    //now see if any children can be removed, and simplify the ones that cannot
+    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 );
+        }else{
+          it->second.simplify( op, defaultVal, argIndex+1 );
+          if( it->second.isEmpty() ){
+            eraseData.push_back( it->first );
+          }
+        }
+      }
+    }
+    for( int i=0; i<(int)eraseData.size(); i++ ){
+      d_data.erase( eraseData[i] );
+    }
+  }
+}
+
+//is total function
+bool UfModelTreeNode::isTotal( Node op, int argIndex ){
+  if( argIndex==(int)(op.getType().getNumChildren()-1) ){
+    return !d_value.isNull();
+  }else{
+    Node r;
+    std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
+    if( it!=d_data.end() ){
+      return it->second.isTotal( op, argIndex+1 );
+    }else{
+      return false;
+    }
+  }
+}
+
+Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){
+  return d_value;
+}
+
+void indent( std::ostream& out, int ind ){
+  for( int i=0; i<ind; i++ ){
+    out << " ";
+  }
+}
+
+void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){
+  if( !d_data.empty() ){
+    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;
+        it->second.debugPrint( out, m, indexOrder, ind+2, arg+1 );
+      }
+    }
+    if( d_data.find( Node::null() )!=d_data.end() ){
+      d_data[ Node::null() ].debugPrint( out, m, indexOrder, ind, arg+1 );
+    }
+  }else{
+    indent( out, ind );
+    out << "return ";
+    m->printRepresentative( out, d_value );
+    out << std::endl;
+  }
+}
+
+
+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 );
+    }
+  }else{
+    return fm_node;
+  }
+}
+
+
+Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){
+  //Notice() << "Get intersection " << n1 << " " << n2 << std::endl;
+  isGround = true;
+  std::vector< Node > children;
+  children.push_back( n1.getOperator() );
+  for( int i=0; i<(int)n1.getNumChildren(); i++ ){
+    if( n1[i]==n2[i] ){
+      if( n1[i].getAttribute(ModelBasisAttribute()) ){
+        isGround = false;
+      }
+      children.push_back( n1[i] );
+    }else if( n1[i].getAttribute(ModelBasisAttribute()) ){
+      children.push_back( n2[i] );
+    }else if( n2[i].getAttribute(ModelBasisAttribute()) ){
+      children.push_back( n1[i] );
+    }else if( m->areEqual( n1[i], n2[i] ) ){
+      children.push_back( n1[i] );
+    }else{
+      return Node::null();
+    }
+  }
+  return NodeManager::currentNM()->mkNode( APPLY_UF, children );
+}
+
+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;
+  if( optUsePartialDefaults() ){
+    if( !ground ){
+      int defSize = (int)d_defaults.size();
+      for( int i=0; i<defSize; i++ ){
+        bool isGround;
+        //for soundness, to allow variable order-independent function interpretations,
+        //  we must ensure that the intersection of all default terms
+        //  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( 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( m, ni, v, isGround, false );
+          }
+        }
+      }
+      d_defaults.push_back( n );
+    }
+    if( isReq && d_set_values[0][ ground ? 1 : 0 ].find( n )!=d_set_values[0][ ground ? 1 : 0 ].end()){
+      d_set_values[0][ ground ? 1 : 0 ].erase( n );
+    }
+  }
+}
+
+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 );
+      }
+    }
+  }
+  if( !d_default_value.isNull() ){
+    tree.setDefaultValue( m, d_default_value );
+  }
+  tree.simplify();
+}
+
+bool UfModelTreeGenerator::optUsePartialDefaults(){
+#ifdef USE_PARTIAL_DEFAULT_VALUES
+  return true;
+#else
+  return false;
+#endif
+}
+
+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_defaults.clear();
+}
+
+
+void UfModelPreferenceData::setValuePreference( Node f, Node n, Node r, bool isPro ){
+  if( std::find( d_values.begin(), d_values.end(), r )==d_values.end() ){
+    d_values.push_back( r );
+  }
+  int index = isPro ? 0 : 1;
+  if( std::find( d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), f )==d_value_pro_con[index][r].end() ){
+    d_value_pro_con[index][r].push_back( f );
+  }
+  d_term_pro_con[index][n].push_back( f );
+}
+
+Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* m ){
+  Node defaultVal;
+  double maxScore = -1;
+  for( size_t i=0; i<d_values.size(); i++ ){
+    Node v = d_values[i];
+    double score = ( 1.0 + (double)d_value_pro_con[0][v].size() )/( 1.0 + (double)d_value_pro_con[1][v].size() );
+    Debug("fmf-model-cons") << "  - score( ";
+    m->printRepresentativeDebug( "fmf-model-cons", v );
+    Debug("fmf-model-cons") << " ) = " << score << std::endl;
+    if( score>maxScore ){
+      defaultVal = v;
+      maxScore = score;
+    }
+  }
+#ifdef RECONSIDER_FUNC_DEFAULT_VALUE
+  if( maxScore<1.0 ){
+    //consider finding another value, if possible
+    Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl;
+    TypeNode tn = defaultTerm.getType();
+    Node newDefaultVal = m->getDomainValue( tn, d_values );
+    if( !newDefaultVal.isNull() ){
+      defaultVal = newDefaultVal;
+      Debug("fmf-model-cons-debug") << "-> Change default value to ";
+      m->printRepresentativeDebug( "fmf-model-cons-debug", defaultVal );
+      Debug("fmf-model-cons-debug") << std::endl;
+    }else{
+      Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl;
+      Debug("fmf-model-cons-debug") << "      Excluding: ";
+      for( int i=0; i<(int)d_values.size(); i++ ){
+        Debug("fmf-model-cons-debug") << d_values[i] << " ";
+      }
+      Debug("fmf-model-cons-debug") << std::endl;
+    }
+  }
+#endif
+  //get the default term (this term must be defined non-ground in model)
+  Debug("fmf-model-cons") << "  Choose ";
+  m->printRepresentativeDebug("fmf-model-cons", defaultVal );
+  Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl;
+  Debug("fmf-model-cons") << "     # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl;
+  Debug("fmf-model-cons") << "     # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl;
+  return defaultVal;
 }
\ No newline at end of file
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 47b149867..9dba16608 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -1,199 +1,199 @@
-/*********************                                                        */

-/*! \file theory_uf_model.h

- ** \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 Model for Theory UF

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__THEORY_UF_MODEL_H

-#define __CVC4__THEORY_UF_MODEL_H

-

-#include "theory/model.h"

-

-namespace CVC4 {

-namespace theory {

-namespace uf {

-

-class UfModelTreeNode

-{

-public:

-  UfModelTreeNode(){}

-  /** the 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 */

-  bool hasConcreteArgumentDefinition();

-public:

-  //is this model tree empty?

-  bool isEmpty() { return d_data.empty() && d_value.isNull(); }

-  //clear

-  void clear();

-  /** setValue function */

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

-  /**  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 */

-  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 ? */

-  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 UfModelTree

-{

-private:

-  //the op this model is for

-  Node d_op;

-  //the order we will treat the arguments

-  std::vector< int > d_index_order;

-  //the data

-  UfModelTreeNode d_tree;

-public:

-  //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 );

-    }

-  }

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

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

-  }

-  /** 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 UfModelTreeGenerator

-{

-private:

-  //store for set values

-  Node d_default_value;

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

-  // defaults

-  std::vector< Node > d_defaults;

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

-public:

-  UfModelTreeGenerator(){}

-  ~UfModelTreeGenerator(){}

-  /** set default value */

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

-  /** set value */

-  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();

-  /** reset */

-  void clear();

-};

-

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

-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];

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

-  bool d_reconsiderModel;

-  /** set value preference */

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

-  /** get best default value */

-  Node getBestDefaultValue( Node defaultTerm, TheoryModel* m );

-};

-

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file theory_uf_model.h
+ ** \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 Model for Theory UF
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_UF_MODEL_H
+#define __CVC4__THEORY_UF_MODEL_H
+
+#include "theory/model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+class UfModelTreeNode
+{
+public:
+  UfModelTreeNode(){}
+  /** the 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 */
+  bool hasConcreteArgumentDefinition();
+public:
+  //is this model tree empty?
+  bool isEmpty() { return d_data.empty() && d_value.isNull(); }
+  //clear
+  void clear();
+  /** setValue function */
+  void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex );
+  /**  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 */
+  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 ? */
+  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 UfModelTree
+{
+private:
+  //the op this model is for
+  Node d_op;
+  //the order we will treat the arguments
+  std::vector< int > d_index_order;
+  //the data
+  UfModelTreeNode d_tree;
+public:
+  //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 );
+    }
+  }
+  UfModelTree( Node op, std::vector< int >& indexOrder ) : d_op( op ){
+    d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() );
+  }
+  /** 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 UfModelTreeGenerator
+{
+private:
+  //store for set values
+  Node d_default_value;
+  std::map< Node, Node > d_set_values[2][2];
+  // defaults
+  std::vector< Node > d_defaults;
+  Node getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround );
+public:
+  UfModelTreeGenerator(){}
+  ~UfModelTreeGenerator(){}
+  /** set default value */
+  void setDefaultValue( Node v ) { d_default_value = v; }
+  /** set value */
+  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();
+  /** reset */
+  void clear();
+};
+
+//this class stores temporary information useful to model engine for constructing model
+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];
+  std::map< Node, std::vector< Node > > d_term_pro_con[2];
+  bool d_reconsiderModel;
+  /** set value preference */
+  void setValuePreference( Node f, Node n, Node r, bool isPro );
+  /** get best default value */
+  Node getBestDefaultValue( Node defaultTerm, TheoryModel* m );
+};
+
+
+}
+}
+}
+
+#endif