Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.

10 files changed, 172 insertions, 53 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 101e26746..7db87d579 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -663,11 +663,14 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
     }
     Expr sop = ops[sub_dt_index][0];
     Type curr_t;
-    if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || sop.getNumChildren()==0 ) ){
+    if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){
       curr_t = sop.getType();
-      Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << std::endl;
+      Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl;
       sygus_to_builtin_expr[t] = sop;
-      d_sygus_bound_var_type[sop] = t;
+      //store that term sop has dedicated sygus type t
+      if( d_sygus_bound_var_type.find( sop )==d_sygus_bound_var_type.end() ){
+        d_sygus_bound_var_type[sop] = t;
+      }
     }else{
       std::vector< Expr > children;
       if( sop.getKind() != kind::BUILTIN ){
@@ -677,13 +680,14 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
         std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
         if( it==sygus_to_builtin_expr.end() ){
           Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
-          Debug("parser-sygus") << ":  type elem " << i << " " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
+          Debug("parser-sygus") << ":  child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
           std::stringstream ss;
           ss << t << "_x_" << i;
           Expr bv = mkBoundVar(ss.str(), bt);
           children.push_back( bv );
           d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i];
         }else{
+          Debug("parser-sygus") << ":  child " << i << " existing sygus to builtin expr : " << it->second << std::endl;
           children.push_back( it->second );
         }
       }
@@ -775,9 +779,10 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
   cnames[index].pop_back();
   cnames[index].push_back(ss.str());
   
-  //TODO : mark function as let constructor
-  d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_vars.begin(), let_vars.end() );
+  //mark function as let constructor
+  d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_define_args.begin(), let_define_args.end() );
   d_sygus_let_func_to_body[let_func] = let_body;
+  d_sygus_let_func_to_num_input_vars[let_func] = let_vars.size();
 }
 
 
@@ -899,13 +904,24 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       testerId.append(name);
       checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
       checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
-      CVC4::DatatypeConstructor c(name, testerId, ops[i] );
+      CVC4::DatatypeConstructor c(name, testerId );
+      Debug("parser-sygus") << "--> Add constructor " << cnames[i] << " to " << dt.getName() << std::endl;
+      Expr let_body;
+      std::vector< Expr > let_args;
+      unsigned let_num_input_args = 0;
+      std::map< CVC4::Expr, CVC4::Expr >::iterator it = d_sygus_let_func_to_body.find( ops[i] );
+      if( it!=d_sygus_let_func_to_body.end() ){
+        let_body = it->second;
+        let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() );
+        let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]];
+        Debug("parser-sygus") << "    it is a let gterm with body " << let_body << std::endl;
+      }
+      c.setSygus( ops[i], let_body, let_args, let_num_input_args );
       for( unsigned j=0; j<cargs[i].size(); j++ ){
         std::stringstream sname;
         sname << name << "_" << j;
         c.addArg(sname.str(), cargs[i][j]);
       }
-      Debug("parser-sygus") << "--> Add constructor " << cnames[i] << " to " << dt.getName() << std::endl;
       dt.addConstructor(c);
     }
   }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 6781fec95..428977e0b 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -301,6 +301,7 @@ private:
   std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type;
   std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars;
   std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body;
