From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 8 Aug 2018 18:09:19 +0000 (-0500)
Subject: Move uf model code from uf to quantifiers (#2095)
X-Git-Tag: cvc5-1.0.0~4799
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2947a2f2af0e9a40c3be9ba2e84f634c36e0dd0f;p=cvc5.git

Move uf model code from uf to quantifiers (#2095)
---

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 9d83c589f..b3dc9965b 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -398,7 +398,7 @@ void FirstOrderModel::computeModelBasisArgAttribute(Node n)
     }
     uint64_t val = 0;
     // determine if it has model basis attribute
-    for (unsigned j = 0; j < n.getNumChildren(); j++)
+    for (unsigned j = 0, nchild = n.getNumChildren(); j < nchild; j++)
     {
       if (n[j].getAttribute(ModelBasisAttribute()))
       {
@@ -416,6 +416,119 @@ unsigned FirstOrderModel::getModelBasisArg(Node n)
   return n.getAttribute(ModelBasisArgAttribute());
 }
 
+Node FirstOrderModelIG::UfModelTreeGenerator::getIntersection(TheoryModel* m,
+                                                              Node n1,
+                                                              Node n2,
+                                                              bool& isGround)
+{
+  isGround = true;
+  std::vector<Node> children;
+  children.push_back(n1.getOperator());
+  for (unsigned i = 0, size = n1.getNumChildren(); i < size; 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 FirstOrderModelIG::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 (!ground)
+  {
+    for (unsigned i = 0, defSize = d_defaults.size(); i < defSize; i++)
+    {
+      // for correctness, 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 ).
+      bool 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(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 FirstOrderModelIG::UfModelTreeGenerator::makeModel(TheoryModel* m,
+                                                        uf::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();
+}
+
+void FirstOrderModelIG::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();
+}
+
 FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) :
 FirstOrderModel(qe, c,name) {
 
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index c33e2c6b7..059250f8d 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -193,15 +193,58 @@ class FirstOrderModel : public TheoryModel
   void computeModelBasisArgAttribute(Node n);
 };/* class FirstOrderModel */
 
-
 class FirstOrderModelIG : public FirstOrderModel
 {
-public: //for Theory UF:
-  //models for each UF operator
-  std::map< Node, uf::UfModelTree > d_uf_model_tree;
-  //model generators
-  std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
-private:
+ public:  // for Theory UF:
+  /** class for generating models for uninterpreted functions
+   *
+   * This implements the model construction from page 6 of Reynolds et al,
+   * "Quantifier Instantiation Techniques for Finite Model Finding in SMT",
+   * CADE 2013.
+   */
+  class UfModelTreeGenerator
+  {
+   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, uf::UfModelTree& tree);
+    /** reset */
+    void clear();
+
+   public:
+    /** the overall default value */
+    Node d_default_value;
+    /**
+     * Stores (required, ground) values in key, value pairs of the form
+     * ( P( a, b ), c ), which indicates P( a, b ) has value c in the model.
+     * The "non-ground" values indicate that the key has a "model-basis"
+     * variable, for example, ( P( _, b ), c ) indicates that P( x, b ) has the
+     * value b for any value of x.
+     */
+    std::map<Node, Node> d_set_values[2][2];
+    /** stores the set of non-ground keys in the above maps */
+    std::vector<Node> d_defaults;
+    /**
+     * Returns the term corresponding to the intersection of n1 and n2, if it
+     * exists, for example, for P( _, a ) and P( b, _ ), this method returns
+     * P( b, a ), where _ is the "model basis" variable. We take into account
+     * equality between arguments, so if a=b, then the intersection of P( a, a )
+     * and P( b, _ ) is P( a, a ).
+     */
+    Node getIntersection(TheoryModel* m, Node n1, Node n2, bool& isGround);
+  };
+  /** models for each UF operator */
+  std::map<Node, uf::UfModelTree> d_uf_model_tree;
+  /** model generators for each UF operator */
+  std::map<Node, UfModelTreeGenerator> d_uf_model_gen;
+
+ private:
   //map from terms to the models used to calculate their value
   std::map< Node, bool > d_eval_uf_use_default;
   std::map< Node, uf::UfModelTree > d_eval_uf_model;
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index cc542f0c3..fcc9cd060 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -166,9 +166,81 @@ bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex)
   }
 }
 
+void QModelBuilderIG::UfModelPreferenceData::setValuePreference(Node q,
+                                                                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(), q)
+      == d_value_pro_con[index][r].end())
+  {
+    d_value_pro_con[index][r].push_back(q);
+  }
+}
+
+Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue(
+    Node defaultTerm, TheoryModel* m)
+{
+  Node defaultVal;
+  double maxScore = -1;
+  for (size_t i = 0, size = d_values.size(); i < size; i++)
+  {
+    Node v = d_values[i];
+    double score = (1.0 + static_cast<double>(d_value_pro_con[0][v].size()))
+                   / (1.0 + static_cast<double>(d_value_pro_con[1][v].size()));
+    Debug("fmf-model-cons-debug") << "  - score( ";
+    m->printRepresentativeDebug("fmf-model-cons-debug", v);
+    Debug("fmf-model-cons-debug") << " ) = " << score << std::endl;
+    if (score > maxScore)
+    {
+      defaultVal = v;
+      maxScore = score;
+    }
+  }
+  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->getRepSet()->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[tn.getNumChildren() - 1] << std::endl;
+      Debug("fmf-model-cons-debug") << "      Excluding: " << d_values;
+      Debug("fmf-model-cons-debug") << std::endl;
+    }
+  }
+  // get the default term (this term must be defined non-ground in model)
+  Debug("fmf-model-cons-debug") << "  Choose ";
+  m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal);
+  Debug("fmf-model-cons-debug")
+      << " as default value (" << defaultTerm << ")" << std::endl;
+  Debug("fmf-model-cons-debug")
+      << "     # quantifiers pro = " << d_value_pro_con[0][defaultVal].size()
+      << std::endl;
+  Debug("fmf-model-cons-debug")
+      << "     # quantifiers con = " << d_value_pro_con[1][defaultVal].size()
+      << std::endl;
+  return defaultVal;
+}
+
 QModelBuilderIG::QModelBuilderIG(context::Context* c, QuantifiersEngine* qe)
     : QModelBuilder(c, qe),
