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.

6 files changed, 37 insertions, 11 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 );