Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.

10 files changed, 77 insertions, 39 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 50b04123c..5cb8cf278 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -703,6 +703,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
         }else if ( !isStar(cond[j]) &&  //handle the case where there are 0 or 1 ground eqc of this type
                    d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){
           Node c = getUsedRepresentative( cond[j] );
+          c = getRepresentative( c );
           children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
         }
       }
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 5be263254..c0a734c35 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -593,7 +593,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
           types.push_back(f[0][i].getType());
         }
         TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );
-        Node op = NodeManager::currentNM()->mkSkolem( "fmc", typ, "op created for full-model checking" );
+        Node op = NodeManager::currentNM()->mkSkolem( "qfmc", typ, "op created for full-model checking" );
         d_quant_cond[f] = op;
       }
       //make sure all types are set
@@ -847,6 +847,8 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
   }
   else if( n.getType().isArray() ){
     //make the definition
+    bool success = false;
+    /*
     Node r = fm->getRepresentative(n);
     Trace("fmc-debug") << "Representative for array is " << r << std::endl;
     while( r.getKind() == kind::STORE ){
@@ -867,10 +869,11 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
         success = true;
       }
     }
+    */
     if( !success ){
-      Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
-      Trace("fmc-warn") << "          Default value was : " << odefaultValue << std::endl;
-      Trace("fmc-debug") << "Can't process base array " << r << std::endl;
+      //Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
+      //Trace("fmc-warn") << "          Default value was : " << odefaultValue << std::endl;
+      //Trace("fmc-debug") << "Can't process base array " << r << std::endl;
       //can't process this array
       d.reset();
       d.addEntry(fm, mkCondDefault(fm, f), Node::null());
@@ -1133,6 +1136,12 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
 void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,
                                              std::vector< Def > & dc, int index,
                                              std::vector< Node > & cond, std::vector<Node> & val ) {
+  Trace("fmc-if-process") << "int compose " << index << " / " << dc.size() << std::endl;
+  for( unsigned i=1; i<cond.size(); i++) {
+    debugPrint("fmc-if-process", cond[i], true);
+    Trace("fmc-if-process") << " ";
+  }
+  Trace("fmc-if-process") << std::endl;
   if ( index==(int)dc.size() ){
     Node c = mkCond(cond);
     Node v = evaluateInterpreted(n, val);
@@ -1264,6 +1273,7 @@ void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::v
   cond.push_back(d_quant_cond[f]);
   for (unsigned i=0; i<f[0].getNumChildren(); i++) {
     Node ts = fm->getStarElement( f[0][i].getType() );
+    Assert( ts.getType()==f[0][i].getType() );
     cond.push_back(ts);
   }
 }
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index cb379ec92..22dac2225 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -31,6 +31,7 @@ using namespace CVC4::kind;
 
 void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
   std::vector< int > fd_assertions;
+  std::map< int, Node > subs_head;
   //first pass : find defined functions, transform quantifiers
   for( unsigned i=0; i<assertions.size(); i++ ){
     Node n = TermDb::getFunDefHead( assertions[i] );
@@ -73,8 +74,9 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
         subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) );
       }
       bd = bd.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+      subs_head[i] = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
 
-      Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl;
+      Trace("fmf-fun-def") << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl;
       Trace("fmf-fun-def") << "  to " << std::endl;
       Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
       new_q = Rewriter::rewrite( new_q );
@@ -91,7 +93,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
     if( is_fd==0 || ( is_fd==1 && ( assertions[i][1].getKind()==EQUAL || assertions[i][1].getKind()==IFF ) ) ){
       std::vector< Node > constraints;
       Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl;
-      Node n = simplify( assertions[i], true, true, constraints, is_fd );
+      Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd==1 ? subs_head[i] : Node::null(), is_fd );
       Assert( constraints.empty() );
       if( n!=assertions[i] ){
         n = Rewriter::rewrite( n );
@@ -105,10 +107,11 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
   }
 }
 
-Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def ) {
+//is_fun_def 1 : top of fun-def, 2 : top of fun-def body, 0 : not top
+Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def ) {
   Trace("fmf-fun-def-debug") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl;
   if( n.getKind()==FORALL ){
-    Node c = simplify( n[1], pol, hasPol, constraints, is_fun_def );
+    Node c = simplifyFormula( n[1], pol, hasPol, constraints, hd, is_fun_def );
     if( c!=n[1] ){
       return NodeManager::currentNM()->mkNode( FORALL, n[0], c );
     }else{
@@ -123,13 +126,13 @@ Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& co
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
         Node c = n[i];
         //do not process LHS of definition
-        if( is_fun_def!=1 || i!=0 ){
+        if( is_fun_def!=1 || c!=hd ){
           bool newHasPol;
           bool newPol;
           QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
           //get child constraints
           std::vector< Node > cconstraints;
-          c = simplify( n[i], newPol, newHasPol, cconstraints, is_fun_def==1 ? 2 : 0 );
+          c = simplifyFormula( n[i], newPol, newHasPol, cconstraints, hd, is_fun_def==1 ? 2 : 0 );
           constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() );
         }
         children.push_back( c );
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h
index 63aa1bf94..54735d4d6 100644
--- a/src/theory/quantifiers/fun_def_process.h
+++ b/src/theory/quantifiers/fun_def_process.h
@@ -36,7 +36,7 @@ private:
   //defined functions to injections input -> argument elements
   std::map< Node, std::vector< Node > > d_input_arg_inj;
   //simplify
-  Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def = 0 );
+  Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def = 0 );
   //simplify term
   void simplifyTerm( Node n, std::vector< Node >& constraints );
 public:
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 078614509..cb969088d 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -127,6 +127,17 @@ Node InstMatch::get( int i ) {
   return d_vals[i];
 }
 
+void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ){
+  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+    Node val = get( i );
+    if( val.isNull() ){
+      Node ic =  qe->getTermDatabase()->getInstantiationConstant( f, i );
+      val = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+    }
+    inst.push_back( val );
+  }
+}
+
 void InstMatch::setValue( int i, TNode n ) {
   d_vals[i] = n;
 }
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 8753c0bb1..21220491f 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -78,6 +78,7 @@ public:
   void applyRewrite();
   /** get */
   Node get( int i );