-      d_basisNoMatch(c),
       d_didInstGen(false),
       d_numQuantSat(0),
       d_numQuantInstGen(0),
@@ -347,7 +419,6 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
   //determine if any functions are constant
   for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){
     Node op = it->first;
-    TermArgBasisTrie tabt;
     std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
     if( itut!=fmig->d_uf_terms.end() ){
       for( size_t i=0; i<itut->second.size(); i++ ){
@@ -360,14 +431,6 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
           d_uf_prefs[op].d_const_val = Node::null();
           break;
         }
-        //for calculating terms that we don't need to consider
-        //if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
-        if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){
-          //need to consider if it is not congruent modulo model basis
-          if( !tabt.addTerm( fmig, n ) ){
-            d_basisNoMatch[n] = true;
-          }
-        }
       }
     }
     if( !d_uf_prefs[op].d_const_val.isNull() ){
@@ -604,15 +667,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
             d_qe->getModel()->setQuantifierActive( f, false );
             //check if choosing this literal would add any additional constraints to default definitions
             selectLitConstraints = false;
-            for( int j=0; j<(int)uf_terms.size(); j++ ){
-              Node op = uf_terms[j].getOperator();
-              if( d_uf_prefs[op].d_reconsiderModel ){
-                selectLitConstraints = true;
-              }
-            }
-            if( !selectLitConstraints ){
-              selectLit = true;
-            }
+            selectLit = true;
           }
           //also check if it is naturally a better literal
           if( !selectLit ){
@@ -662,7 +717,6 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
       Debug("fmf-model-prefs") << "  * Constant SAT due to definition of ops: ";
       for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
         Debug("fmf-model-prefs") << selectionLitTerms[i] << " ";
-        d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false;
       }
       Debug("fmf-model-prefs") << std::endl;
     }else{
@@ -671,7 +725,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
         for( int j=0; j<(int)pro_con[k].size(); j++ ){
           Node op = pro_con[k][j].getOperator();
           Node r = fmig->getRepresentative( pro_con[k][j] );
-          d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
+          d_uf_prefs[op].setValuePreference(f, r, k == 0);
         }
       }
     }
@@ -731,21 +785,6 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
 
 void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
   FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