+  std::map< CVC4::Expr, unsigned > d_sygus_let_func_to_num_input_vars;
   
   void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs );
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5d5bb93dc..1ab4ee62a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1429,6 +1429,11 @@ void SmtEngine::setDefaults() {
   if( options::recurseCbqi() || options::cbqi2() ){
     options::cbqi.set( true );
   }
+  if( options::cbqi2() ){
+    if( !options::rewriteDivk.wasSetByUser()) {
+      options::rewriteDivk.set( true );
+    }
+  }
   if( options::cbqi() ){
     if( !options::quantConflictFind.wasSetByUser() ){
       options::quantConflictFind.set( false );
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 19aacd0df..a9e6b3a78 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -928,10 +928,17 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node
               Node progc = prog;
               if( options::sygusNormalFormGlobalArg() ){
                 bool argChanged = false;
+                Trace("sygus-nf-gen-debug") << "Check replacements on " << prog << " " << prog.getKind() << std::endl;
                 for( unsigned i=0; i<prog.getNumChildren(); i++ ){
                   Node prev = children[i];
                   children[i] = d_tds->getVarInc( children_stype[i], var_count );
+                  if( parentOpKind!=kind::BUILTIN ){
+                    children.insert( children.begin(), prog.getOperator() );
+                  }
                   Node progcn = NodeManager::currentNM()->mkNode( prog.getKind(), children );
+                  if( parentOpKind!=kind::BUILTIN ){
+                    children.erase( children.begin(), children.begin() + 1 );
+                  }
                   Node progcr = Rewriter::rewrite( progcn );
                   Trace("sygus-nf-gen-debug") << "Var replace argument " << i << " : " << progcn << " -> " << progcr << std::endl;
                   if( progcr==progr ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 40fea68da..5f3498f49 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -389,7 +389,8 @@ bool CegInstantiation::getModelValues( CegConjecture * conj, std::vector< Node >
       TypeNode tn = nv.getType();
       Trace("cegqi-engine") << n[i] << " -> ";
       std::stringstream ss;
-      printSygusTerm( ss, nv );
+      std::vector< Node > lvs;
+      TermDbSygus::printSygusTerm( ss, nv, lvs );
       Trace("cegqi-engine") << ss.str() << " ";
     }
     if( nv.isNull() ){
@@ -522,7 +523,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
           if( sol.isNull() ){
             out << "?";
           }else{
-            printSygusTerm( out, sol );
+            std::vector< Node > lvs;
+            TermDbSygus::printSygusTerm( out, sol, lvs );
           }
         }
         out << ")" << std::endl;
@@ -531,33 +533,6 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
   }
 }
 
-void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) {
-  if( n.getKind()==APPLY_CONSTRUCTOR ){
-    TypeNode tn = n.getType();
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    if( dt.isSygus() ){
-      int cIndex = Datatype::indexOf( n.getOperator().toExpr() );
-      Assert( !dt[cIndex].getSygusOp().isNull() );
-      if( n.getNumChildren()>0 ){
-        out << "(";
-      }
-      out << dt[cIndex].getSygusOp();
-      if( n.getNumChildren()>0 ){
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          out << " ";
-          printSygusTerm( out, n[i] );
-        }
-        out << ")";
-      }
-      return;
-    }
-  }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){
-    out << n.getAttribute(SygusProxyAttribute());
-  }else{
-    out << n;
-  }
-}
-
 void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
   if( n.getKind()==OR ){
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 09e449b35..74e9b0aba 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -116,9 +116,6 @@ private:
   Node getModelValue( Node n );
   /** get model term */
   Node getModelTerm( Node n );
-private:
-  /** print sygus term */
-  void printSygusTerm( std::ostream& out, Node n );
 public:
   CegInstantiation( QuantifiersEngine * qe, context::Context* c );
 public:
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d57f52b35..79199d8b4 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1511,7 +1511,9 @@ Node TermDbSygus::getGenericBase( TypeNode tn, const Datatype& dt, int c ) {
     std::map< TypeNode, int > var_count;
     std::map< int, Node > pre;
     Node g = mkGeneric( dt, c, var_count, pre );
+    Trace("sygus-db-debug") << "Sygus DB : Generic is " << g << std::endl;
     Node gr = Rewriter::rewrite( g );
+    Trace("sygus-db-debug") << "Sygus DB : Generic rewritten is " << gr << std::endl;
     gr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( gr.toExpr() ) );
     Trace("sygus-db") << "Sygus DB : Generic base " << dt[c].getName() << " : " << gr << std::endl;
     d_generic_base[tn][c] = gr;
@@ -1530,6 +1532,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
   if( op.getKind()!=BUILTIN ){
     children.push_back( op );
   }
+  Trace("sygus-db") << "mkGeneric " << dt.getName() << " " << op << " " << op.getKind() << "..." << std::endl;
   for( int i=0; i<(int)dt[c].getNumArgs(); i++ ){
     TypeNode tna = TypeNode::fromType( ((SelectorType)dt[c][i].getType()).getRangeType() );
     Node a;
@@ -1542,13 +1545,14 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
     Assert( !a.isNull() );
     children.push_back( a );
   }
+  Node ret;
   if( op.getKind()==BUILTIN ){
-    return NodeManager::currentNM()->mkNode( op, children );
+    ret = NodeManager::currentNM()->mkNode( op, children );
   }else{
     if( children.size()==1 ){
-      return children[0];
+      ret = children[0];
     }else{
-      return NodeManager::currentNM()->mkNode( APPLY, children );
+      ret = NodeManager::currentNM()->mkNode( APPLY, children );
       /*
       Node n = NodeManager::currentNM()->mkNode( APPLY, children );
       //must expand definitions
@@ -1558,6 +1562,8 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
       */
     }
   }
+  Trace("sygus-db") << "...returning " << ret << std::endl;
+  return ret;
 }
 
 Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
@@ -1573,7 +1579,9 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
       pre[j] = sygusToBuiltin( n[j], getArgType( dt[i], j ) );
     }
     Node ret = mkGeneric( dt, i, var_count, pre );
