Make fun-def quantifiers carry the function app they define, make fun-def utilities more robust. Fix bug in conjecture generation for non-parameterized operators.

6 files changed, 118 insertions, 76 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index eac16372a..8b7c0bda2 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -913,12 +913,10 @@ smt25Command[CVC4::Command*& cmd]
       term[expr, expr2]
       { PARSER_STATE->popScope(); 
         std::string attr_name("fun-def");
-        Type t = EXPR_MANAGER->booleanType();
-        Expr avar = PARSER_STATE->mkVar(attr_name, t);
-        aexpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
-        aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr );
+        aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app);
+        aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr);
         //set the attribute to denote this is a function definition
-        static_cast<CommandSequence*>($cmd)->addCommand( new SetUserAttributeCommand( attr_name, avar ) );
+        static_cast<CommandSequence*>($cmd)->addCommand( new SetUserAttributeCommand( attr_name, func_app ) );
         //assert it
         Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs), MK_EXPR( func_app.getType().isBoolean() ? kind::IFF : kind::EQUAL, func_app, expr ), aexpr);
         static_cast<CommandSequence*>($cmd)->addCommand( new AssertCommand(as, false) );
@@ -952,14 +950,6 @@ smt25Command[CVC4::Command*& cmd]
     RPAREN_TOK
     LPAREN_TOK
     { 
-      std::string attr_name("fun-def");
-      Type t = EXPR_MANAGER->booleanType();
-      Expr avar = PARSER_STATE->mkVar(attr_name, t);
-      aexpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
-      aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr );
-      //set the attribute to denote these are function definitions
-      static_cast<CommandSequence*>($cmd)->addCommand( new SetUserAttributeCommand( attr_name, avar ) );
-    
       //set up the first scope 
       if( sortedVarNamesList.empty() ){
         PARSER_STATE->parseError(std::string("Must define at least one function in define-funs-rec"));
@@ -980,6 +970,12 @@ smt25Command[CVC4::Command*& cmd]
     term[expr,expr2]
     { 
       func_defs.push_back( expr );
+      
+      std::string attr_name("fun-def");
+      aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app);
+      aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr );
+      //set the attribute to denote these are function definitions
+      static_cast<CommandSequence*>($cmd)->addCommand( new SetUserAttributeCommand( attr_name, func_app ) );
       //assert it
       Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs), MK_EXPR( func_app.getType().isBoolean() ? kind::IFF : kind::EQUAL, func_app, expr ), aexpr);
       static_cast<CommandSequence*>($cmd)->addCommand( new AssertCommand(as, false) );
@@ -1752,7 +1748,10 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
         ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
         PARSER_STATE->warning(ss.str());
       }
+      Expr avar;
       bool success = true;
