Sygus Lambda Grammars (#1390)

2 files changed, 41 insertions, 98 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index f654f2608..513cb2170 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -181,25 +181,18 @@ 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 ) {
+void Datatype::addSygusConstructor(CVC4::Expr op,
+                                   std::string& cname,
+                                   std::vector<CVC4::Type>& cargs,
+                                   std::shared_ptr<SygusPrintCallback> spc)
+{
   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
-    }
-  }
+  Debug("dt-sygus") << "    sygus op : " << op << std::endl;
   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 );
+  c.setSygus(op, spc);
   for( unsigned j=0; j<cargs.size(); j++ ){
     Debug("parser-sygus-debug") << "  arg " << j << " : " << cargs[j] << std::endl;
     std::stringstream sname;
@@ -208,13 +201,6 @@ void Datatype::addSygusConstructor( CVC4::Expr op, std::string& cname, std::vect
   }
   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");
@@ -784,7 +770,8 @@ DatatypeConstructor::DatatypeConstructor(std::string name)
       d_name(name + '\0' + "is_" + name),  // default tester name is "is_FOO"
       d_tester(),
       d_args(),
-      d_sygus_num_let_input_args(0) {
+      d_sygus_pc(nullptr)
+{
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 }
 
@@ -796,16 +783,19 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester)
       d_name(name + '\0' + tester),
       d_tester(),
       d_args(),
-      d_sygus_num_let_input_args(0) {
+      d_sygus_pc(nullptr)
+{
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
   PrettyCheckArgument(!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 ){
+void DatatypeConstructor::setSygus(Expr op,
+                                   std::shared_ptr<SygusPrintCallback> spc)
+{
+  PrettyCheckArgument(
+      !isResolved(), this, "cannot modify a finalized Datatype constructor");
   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;
+  d_sygus_pc = spc;
 }
 
 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
@@ -882,37 +872,18 @@ Expr DatatypeConstructor::getSygusOp() const {
   return d_sygus_op;
 }
 
-Expr DatatypeConstructor::getSygusLetBody() const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_let_body;
-}
-
-unsigned DatatypeConstructor::getNumSygusLetArgs() const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_let_args.size();
-}
-
-Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_let_args[i];
-}
-
-unsigned DatatypeConstructor::getNumSygusLetInputArgs() const {
-  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_num_let_input_args;
-}
-
 bool DatatypeConstructor::isSygusIdFunc() const {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-  return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body;
+  return (d_sygus_op.getKind() == kind::LAMBDA
+          && d_sygus_op[0].getNumChildren() == 1
+          && d_sygus_op[0][0] == d_sygus_op[1]);
 }
 
 SygusPrintCallback* DatatypeConstructor::getSygusPrintCallback() const
 {
   PrettyCheckArgument(
       isResolved(), this, "this datatype constructor is not yet resolved");
-  // TODO  (#1344) return the stored callback
-  return nullptr;
+  return d_sygus_pc.get();
 }
 
 Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) {
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index a92a0738e..85ecfb946 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -191,7 +191,7 @@ class CVC4_PUBLIC SygusPrintCallback
 {
  public:
   SygusPrintCallback() {}
-  ~SygusPrintCallback() {}
+  virtual ~SygusPrintCallback() {}
   /**
    * Writes the term that sygus datatype expression e
    * encodes to stream out. p is the printer that
@@ -232,6 +232,7 @@ class CVC4_PUBLIC DatatypeConstructor {
    */
   DatatypeConstructor(std::string name, std::string tester);
 
+  ~DatatypeConstructor() {}
   /**
    * Add an argument (i.e., a data field) of the given name and type
    * to this Datatype constructor.  Selector names need not be unique;
@@ -287,29 +288,10 @@ class CVC4_PUBLIC DatatypeConstructor {
    * deep embedding.
    */
   Expr getSygusOp() const;
-  /** get sygus let body
-   *
-   * The sygus official format
-   * (http://www.sygus.org/SyGuS-COMP2015.html)
-   * allows for let expressions to occur in grammars.
-   *
-   * TODO (#1344) refactor this
-   */
-  Expr getSygusLetBody() const;
-  /** get number of sygus let args
-   * TODO (#1344) refactor this
-   */
-  unsigned getNumSygusLetArgs() const;
-  /** get sygus let arg
-   * TODO (#1344) refactor this
-   */
-  Expr getSygusLetArg( unsigned i ) const;
-  /** get number of let arguments that should be printed as arguments to let
-   * TODO (#1344) refactor this
-   */
-  unsigned getNumSygusLetInputArgs() const;
   /** is this a sygus identity function?
-   * TODO (#1344) refactor this
+   *
+   * This returns true if the sygus operator of this datatype constructor is
+   * of the form (lambda (x) x).
    */
   bool isSygusIdFunc() const;
   /** get sygus print callback
@@ -431,11 +413,13 @@ class CVC4_PUBLIC DatatypeConstructor {
   int getSelectorIndexInternal( Expr sel ) const;
 
   /** involves external type
+   *
    * Get whether this constructor has a subfield
    * in any constructor that is not a datatype type.
    */
   bool involvesExternalType() const;
   /** involves external type
+   *
    * Get whether this constructor has a subfield
    * in any constructor that is an uninterpreted type.
    */
@@ -443,13 +427,11 @@ class CVC4_PUBLIC DatatypeConstructor {
 
   /** set sygus
    *
-   * Set that this constructor is a sygus datatype
-   * constructor that encodes operator op.
-   * The remaining arguments are for handling
-   * let expressions in user-provided sygus
-   * grammars (see above).
+   * Set that this constructor is a sygus datatype constructor that encodes
+   * operator op. spc is the sygus callback of this datatype constructor,
+   * which is stored in a shared pointer.
    */
-  void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus );
+  void setSygus(Expr op, std::shared_ptr<SygusPrintCallback> spc);
 
  private:
   /** the name of the constructor */
@@ -462,14 +444,11 @@ class CVC4_PUBLIC DatatypeConstructor {
   std::vector<DatatypeConstructorArg> d_args;
   /** sygus operator */
   Expr d_sygus_op;
-  /** sygus let body */
-  Expr d_sygus_let_body;
-  /** sygus let args */
-  std::vector<Expr> d_sygus_let_args;
-  /** sygus num let input args */
-  unsigned d_sygus_num_let_input_args;
+  /** sygus print callback */
+  std::shared_ptr<SygusPrintCallback> d_sygus_pc;
 
   /** shared selectors for each type
+   *
    * This stores the shared (constructor-agnotic)
    * selectors that access the fields of this datatype.
    * In the terminology of "Datatypes with Shared Selectors",
@@ -673,25 +652,18 @@ public:
    *      this constructor encodes
    * cname : the name of the constructor (for printing only)
    * cargs : the arguments of the constructor
+   * spc : an (optional) callback that is used for custom printing. This is
+   *       to accomodate user-provided grammars in the sygus format.
    *
    * It should be the case that cargs are sygus datatypes that
    * encode the arguments of op. For example, a sygus constructor
    * with op = PLUS should be such that cargs.size()>=2 and
    * the sygus type of cargs[i] is Real/Int for each i.
    */
-  void addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs );
-  /** add sygus constructor (for let expression constructors)
-   *
-   * This adds a sygus constructor to this datatype, where
-   * this datatype should be currently unresolved.
-   *
-   * In contrast to the above function, the constructor we
-   * add corresponds to a let expression if let_body is
-   * non-null. For details, see documentation for
-   * DatatypeConstructor::getSygusLetBody above.
-   */
-  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 );
+  void addSygusConstructor(CVC4::Expr op,
+                           std::string& cname,
+                           std::vector<CVC4::Type>& cargs,
+                           std::shared_ptr<SygusPrintCallback> spc = nullptr);
 
   /** set that this datatype is a tuple */
   void setTuple();