+    Trace("sygus-db-debug") << "SygusToBuiltin : Generic is " << ret << std::endl;
     ret = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( ret.toExpr() ) );
+    Trace("sygus-db-debug") << "SygusToBuiltin : After expand definitions " << ret << std::endl;
     d_sygus_to_builtin[tn][n] = ret;
     return ret;
   }else{
@@ -2030,4 +2038,80 @@ Node TermDbSygus::expandBuiltinTerm( Node t ){
                                                  NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
   }
   return Node::null();
-}
\ No newline at end of file
+}
+
+
+void doReplace(std::string& str, const std::string& oldStr, const std::string& newStr){
+  size_t pos = 0;
+  while((pos = str.find(oldStr, pos)) != std::string::npos){
+     str.replace(pos, oldStr.length(), newStr);
+     pos += newStr.length();
+  }
+}
+
+void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ) {
+  if( n.getKind()==APPLY_CONSTRUCTOR ){
+    TypeNode tn = n.getType();
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    if( dt.isSygus() ){
+      int cIndex = Datatype::indexOf( n.getOperator().toExpr() );
+      Assert( !dt[cIndex].getSygusOp().isNull() );
+      if( dt[cIndex].getSygusLetBody().isNull() ){
+        if( n.getNumChildren()>0 ){
+          out << "(";
+        }
+        out << dt[cIndex].getSygusOp();
+        if( n.getNumChildren()>0 ){
+          for( unsigned i=0; i<n.getNumChildren(); i++ ){
+            out << " ";
+            printSygusTerm( out, n[i], lvs );
+          }
+          out << ")";
+        }
+      }else{
+        //print as let term
+        out << "(let (";
+        std::vector< Node > subs_lvs;
+        std::vector< Node > new_lvs;
+        for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
+          Node v = Node::fromExpr( dt[cIndex].getSygusLetArg( i ) );
+          subs_lvs.push_back( v );
+          std::stringstream ss;
+          ss << "_l_" << new_lvs.size();
+          Node lv = NodeManager::currentNM()->mkBoundVar( ss.str(), v.getType() );
+          new_lvs.push_back( lv );
+          //map free variables to proper terms
+          if( i<dt[cIndex].getNumSygusLetInputArgs() ){
+            //it should be printed as a let argument
+            out << "(";
+            out << lv << " " << lv.getType() << " ";
+            printSygusTerm( out, n[i], lvs );
+            out << ")";
+          }
+        }
+        out << ") ";
+        //print the body
+        Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() );
+        let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() );
+        new_lvs.insert( new_lvs.end(), lvs.begin(), lvs.end() );
+        std::stringstream body_out;
+        printSygusTerm( body_out, let_body, new_lvs );
+        std::string body = body_out.str();
+        for( unsigned i=dt[cIndex].getNumSygusLetInputArgs(); i<dt[cIndex].getNumSygusLetArgs(); i++ ){ 
+          std::stringstream old_str;
+          old_str << new_lvs[i];
+          std::stringstream new_str;
+          printSygusTerm( new_str, n[i], lvs );
+          doReplace( body, old_str.str().c_str(), new_str.str().c_str() );
+        }
+        out << body << ")";
+      }
+      return;
+    }
+  }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){
+    out << n.getAttribute(SygusProxyAttribute());
+  }else{
+    out << n;
+  }
+}
+
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 37b1528b3..0bb2c3224 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -459,6 +459,8 @@ public:
   Node minimizeBuiltinTerm( Node n );
   /** given a term, expand it into more basic components */
   Node expandBuiltinTerm( Node n );
