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

2 files changed, 0 insertions, 194 deletions

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