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

2 files changed, 109 insertions, 57 deletions

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
   {