+      std::string attr_name = attr;
+      attr_name.erase( attr_name.begin() );
       if( attr==":fun-def" ){
         if( ( expr.getKind()!=kind::EQUAL && expr.getKind()!=kind::IFF ) || expr[0].getKind()!=kind::APPLY_UF ){
           success = false;
@@ -1776,14 +1775,15 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
           std::stringstream ss;
           ss << "warning: Function definition should be an equality whose LHS is an uninterpreted function applied to unique variables.";
           PARSER_STATE->warning(ss.str());
+        }else{
+          avar = expr[0];
         }
+      }else{
+        Type t = EXPR_MANAGER->booleanType();
+        avar = PARSER_STATE->mkVar(attr_name, t);
       }
       if( success ){
-        std::string attr_name = attr;
-        attr_name.erase( attr_name.begin() );
         //will set the attribute on auxiliary var (preserves attribute on formula through rewriting)
-        Type t = EXPR_MANAGER->booleanType();
-        Expr avar = PARSER_STATE->mkVar(attr_name, t);
         retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
         Command* c = new SetUserAttributeCommand( attr_name, avar );
         c->setMuted(true);
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 520ea5e70..48d3f3902 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -285,8 +285,12 @@ Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
   while( d_free_var[tn].size()<=i ){

     std::stringstream oss;

     oss << tn;

+    std::string typ_name = oss.str();

+    while( typ_name[0]=='(' ){

+      typ_name.erase( typ_name.begin() );

+    }

     std::stringstream os;

-    os << oss.str()[0] << i;

+    os << typ_name[0] << i;

     Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn );

     d_free_var_num[x] = d_free_var[tn].size();

     d_free_var[tn].push_back( x );

@@ -1713,7 +1717,9 @@ Node TermGenerator::getTerm( TermGenEnv * s ) {
     Node f = s->getTgFunc( d_typ, d_status_num );

     if( d_children.size()==s->d_func_args[f].size() ){

       std::vector< Node > children;

-      children.push_back( f );

+      if( s->d_tg_func_param[f] ){

+        children.push_back( f );

+      }

       for( unsigned i=0; i<d_children.size(); i++ ){

         Node nc = s->d_tg_alloc[d_children[i]].getTerm( s );

         if( nc.isNull() ){

@@ -1776,6 +1782,7 @@ void TermGenEnv::collectSignatureInformation() {
           d_func_kind[it->first] = nn.getKind();

           d_typ_tg_funcs[tnull].push_back( it->first );

           d_typ_tg_funcs[nn.getType()].push_back( it->first );

+          d_tg_func_param[it->first] = ( nn.getMetaKind() == kind::metakind::PARAMETERIZED );

           Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl;

           getTermDatabase()->computeUfEqcTerms( it->first );

         }

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 462fadfce..2d8e8e403 100755
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -138,6 +138,8 @@ public:
   std::map< TypeNode, unsigned > d_var_limit;

   //the functions we can currently generate

   std::map< TypeNode, std::vector< TNode > > d_typ_tg_funcs;

+  // whether functions must add operators

+  std::map< TNode, bool > d_tg_func_param;

   //the equivalence classes (if applicable) that match the currently generated term

   bool d_gen_relevant_terms;

   //relevant equivalence classes

diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 0bc365ec7..b80d9d744 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -32,66 +32,71 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
   std::vector< int > fd_assertions;
   //first pass : find defined functions, transform quantifiers
   for( unsigned i=0; i<assertions.size(); i++ ){
-    if( assertions[i].getKind()==FORALL ){
-      if( quantifiers::TermDb::isFunDef( assertions[i] ) ){
-        Assert( assertions[i][1].getKind()==EQUAL || assertions[i][1].getKind()==IFF );
-        Node n = assertions[i][1][0];
-        Assert( n.getKind()==APPLY_UF );
-        Node f = n.getOperator();
-
-        //check if already defined, if so, throw error
-        if( d_sorts.find( f )!=d_sorts.end() ){
-          Message() << "Cannot define function " << f << " more than once." << std::endl;
-          exit( 0 );
-        }
+    Node n = TermDb::getFunDefHead( assertions[i] );
+    if( !n.isNull() ){
+      Assert( n.getKind()==APPLY_UF );
+      Node f = n.getOperator();
 
-        //create a sort S that represents the inputs of the function
-        std::stringstream ss;
-        ss << "I_" << f;
-        TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() );
-        d_sorts[f] = iType;
+      //check if already defined, if so, throw error
+      if( d_sorts.find( f )!=d_sorts.end() ){
+        Message() << "Cannot define function " << f << " more than once." << std::endl;
+        exit( 0 );
+      }
+      
+      Node bd = TermDb::getFunDefBody( assertions[i] );
+      Assert( !bd.isNull() );
+      bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
 
-        //create functions f1...fn mapping from this sort to concrete elements
-        for( unsigned j=0; j<n.getNumChildren(); j++ ){
-          TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() );
-          std::stringstream ss;
-          ss << f << "_arg_" << j;
-          d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) );
-        }
+      //create a sort S that represents the inputs of the function
+      std::stringstream ss;
+      ss << "I_" << f;
+      TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() );
+      d_sorts[f] = iType;
 
-        //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
-        std::vector< Node > children;
-        Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType );
-        Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bv );
-        std::vector< Node > subs;
-        std::vector< Node > vars;
-        for( unsigned j=0; j<n.getNumChildren(); j++ ){
-          vars.push_back( n[j] );
-          subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) );
-        }
-        Node bd = assertions[i][1].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+      //create functions f1...fn mapping from this sort to concrete elements
+      for( unsigned j=0; j<n.getNumChildren(); j++ ){
+        TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() );
+        std::stringstream ss;
+        ss << f << "_arg_" << j;
+        d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) );
+      }
 
