Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.

3 files changed, 152 insertions, 4 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 39bdddbad..4f1fc82b1 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -28,6 +28,7 @@
 #include "expr/node_manager.h"
 #include "expr/type.h"
 #include "options/set_language.h"
+#include "options/datatypes_options.h"
 
 using namespace std;
 
@@ -161,7 +162,7 @@ void Datatype::resolve(ExprManager* em,
     evalType.push_back(TypeNode::fromType(d_sygus_type));
     TypeNode eval_func_type = nm->mkFunctionType(evalType);
     d_sygus_eval = nm->mkSkolem(name, eval_func_type, "sygus evaluation function").toExpr();    
-  }  
+  }
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
@@ -180,6 +181,41 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
   d_sygus_allow_all = allow_all;
 }
 
+void Datatype::addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
+                                    CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) {
+  Debug("dt-sygus") << "--> Add constructor " << cname << " to " << getName() << std::endl;
+  if( !let_body.isNull() ){
+    Debug("dt-sygus") << "    let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl;
+    //TODO : remove arguments not occurring in body
+    //if this is a self identity function, ignore
+    if( let_args.size()==0 && let_args[0]==let_body ){
+      Debug("dt-sygus") << "    identity function " << cargs[0] << " to " << getName() << std::endl;
+      //TODO
+    }
+  }
+  std::string name = getName() + "_" + cname;
+  std::string testerId("is-");
+  testerId.append(name);
+  //checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+  //checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
+  CVC4::DatatypeConstructor c(name, testerId );
+  c.setSygus( op, let_body, let_args, let_num_input_args );
+  for( unsigned j=0; j<cargs.size(); j++ ){
+    Debug("parser-sygus-debug") << "  arg " << j << " : " << cargs[j] << std::endl;
+    std::stringstream sname;
+    sname << name << "_" << j;
+    c.addArg(sname.str(), cargs[j]);
+  }
+  addConstructor(c);
+}
+
+void Datatype::addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs ) {
+  CVC4::Expr let_body; 
+  std::vector< CVC4::Expr > let_args; 
+  unsigned let_num_input_args = 0;
+  addSygusConstructor( op, cname, cargs, let_body, let_args, let_num_input_args );
+}
+                                    
 void Datatype::setTuple() {
   PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype");
   d_isTuple = true;
@@ -584,6 +620,30 @@ const DatatypeConstructor& Datatype::operator[](std::string name) const {
   IllegalArgument(name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str());
 }
 
+
+Expr Datatype::getSharedSelector( Type dtt, Type t, unsigned index ) const{
+  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  std::map< Type, std::map< Type, std::map< unsigned, Expr > > >::iterator itd = d_shared_sel.find( dtt );
+  if( itd!=d_shared_sel.end() ){
+    std::map< Type, std::map< unsigned, Expr > >::iterator its = itd->second.find( t );
+    if( its!=itd->second.end() ){
+      std::map< unsigned, Expr >::iterator it = its->second.find( index );
+      if( it!=its->second.end() ){
+        return it->second;
+      }
+    }
+  }
+  //make the shared selector
+  Expr s;
+  NodeManager* nm = NodeManager::fromExprManager( d_self.getExprManager() );
+  std::stringstream ss;
+  ss << "sel_" << index;
+  s = nm->mkSkolem(ss.str(), nm->mkSelectorType(TypeNode::fromType(dtt), TypeNode::fromType(t)), "is a shared selector", NodeManager::SKOLEM_NO_NOTIFY).toExpr();
+  d_shared_sel[dtt][t][index] = s;
+  Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t << std::endl;
+  return s; 
+}
+
 Expr Datatype::getConstructor(std::string name) const {
   return (*this)[name].getConstructor();
 }
@@ -797,6 +857,7 @@ Expr DatatypeConstructor::getConstructor() const {
 
 Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(returnType.isDatatype(), this, "cannot get specialized constructor type for non-datatype type");
   ExprManagerScope ems(d_constructor);
   const Datatype& dt = Datatype::datatypeOf(d_constructor);
   PrettyCheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
@@ -1011,6 +1072,30 @@ Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& proces
   return groundTerm;
 }
 
+void DatatypeConstructor::computeSharedSelectors( Type domainType ) const {
+  if( d_shared_selectors[domainType].size()<getNumArgs() ){
+    TypeNode ctype;
+    if( DatatypeType(domainType).isParametric() ){
+      ctype = TypeNode::fromType( getSpecializedConstructorType( domainType ) );
+    }else{
+      ctype = TypeNode::fromType( d_constructor.getType() );
+    }
+    Assert( ctype.isConstructor() );
+    Assert( ctype.getNumChildren()-1==getNumArgs() );
+    //compute the shared selectors
+    const Datatype& dt = Datatype::datatypeOf(d_constructor);
+    std::map< TypeNode, unsigned > counter;
+    for( unsigned j=0; j<ctype.getNumChildren()-1; j++ ){
+      TypeNode t = ctype[j];
+      Expr ss = dt.getSharedSelector( domainType, t.toType(), counter[t] );
+      d_shared_selectors[domainType].push_back( ss );
+      Assert( d_shared_selector_index[domainType].find( ss )==d_shared_selector_index[domainType].end() );
+      d_shared_selector_index[domainType][ss] = j;
+      counter[t]++;
+    }
+  }
+}
+
 
 const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
   PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
@@ -1069,6 +1154,37 @@ Expr DatatypeConstructorArg::getSelector() const {
   return d_selector;
 }
 
+Expr DatatypeConstructor::getSelectorInternal( Type domainType, size_t index ) const {
+  PrettyCheckArgument(isResolved(), this, "cannot get an internal selector for an unresolved datatype constructor");
+  PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
+  if( options::dtSharedSelectors() ){
+    computeSharedSelectors( domainType );
+    Assert( d_shared_selectors[domainType].size()==getNumArgs() );
+    return d_shared_selectors[domainType][index];
+  }else{
+    return d_args[index].getSelector();
+  }
+}
+
+int DatatypeConstructor::getSelectorIndexInternal( Expr sel ) const {
+  PrettyCheckArgument(isResolved(), this, "cannot get an internal selector index for an unresolved datatype constructor");
+  if( options::dtSharedSelectors() ){
+    Assert( sel.getType().isSelector() );
+    Type domainType = ((SelectorType)sel.getType()).getDomain();
+    computeSharedSelectors( domainType );
+    std::map< Expr, unsigned >::iterator its = d_shared_selector_index[domainType].find( sel );
+    if( its!=d_shared_selector_index[domainType].end() ){
+      return (int)its->second;
+    }
+  }else{
+    unsigned sindex = Datatype::indexOf(sel);
+    if( getNumArgs() > sindex && d_args[sindex].getSelector() == sel ){
+      return (int)sindex;
+    }
+  }
+  return -1;
+}
+
 Expr DatatypeConstructorArg::getConstructor() const {
   PrettyCheckArgument(isResolved(), this,
                 "cannot get a associated constructor for argument of an unresolved datatype constructor");
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 456e70fd5..84588fef0 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -197,6 +197,10 @@ private:
   Expr d_sygus_let_body;
   std::vector< Expr > d_sygus_let_args;
   unsigned d_sygus_num_let_input_args;
+  
+  /** shared selectors */
+  mutable std::map< Type, std::vector< Expr > > d_shared_selectors;
+  mutable std::map< Type, std::map< Expr, unsigned > > d_shared_selector_index;
 
   void resolve(ExprManager* em, DatatypeType self,
                const std::map<std::string, DatatypeType>& resolutions,
@@ -226,6 +230,8 @@ private:
   bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException);
   /** compute ground term */
   Expr computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException);
+  /** compute shared selectors */
+  void computeSharedSelectors( Type domainType ) const;
 public:
   /**
    * Create a new Datatype constructor with the given name for the
@@ -378,6 +384,17 @@ public:
    */
   Expr getSelector(std::string name) const;
 
+
+  /**
+   * Get the internal selector for a constructor argument.
+   */
+  Expr getSelectorInternal( Type domainType, size_t index ) const;
+  
+  /** 
+   * Get the index for the selector
+   */
+  int getSelectorIndexInternal( Expr sel ) const;
+  
   /**
    * Get whether this datatype involves an external type.  If so,
    * then we will pose additional requirements for sharing.
@@ -506,6 +523,8 @@ private:
   mutable int d_well_founded;
   // ground term for this datatype
   mutable std::map< Type, Expr > d_ground_term;
+  // shared selectors
+  mutable std::map< Type, std::map< Type, std::map< unsigned, Expr > > > d_shared_sel;
 
   /**
    * Datatypes refer to themselves, recursively, and we have a
@@ -549,7 +568,9 @@ private:
   /** compute whether this datatype is well-founded */
   bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException);
   /** compute ground term */