+  /** print sygus term */
+  static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs );
 };
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 5a7a6da89..b1ab011ef 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -607,15 +607,14 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
   CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 }
 
-DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester, Expr sygus_op) :
-  d_name(name + '\0' + tester),
-  d_tester(),
-  d_args(),
-  d_sygus_op(sygus_op) {
-  CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
-  CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){
+  d_sygus_op = op;
+  d_sygus_let_body = let_body;
+  d_sygus_let_args.insert( d_sygus_let_args.end(), let_args.begin(), let_args.end() );
+  d_sygus_num_let_input_args = num_let_input_args;
 }
 
+
 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // We don't want to introduce a new data member, because eventually
   // we're going to be a constant stuffed inside a node.  So we stow
@@ -689,6 +688,26 @@ Expr DatatypeConstructor::getSygusOp() const {
   return d_sygus_op;
 }
 
+Expr DatatypeConstructor::getSygusLetBody() const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_let_body;
+}
+
+unsigned DatatypeConstructor::getNumSygusLetArgs() const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_let_args.size();
+}
+
+Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_let_args[i];
+} 
+
+unsigned DatatypeConstructor::getNumSygusLetInputArgs() const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_num_let_input_args;
+}
+  
 Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 224ac89ad..1945c4390 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -187,6 +187,9 @@ private:
   std::vector<DatatypeConstructorArg> d_args;
   /** the operator associated with this constructor (for sygus) */
   Expr d_sygus_op;
+  Expr d_sygus_let_body;
+  std::vector< Expr > d_sygus_let_args;
+  unsigned d_sygus_num_let_input_args;
 
   void resolve(ExprManager* em, DatatypeType self,
                const std::map<std::string, DatatypeType>& resolutions,
@@ -232,7 +235,9 @@ public:
    * constructor and tester aren't created until resolution time.
    */
   DatatypeConstructor(std::string name, std::string tester);
-  DatatypeConstructor(std::string name, std::string tester, Expr sygus_op);
+  
+  /** set sygus */
+  void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus );
 
   /**
    * Add an argument (i.e., a data field) of the given name and type
@@ -281,7 +286,15 @@ public:
   
   /** get sygus op */
   Expr getSygusOp() const;
-
+  /** get sygus let body */
+  Expr getSygusLetBody() const;
+  /** get number of sygus let args */
+  unsigned getNumSygusLetArgs() const;
+  /** get sygus let arg */
+  Expr getSygusLetArg( unsigned i ) const;
+  /** get number of let arguments that should be printed as arguments to let */
+  unsigned getNumSygusLetInputArgs() const;
+  
   /**
    * Get the tester name for this Datatype constructor.
    */