-        Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl;
-        Trace("fmf-fun-def") << "  to " << std::endl;
-        assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
-        Trace("fmf-fun-def") << "  " << assertions[i] << std::endl;
-        fd_assertions.push_back( i );
+      //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
+      std::vector< Node > children;
+      Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType );
+      Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bv );
+      std::vector< Node > subs;
+      std::vector< Node > vars;
+      for( unsigned j=0; j<n.getNumChildren(); j++ ){
+        vars.push_back( n[j] );
+        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() );
+
+      Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl;
+      Trace("fmf-fun-def") << "  to " << std::endl;
+      assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
+      assertions[i] = Rewriter::rewrite( assertions[i] );
+      Trace("fmf-fun-def") << "  " << assertions[i] << std::endl;
+      fd_assertions.push_back( i );
     }
   }
   //second pass : rewrite assertions
   for( unsigned i=0; i<assertions.size(); i++ ){
     int is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end() ? 1 : 0;
-    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 );
-    Assert( constraints.empty() );
-    if( n!=assertions[i] ){
-      n = Rewriter::rewrite( n );
-      Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl;
-      Trace("fmf-fun-def-rewrite") << "  to " << std::endl;
-      Trace("fmf-fun-def-rewrite") << "  " << n << std::endl;
-      assertions[i] = n;
+    //constant boolean function definitions do not add domain constraints
+    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 );
+      Assert( constraints.empty() );
+      if( n!=assertions[i] ){
+        n = Rewriter::rewrite( n );
+        Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl;
+        Trace("fmf-fun-def-rewrite") << "  to " << std::endl;
+        Trace("fmf-fun-def-rewrite") << "  " << n << std::endl;
+        assertions[i] = n;
+      }
     }
   }
 }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 2e2007c0a..090d127f1 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1187,20 +1187,44 @@ Node TermDb::getRewriteRule( Node q ) {
 }
 
 bool TermDb::isFunDef( Node q ) {
-  if( q.getKind()==FORALL && ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && q.getNumChildren()==3 ){
+  return !getFunDefHead( q ).isNull();
+}
+
+Node TermDb::getFunDefHead( Node q ) {
+  //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && 
+  if( q.getKind()==FORALL && q.getNumChildren()==3 ){
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
       if( q[2][i].getKind()==INST_ATTRIBUTE ){
         if( q[2][i][0].getAttribute(FunDefAttribute()) ){
-          return true;
+          return q[2][i][0];
         }
       }
     }
   }
-  return false;
+  return Node::null();
+}
+Node TermDb::getFunDefBody( Node q ) {
+  Node h = getFunDefHead( q );
+  if( !h.isNull() ){
+    if( q[1].getKind()==EQUAL || q[1].getKind()==IFF ){
+      if( q[1][0]==h ){
+        return q[1][1];
+      }else if( q[1][1]==h ){
+        return q[1][0];
+      }
+    }else{
+      Node atom = q[1].getKind()==NOT ? q[1][0] : q[1];
+      bool pol = q[1].getKind()!=NOT;
+      if( atom==h ){
+        return NodeManager::currentNM()->mkConst( pol );
+      }
+    }
+  }
+  return Node::null();
 }
-
 
 void TermDb::computeAttributes( Node q ) {
+  Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
   if( q.getNumChildren()==3 ){
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
       Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl;
@@ -1217,9 +1241,9 @@ void TermDb::computeAttributes( Node q ) {
         if( avar.getAttribute(FunDefAttribute()) ){
           Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
           d_qattr_fundef[q] = true;
-          Assert( q[1].getKind()==EQUAL || q[1].getKind()==IFF );
-          Assert( q[1][0].getKind()==APPLY_UF );
-          Node f = q[1][0].getOperator();
+          //Assert( q[1].getKind()==EQUAL || q[1].getKind()==IFF );
+          //Assert( q[2][i][0]==q[1][0] || q[2][i][0]==q[1][1] );
+          Node f = q[2][i][0].getOperator();
           if( d_fun_defs.find( f )!=d_fun_defs.end() ){
             Message() << "Cannot define function " << f << " more than once." << std::endl;
             exit( 0 );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e4e34ce7f..db84ba885 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -340,6 +340,10 @@ public: //general queries concerning quantified formulas wrt modules
   static Node getRewriteRule( Node q );
   /** is fun def */
   static bool isFunDef( Node q );
+  /** get fun def body */
+  static Node getFunDefHead( Node q );
+  /** get fun def body */
+  static Node getFunDefBody( Node q );
 //attributes
 private:
   std::map< Node, bool > d_qattr_conjecture;