-  Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException);
+  Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException);  
+  /** Get the shared selector */
+  Expr getSharedSelector( Type dtt, Type t, unsigned index ) const;
 public:
 
   /** Create a new Datatype of the given name. */
@@ -575,7 +596,11 @@ public:
    *    allow_const : whether all constants are (implicitly) included in the grammar
    */
   void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all );
-
+  /** add sygus constructor */
+  void addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs );
+  void addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
+                            CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args );
+                                    
   /** set tuple */
   void setTuple();
 
@@ -726,7 +751,7 @@ public:
    * similarly-named constructors, the first is returned.
    */
   const DatatypeConstructor& operator[](std::string name) const;
-
+ 
   /**
    * Get the constructor operator for the named constructor.
    * This is a linear search through the constructors, so in
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 262085a23..e45ca49e0 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -22,6 +22,8 @@
 #include "base/output.h"
 #include "expr/attribute.h"
 
+#include "theory/quantifiers/term_database.h"
+
 
 using namespace std;
 
@@ -111,6 +113,11 @@ bool NodeTemplate<ref_count>::hasBoundVar() {
       for(iterator i = begin(); i != end() && !hasBv; ++i) {
         hasBv = (*i).hasBoundVar();
       }
+      if( !hasBv ){
+        if( getKind()==kind::APPLY_UF && getOperator().hasAttribute(theory::SygusSynthFunVarListAttribute()) ){
+          hasBv = true;
+        }
+      }
     }
     setAttribute(HasBoundVarAttr(), hasBv);
     setAttribute(HasBoundVarComputedAttr(), true);