-  if( optReconsiderFuncConstants() ){
-    //reconsider constant functions that weren't necessary
-    if( d_uf_model_constructed[op] ){
-      if( d_uf_prefs[op].d_reconsiderModel ){
-        //if we are allowed to reconsider default value, then see if the default value can be improved
-        Node v = d_uf_prefs[op].d_const_val;
-        if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){
-          Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl;
-          fmig->d_uf_model_tree[op].clear();
-          fmig->d_uf_model_gen[op].clear();
-          d_uf_model_constructed[op] = false;
-        }
-      }
-    }
-  }
   if( !d_uf_model_constructed[op] ){
     //construct the model for the uninterpretted function/predicate
     bool setDefaultVal = true;
@@ -765,19 +804,13 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
         //set n = v in the model tree
         //set it as ground value
         fmig->d_uf_model_gen[op].setValue( fm, n, v );
-        if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){
-          //also set as default value if necessary
-          if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
-            Trace("fmf-model-cons") << "  Set as default." << std::endl;
-            fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
-            if( n==defaultTerm ){
-              //incidentally already set, we will not need to find a default value
-              setDefaultVal = false;
-            }
-          }
-        }else{
+        // also set as default value if necessary
+        if (n.hasAttribute(ModelBasisArgAttribute())
+            && n.getAttribute(ModelBasisArgAttribute()) != 0)
+        {
+          Trace("fmf-model-cons") << "  Set as default." << std::endl;
+          fmig->d_uf_model_gen[op].setValue(fm, n, v, false);
           if( n==defaultTerm ){
-            fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
             //incidentally already set, we will not need to find a default value
             setDefaultVal = false;
           }
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index b08537e9f..353883a20 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -56,10 +56,6 @@ public:
   unsigned getNumTriedLemmas() { return d_triedLemmas; }
 };
 
-
-
-
-
 class TermArgBasisTrie {
 public:
   /** the data */
@@ -80,9 +76,34 @@ class QModelBuilderIG : public QModelBuilder
   typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
 
  protected:
-  BoolMap d_basisNoMatch;
-  //map from operators to model preference data
-  std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
+  /**
+   * This class stores temporary information useful to model engine for
+   * constructing models for uninterpreted functions.
+   */
+  class UfModelPreferenceData
+  {
+   public:
+    UfModelPreferenceData() {}
+    virtual ~UfModelPreferenceData() {}
+    /** any constant value of the type */
+    Node d_const_val;
+    /** list of possible default values */
+    std::vector<Node> d_values;
+    /**
+     * Map from values to the set of quantified formulas that are (pro, con)
+     * that value. A quantified formula may be "pro" a particular default
+     * value of an uninterpreted function if that value is likely to satisfy
+     * many points in its domain. For example, forall x. P( f( x ) ) may be
+     * "pro" the default value true for P.
+     */
+    std::map<Node, std::vector<Node> > d_value_pro_con[2];
+    /** set that quantified formula q is pro/con the default value of r */
+    void setValuePreference(Node q, Node r, bool isPro);
+    /** get best default value */
+    Node getBestDefaultValue(Node defaultTerm, TheoryModel* m);
+  };
+  /** map from operators to model preference data */
+  std::map<Node, UfModelPreferenceData> d_uf_prefs;
   //built model uf
   std::map< Node, bool > d_uf_model_constructed;
   //whether inst gen was done
@@ -189,8 +210,6 @@ class QModelBuilderDefault : public QModelBuilderIG
  public:
   QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
 
-  //options
-  bool optReconsiderFuncConstants() { return true; }
   //has inst gen
   bool hasInstGen(Node f) override
   {
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 8c994217d..3d656cf24 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -24,10 +24,6 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 
-
-#define RECONSIDER_FUNC_DEFAULT_VALUE
-#define USE_PARTIAL_DEFAULT_VALUES
-
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -317,147 +313,3 @@ Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){
   }
   return getFunctionValue( vars, simplify );
 }
-
-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++ ){
-        //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 ).
-        bool 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( 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-debug") << "  - score( ";
-    m->printRepresentativeDebug( "fmf-model-cons-debug", v );
-    Debug("fmf-model-cons-debug") << " ) = " << 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->getRepSet()->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-debug") << "  Choose ";
-  m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal );
-  Debug("fmf-model-cons-debug") << " as default value (" << defaultTerm << ")" << std::endl;
-  Debug("fmf-model-cons-debug") << "     # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl;
-  Debug("fmf-model-cons-debug") << "     # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl;
-  return defaultVal;
-}
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 0fc0421b6..201faccee 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -23,8 +23,6 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
-// TODO (#1302) : some of these classes should be moved to
-// src/theory/quantifiers/
 class UfModelTreeNode
 {
 public:
@@ -148,50 +146,6 @@ public:
   }
 };
 
-
-class UfModelTreeGenerator
-{
-public:
-  //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 );
-};
-
-
 }
 }
 }