+  void getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst );
   /** set */
   void setValue( int i, TNode n );
   bool set( QuantifiersEngine* qe, int i, TNode n );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8dec3898c..3fa3b2a1b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -748,24 +748,15 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
 }
 
 bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){
-  // For resource-limiting (also does a time check).
-  getOutputChannel().safePoint();
-
   std::vector< Node > terms;
-  //make sure there are values for each variable we are instantiating
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    Node val = m.get( i );
-    if( val.isNull() ){
-      Node ic = d_term_db->getInstantiationConstant( f, i );
-      val = d_term_db->getFreeVariableForInstConstant( ic );
-      Trace("inst-add-debug") << "mkComplete " << val << std::endl;
-    }
-    terms.push_back( val );
-  }
+  m.getTerms( this, f, terms );
   return addInstantiation( f, terms, mkRep, modEq, modInst );
 }
 
 bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) {
+  // For resource-limiting (also does a time check).
+  getOutputChannel().safePoint();
+
   Assert( terms.size()==f[0].getNumChildren() );
   Trace("inst-add-debug") << "Add instantiation: ";
   for( unsigned i=0; i<terms.size(); i++ ){
@@ -1020,7 +1011,7 @@ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
   }
   Trace(c) << std::endl;
   for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
-    Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;    
+    Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
   }
 }
 
@@ -1075,6 +1066,23 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
   if( !options::internalReps() ){
     return r;
   }else{
+    if( options::finiteModelFind() ){
+      if( r.isConst() ){
+        //map back from values assigned by model, if any
+        if( d_qe->getModel() ){
+          std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
+          if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
+            r = it->second;
+            r = getRepresentative( r );
+          }else{
+            if( r.getType().isSort() ){
+              Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
+            }
+          }
+        }
+      }
+    }
+
     if( d_int_rep.find( r )==d_int_rep.end() ){
       //find best selection for representative
       Node r_best;
@@ -1093,9 +1101,8 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
       Trace("internal-rep-select")  << " } " << std::endl;
       int r_best_score = -1;
       for( size_t i=0; i<eqc.size(); i++ ){
-        //if cbqi is active, do not choose instantiation constant terms
-        if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){
-          int score = getRepScore( eqc[i], f, index );
+        int score = getRepScore( eqc[i], f, index );
+        if( score!=-2 ){
           if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
             r_best = eqc[i];
             r_best_score = score;
@@ -1253,21 +1260,21 @@ int getDepth( Node n ){
 
 //smaller the score, the better
 int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
-  int s;
-  if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
+  if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){
+    return -2;
+  }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
     return -1;
   }else if( options::instMaxLevel()!=-1 ){
     //score prefer lowest instantiation level
     if( n.hasAttribute(InstLevelAttribute()) ){
-      s = n.getAttribute(InstLevelAttribute());
+      return n.getAttribute(InstLevelAttribute());
     }else{
-      s = options::instLevelInputOnly() ? -1 : 0;
+      return options::instLevelInputOnly() ? -1 : 0;
     }
   }else{
     //score prefers earliest use of this term as a representative
-    s = d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
+    return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
   }
-  return s;
   //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n );    //term depth
 }
 
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index db0524034..5580dc3d7 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -26,6 +26,7 @@ void RepSet::clear(){
   d_type_reps.clear();
   d_type_complete.clear();
   d_tmap.clear();
+  d_values_to_terms.clear();
 }
 
 bool RepSet::hasRep( TypeNode tn, Node n ) {
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 19bb6d3d3..4aab230e6 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -33,6 +33,8 @@ public:
   std::map< TypeNode, std::vector< Node > > d_type_reps;
   std::map< TypeNode, bool > d_type_complete;
   std::map< Node, int > d_tmap;
+  // map from values to terms they were assigned for
+  std::map< Node, Node > d_values_to_terms;
   /** clear the set */
   void clear();
   /** has type */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 072f579be..52b018234 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -198,7 +198,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     }
 
     if (!d_equalityEngine->hasTerm(n)) {
-      if(n.getType().isRegExp()) { 
+      if(n.getType().isRegExp()) {
         ret = Rewriter::rewrite(ret);
       } else {
         // Unknown term - return first enumerated value for this type
@@ -666,7 +666,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       }
     } while (changed);
 
-    if (!fullModel || !unassignedAssignable) {
+    if (!unassignedAssignable) {
       break;
     }
 
@@ -675,9 +675,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     // different are different.
 
     // Only make assignments on a type if:
-    // 1. fullModel is true
-    // 2. there are no terms that share the same base type with un-normalized representatives
-    // 3. there are no terms that share teh same base type that are unevaluated evaluable terms
+    // 1. there are no terms that share the same base type with un-normalized representatives
+    // 2. there are no terms that share teh same base type that are unevaluated evaluable terms
     // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode where assignOne is true, go ahead and make one assignment
     changed = false;
     for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
@@ -730,6 +729,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
           Assert(!n.isNull());
           constantReps[*i2] = n;
           Trace("model-builder") << "    Assign: Setting constant rep of " << (*i2) << " to " << n << endl;
+          if( !fullModel ){
+            tm->d_rep_set.d_values_to_terms[n] = (*i2);
+          }
           changed = true;
           noRepSet.erase(i2);
           if (assignOne) {