Update sygus v1 parser to use ParseOp utility (#3756)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 81328831a05ee1e526f096a0b1961a5ec423d2d0..975dd26f65f1e084d0cc22ed9901e86793970cba 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -924,6 +924,7 @@ install(FILES
           parser/parser.h
           parser/parser_builder.h
           parser/parser_exception.h
+          parser/parse_op.h
         DESTINATION
           ${INCLUDE_INSTALL_DIR}/cvc4/parser)
 install(FILES

diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 508a745320e99e16d0f21acb7779ebb48b202295..3cd6a7e51f5412d914132f7be508b20a38ab208c 100644 (file)
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -151,6 +151,7 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java
   ${CMAKE_CURRENT_BINARY_DIR}/Options.java
   ${CMAKE_CURRENT_BINARY_DIR}/OutputLanguage.java
+  ${CMAKE_CURRENT_BINARY_DIR}/ParseOp.java
   ${CMAKE_CURRENT_BINARY_DIR}/Parser.java
   ${CMAKE_CURRENT_BINARY_DIR}/ParserBuilder.java
   ${CMAKE_CURRENT_BINARY_DIR}/ParserEndOfFileException.java

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 7e5fb6d7debb633049c6fe6eaffe1c07a7ffca60..4d2467f84543d9af4ed8d4bdd5dac3d451d0eaae 100644 (file)
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -252,7 +252,18 @@ void Datatype::addSygusConstructor(Expr op,
   }
   addConstructor(c);
 }
-                                    
+
+void Datatype::addSygusConstructor(Kind k,
+                                   const std::string& cname,
+                                   const std::vector<Type>& cargs,
+                                   std::shared_ptr<SygusPrintCallback> spc,
+                                   int weight)
+{
+  ExprManagerScope ems(*d_em);
+  Expr op = d_em->operatorOf(k);
+  addSygusConstructor(op, cname, cargs, spc, weight);
+}
+
 void Datatype::setTuple() {
   PrettyCheckArgument(
       !isResolved(), this, "cannot set tuple to a finalized Datatype");

diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index dccda5ad445d02d6c0b0ebfd48329e31f9f7928e..1ae59f00c8d53f199f06bdc1bb2f2b4e8f3ab8f7 100644 (file)
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -630,6 +630,14 @@ class CVC4_PUBLIC Datatype {
                            const std::vector<Type>& cargs,
                            std::shared_ptr<SygusPrintCallback> spc = nullptr,
                            int weight = -1);
+  /**
+   * Same as above, with builtin kind k.
+   */
+  void addSygusConstructor(Kind k,
+                           const std::string& cname,
+                           const std::vector<Type>& cargs,
+                           std::shared_ptr<SygusPrintCallback> spc = nullptr,
+                           int weight = -1);
 
   /** set that this datatype is a tuple */
   void setTuple();

diff --git a/src/expr/datatype.i b/src/expr/datatype.i
index 6bd5eb82c7825fc5dab9d07b1343e809c205625e..83e21793cf077c16e5e2b318ba0617d07fb29610 100644 (file)
--- a/src/expr/datatype.i
+++ b/src/expr/datatype.i
@@ -9,6 +9,8 @@
 #endif /* SWIGJAVA */
 %}
 
+%include "expr/kind.i"
+
 %extend std::vector< CVC4::Datatype > {
   /* These member functions have slightly different signatures in
    * different swig language packages.  The underlying issue is that

diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index f2c1a6ef42de7f256ca08e0a62f1c5b8068ee884..77a9ba05347a4fa05c08c4057d59f7d0b4587f69 100644 (file)
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -32,12 +32,12 @@ set(libcvc4parser_src_files
   line_buffer.h
   memory_mapped_input_buffer.cpp
   memory_mapped_input_buffer.h
+  parse_op.h
   parser.cpp
   parser.h
   parser_builder.cpp
   parser_builder.h
   parser_exception.h
-  smt2/parse_op.h
   smt2/smt2.cpp
   smt2/smt2.h
   smt2/smt2_input.cpp

diff --git a/src/parser/cvc4parser.i b/src/parser/cvc4parser.i
index 2ad3bf01deced5ffe6ecb8cbaca955b70b7cd622..accb4826cc6adf80b020088372242e1a30fdae00 100644 (file)
--- a/src/parser/cvc4parser.i
+++ b/src/parser/cvc4parser.i
@@ -9,7 +9,8 @@ namespace CVC4 {}
 using namespace CVC4;
 %}
 
-%include "parser/parser_exception.i"
 %include "parser/input.i"
+%include "parser/parse_op.i"
 %include "parser/parser.i"
 %include "parser/parser_builder.i"
+%include "parser/parser_exception.i"

diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h
new file mode 100644 (file)
index 0000000..2465bf3
--- /dev/null
+++ b/src/parser/parse_op.h
@@ -0,0 +1,93 @@
+/*********************                                                        */
+/*! \file parse_op.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Definitions of parsed operators.
+ **/
+
+#include "cvc4parser_public.h"
+
+#ifndef CVC4__PARSER__PARSE_OP_H
+#define CVC4__PARSER__PARSE_OP_H
+
+#include <string>
+
+#include "expr/expr.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+
+/** A parsed operator
+ *
+ * The purpose of this struct is to store information regarding a parsed term
+ * that might not be ready to associate with an expression.
+ *
+ * While parsing terms in smt2, we may store a combination of one or more of
+ * the following to track how to process this term:
+ * (1) A kind.
+ * (2) A string name.
+ * (3) An expression expr.
+ * (4) A type t.
+ *
+ * Examples:
+ *
+ * - For declared functions f that we have not yet looked up in a symbol table,
+ * we store (2). We may store a name in a state if f is overloaded and we have
+ * not yet parsed its arguments to know how to disambiguate f.
+ * - For tuple selectors (_ tupSel n), we store (1) and (3). Kind is set to
+ * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the
+ * caller as the n^th generic tuple selector. We do this since there is no
+ * AST expression representing generic tuple select, and we do not have enough
+ * type information at this point to know the type of the tuple we will be
+ * selecting from.
+ * - For array constant specifications prior to type ascription e.g. when we
+ * have parsed "const", we store (1), setting the kind to STORE_ALL.
+ * - For array constant specifications (as const (Array T1 T2)), we store (1)
+ * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2).
+ * When parsing this as an operator e.g. ((as const (Array T1 T2)) t), we
+ * interpret this operator by converting the next parsed constant of type T2 to
+ * an Array of type (Array T1 T2) over that constant.
+ */
+struct CVC4_PUBLIC ParseOp
+{
+  ParseOp() : d_kind(kind::NULL_EXPR) {}
+  /** The kind associated with the parsed operator, if it exists */
+  Kind d_kind;
+  /** The name associated with the parsed operator, if it exists */
+  std::string d_name;
+  /** The expression associated with the parsed operator, if it exists */
+  Expr d_expr;
+  /** The type associated with the parsed operator, if it exists */
+  Type d_type;
+
+  /* Return true if this is equal to 'p'. */
+  bool operator==(const ParseOp& p) const
+  {
+    return d_kind == p.d_kind && d_name == p.d_name && d_expr == p.d_expr
+           && d_type == p.d_type;
+  }
+};
+
+inline std::ostream& operator<<(std::ostream& os, const ParseOp& p)
+{
+  if (!p.d_expr.isNull())
+  {
+    return os << p.d_expr;
+  }
+  else if (p.d_kind != kind::NULL_EXPR)
+  {
+    return os << p.d_kind;
+  }
+  return os << "ParseOp::unknown";
+}
+
+}  // namespace CVC4
+
+#endif /* CVC4__PARSER__PARSE_OP_H */

diff --git a/src/parser/parse_op.i b/src/parser/parse_op.i
new file mode 100644 (file)
index 0000000..37c3bd3
--- /dev/null
+++ b/src/parser/parse_op.i
@@ -0,0 +1,5 @@
+%{
+#include "parser/parse_op.h"
+%}
+
+%include "parser/parse_op.h"

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 9829b70d95b5d9907d19026a3d0ad076c74b70b3..af193c04bf288c91b543bb481deabc643a03ca78 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -138,6 +138,11 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) {
 }
 
 Kind Parser::getKindForFunction(Expr fun) {
+  Kind k = getExprManager()->operatorToKind(fun);
+  if (k != UNDEFINED_KIND)
+  {
+    return k;
+  }
   Type t = fun.getType();
   if (t.isFunction())
   {
@@ -155,11 +160,7 @@ Kind Parser::getKindForFunction(Expr fun) {
   {
     return APPLY_TESTER;
   }
-  else
-  {
-    parseError("internal error: unhandled function application kind");
-    return UNDEFINED_KIND;
-  }
+  return UNDEFINED_KIND;
 }
 
 Type Parser::getSort(const std::string& name) {

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 642b81fb07c4ea1e33b0acf5ab7689b7f63d285b..b0ef2328fb814d0a0623aef756a856cb5c1b6a8b 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -29,6 +29,7 @@
 #include "expr/kind.h"
 #include "expr/symbol_table.h"
 #include "parser/input.h"
+#include "parser/parse_op.h"
 #include "parser/parser_exception.h"
 #include "util/unsafe_interrupt_exception.h"
 
@@ -58,7 +59,8 @@ public:
     gterm_ignore,
   };
   Type d_type;
-  Expr d_expr;
+  /** The parsed operator */
+  ParseOp d_op;
   std::vector< Expr > d_let_vars;
   unsigned d_gterm_type;
   std::string d_name;
@@ -367,11 +369,12 @@ public:
   virtual Expr getExpressionForNameAndType(const std::string& name, Type t);
   
   /**
-   * Returns the kind that should be used for applications of expression fun, where
-   * fun has "function-like" type, i.e. where checkFunctionLike(fun) returns true. 
-   * Returns a parse error if fun does not have function-like type.
+   * Returns the kind that should be used for applications of expression fun.
+   * This is a generalization of ExprManager::operatorToKind that also
+   * handles variables whose types are "function-like", i.e. where
+   * checkFunctionLike(fun) returns true.
    * 
-   * For example, this function returns
+   * For examples of the latter, this function returns
    *   APPLY_UF if fun has function type, 
    *   APPLY_CONSTRUCTOR if fun has constructor type.
    */

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 30239dc2f733618aa42319cba3b01350b82ff07b..aed62f94cc40d4919e809aa88aa2a90c4726f81c 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -81,7 +81,7 @@ using namespace CVC4::parser;
 
 #include "parser/antlr_tracing.h"
 #include "parser/parser.h"
-#include "parser/smt2/parse_op.h"
+#include "parser/parse_op.h"
 #include "smt/command.h"
 
 namespace CVC4 {
@@ -662,7 +662,7 @@ sygusGrammarV1[CVC4::Type & ret,
   std::vector<std::vector<CVC4::SygusGTerm>> sgts;
   std::vector<CVC4::Datatype> datatypes;
   std::vector<Type> sorts;
-  std::vector<std::vector<Expr>> ops;
+  std::vector<std::vector<ParseOp>> ops;
   std::vector<std::vector<std::string>> cnames;
   std::vector<std::vector<std::vector<CVC4::Type>>> cargs;
   std::vector<bool> allow_const;
@@ -837,7 +837,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
           k = PARSER_STATE->getOperatorKind(name);
           sgt.d_name = kind::kindToString(k);
           sgt.d_gterm_type = SygusGTerm::gterm_op;
-          sgt.d_expr = EXPR_MANAGER->operatorOf(k);
+          sgt.d_op.d_kind = k;
         }else{
           // what is this sygus term trying to accomplish here, if the
           // symbol isn't yet declared?!  probably the following line will
@@ -853,7 +853,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
           }
           sgt.d_name = name;
           sgt.d_gterm_type = SygusGTerm::gterm_op;
-          sgt.d_expr = PARSER_STATE->getVariable(name) ;
+          sgt.d_op.d_expr = PARSER_STATE->getVariable(name) ;
         }
       }
     )
@@ -878,7 +878,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
                               << "expression " << atomTerm << std::endl;
         std::stringstream ss;
         ss << atomTerm;
-        sgt.d_expr = atomTerm.getExpr();
+        sgt.d_op.d_expr = atomTerm.getExpr();
         sgt.d_name = ss.str();
         sgt.d_gterm_type = SygusGTerm::gterm_op;
       }
@@ -888,13 +888,13 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
         Debug("parser-sygus") << "Sygus grammar " << fun
                               << " : unary minus integer literal " << name
                               << std::endl;
-        sgt.d_expr = MK_CONST(Rational(name));
+        sgt.d_op.d_expr = MK_CONST(Rational(name));
         sgt.d_name = name;
         sgt.d_gterm_type = SygusGTerm::gterm_op;
       }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){
         Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol "
                               << name << std::endl;
-        sgt.d_expr = PARSER_STATE->getExpressionForName(name);
+        sgt.d_op.d_expr = PARSER_STATE->getExpressionForName(name);
         sgt.d_name = name;
         sgt.d_gterm_type = SygusGTerm::gterm_op;
       }else{

diff --git a/src/parser/smt2/parse_op.h b/src/parser/smt2/parse_op.h
deleted file mode 100644 (file)
index 40b42d0..0000000
--- a/src/parser/smt2/parse_op.h
+++ /dev/null
@@ -1,74 +0,0 @@
-/*********************                                                        */
-/*! \file parse_op.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Definitions of parsed operators in smt2.
- **/
-
-#include "cvc4parser_private.h"
-
-#ifndef CVC4__PARSER__SMT2__PARSE_OP_H
-#define CVC4__PARSER__SMT2__PARSE_OP_H
-
-#include <string>
-
-#include "expr/expr.h"
-#include "expr/kind.h"
-
-namespace CVC4 {
-
-/** A parsed operator
- *
- * The purpose of this struct is to store information regarding a parsed term
- * in the smt2 language that might not be ready to associate with an
- * expression.
- *
- * While parsing terms in smt2, we may store a combination of one or more of
- * the following to track how to process this term:
- * (1) A kind.
- * (2) A string name.
- * (3) An expression expr.
- * (4) A type t.
- *
- * Examples:
- *
- * - For declared functions f that we have not yet looked up in a symbol table,
- * we store (2). We may store a name in a state if f is overloaded and we have
- * not yet parsed its arguments to know how to disambiguate f.
- * - For tuple selectors (_ tupSel n), we store (1) and (3). Kind is set to
- * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the
- * caller as the n^th generic tuple selector. We do this since there is no
- * AST expression representing generic tuple select, and we do not have enough
- * type information at this point to know the type of the tuple we will be
- * selecting from.
- * - For array constant specifications prior to type ascription e.g. when we
- * have parsed "const", we store (1), setting the kind to STORE_ALL.
- * - For array constant specifications (as const (Array T1 T2)), we store (1)
- * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2).
- * When parsing this as an operator e.g. ((as const (Array T1 T2)) t), we
- * interpret this operator by converting the next parsed constant of type T2 to
- * an Array of type (Array T1 T2) over that constant.
- */
-struct ParseOp
-{
-  ParseOp() : d_kind(kind::NULL_EXPR) {}
-  /** The kind associated with the parsed operator, if it exists */
-  Kind d_kind;
-  /** The name associated with the parsed operator, if it exists */
-  std::string d_name;
-  /** The expression associated with the parsed operator, if it exists */
-  Expr d_expr;
-  /** The type associated with the parsed operator, if it exists */
-  Type d_type;
-};
-
-}  // namespace CVC4
-
-#endif /* CVC4__PARSER__SMT2__PARSE_OP_H */

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 291885278107d424b52d0999db8164b26d7fe12a..3ab3c0eb168af408ac068f46162c1d2694dc7fbb 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -975,7 +975,7 @@ void Smt2::processSygusGTerm(
     int index,
     std::vector<CVC4::Datatype>& datatypes,
     std::vector<CVC4::Type>& sorts,
-    std::vector<std::vector<CVC4::Expr>>& ops,
+    std::vector<std::vector<ParseOp>>& ops,
     std::vector<std::vector<std::string>>& cnames,
     std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
     std::vector<bool>& allow_const,
@@ -988,19 +988,20 @@ void Smt2::processSygusGTerm(
 {
   if (sgt.d_gterm_type == SygusGTerm::gterm_op)
   {
-    Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index
-                          << std::endl;
+    Debug("parser-sygus") << "Add " << sgt.d_op << " to datatype "
+                          << index << std::endl;
     Kind oldKind;
     Kind newKind = kind::UNDEFINED_KIND;
     //convert to UMINUS if one child of MINUS
-    if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){
+    if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == kind::MINUS)
+    {
       oldKind = kind::MINUS;
       newKind = kind::UMINUS;
     }
     if( newKind!=kind::UNDEFINED_KIND ){
-      Expr newExpr = getExprManager()->operatorOf(newKind);
-      Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl;
-      sgt.d_expr = newExpr;
+      Debug("parser-sygus")
+          << "Replace " << sgt.d_op.d_kind << " with " << newKind << std::endl;
+      sgt.d_op.d_kind = newKind;
       std::string oldName = kind::kindToString(oldKind);
       std::string newName = kind::kindToString(newKind);
       size_t pos = 0;
@@ -1008,7 +1009,7 @@ void Smt2::processSygusGTerm(
         sgt.d_name.replace(pos, oldName.length(), newName);
       }
     }
-    ops[index].push_back( sgt.d_expr );
+    ops[index].push_back(sgt.d_op);
     cnames[index].push_back( sgt.d_name );
     cargs[index].push_back( std::vector< CVC4::Type >() );
     for( unsigned i=0; i<sgt.d_children.size(); i++ ){
@@ -1041,7 +1042,9 @@ void Smt2::processSygusGTerm(
       std::stringstream ss;
       ss << consts[i];
       Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
-      ops[index].push_back( consts[i] );
+      ParseOp constOp;
+      constOp.d_expr = consts[i];
+      ops[index].push_back(constOp);
       cnames[index].push_back( ss.str() );
       cargs[index].push_back( std::vector< CVC4::Type >() );
     }
@@ -1059,7 +1062,9 @@ void Smt2::processSygusGTerm(
         std::stringstream ss;
         ss << sygus_vars[i];
         Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
-        ops[index].push_back( sygus_vars[i] );
+        ParseOp varOp;
+        varOp.d_expr = sygus_vars[i];
+        ops[index].push_back(varOp);
         cnames[index].push_back( ss.str() );
         cargs[index].push_back( std::vector< CVC4::Type >() );
       }
@@ -1091,17 +1096,20 @@ void Smt2::processSygusGTerm(
   }
 }
 
-bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
-                                  std::vector< CVC4::Datatype >& datatypes,
-                                  std::vector< CVC4::Type>& sorts,
-                                  std::vector< std::vector<CVC4::Expr> >& ops,
-                                  std::vector< std::vector<std::string> >& cnames,
-                                  std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                                  std::vector< bool >& allow_const,
-                                  std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
+bool Smt2::pushSygusDatatypeDef(
+    Type t,
+    std::string& dname,
+    std::vector<CVC4::Datatype>& datatypes,
+    std::vector<CVC4::Type>& sorts,
+    std::vector<std::vector<ParseOp>>& ops,
+    std::vector<std::vector<std::string>>& cnames,
+    std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+    std::vector<bool>& allow_const,
+    std::vector<std::vector<std::string>>& unresolved_gterm_sym)
+{
   sorts.push_back(t);
   datatypes.push_back(Datatype(getExprManager(), dname));
-  ops.push_back(std::vector<Expr>());
+  ops.push_back(std::vector<ParseOp>());
   cnames.push_back(std::vector<std::string>());
   cargs.push_back(std::vector<std::vector<CVC4::Type> >());
   allow_const.push_back(false);
@@ -1109,13 +1117,15 @@ bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
   return true;
 }
 
-bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
-                                 std::vector< CVC4::Type>& sorts,
-                                 std::vector< std::vector<CVC4::Expr> >& ops,
-                                 std::vector< std::vector<std::string> >& cnames,
-                                 std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                                 std::vector< bool >& allow_const,
-                                 std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
+bool Smt2::popSygusDatatypeDef(
+    std::vector<CVC4::Datatype>& datatypes,
+    std::vector<CVC4::Type>& sorts,
+    std::vector<std::vector<ParseOp>>& ops,
+    std::vector<std::vector<std::string>>& cnames,
+    std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+    std::vector<bool>& allow_const,
+    std::vector<std::vector<std::string>>& unresolved_gterm_sym)
+{
   sorts.pop_back();
   datatypes.pop_back();
   ops.pop_back();
@@ -1126,15 +1136,20 @@ bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
   return true;
 }
 
-Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
-                                    std::vector< CVC4::Type>& sorts,
-                                    std::vector< std::vector<CVC4::Expr> >& ops,
-                                    std::vector< std::vector<std::string> >& cnames,
-                                    std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                                    std::vector< bool >& allow_const,
-                                    std::vector< std::vector< std::string > >& unresolved_gterm_sym,
-                                    std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
-                                    std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) {
+Type Smt2::processSygusNestedGTerm(
+    int sub_dt_index,
+    std::string& sub_dname,
+    std::vector<CVC4::Datatype>& datatypes,
+    std::vector<CVC4::Type>& sorts,
+    std::vector<std::vector<ParseOp>>& ops,
+    std::vector<std::vector<std::string>>& cnames,
+    std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+    std::vector<bool>& allow_const,
+    std::vector<std::vector<std::string>>& unresolved_gterm_sym,
+    std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
+    std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
+    Type sub_ret)
+{
   Type t = sub_ret;
   Debug("parser-sygus") << "Argument is ";
   if( t.isNull() ){
@@ -1145,9 +1160,12 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
     if( cargs[sub_dt_index].empty() ){
       parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
     }
-    Expr sop = ops[sub_dt_index][0];
+    ParseOp op = ops[sub_dt_index][0];
     Type curr_t;
-    if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){
+    if (!op.d_expr.isNull()
+        && (op.d_expr.isConst() || cargs[sub_dt_index][0].empty()))
+    {
+      Expr sop = op.d_expr;
       curr_t = sop.getType();
       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;
       // only cache if it is a singleton datatype (has unique expr)
@@ -1160,11 +1178,10 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
           d_sygus_bound_var_type[sop] = t;
         }
       }
-    }else{
+    }
+    else
+    {
       std::vector< Expr > children;
-      if( sop.getKind() != kind::BUILTIN ){
-        children.push_back( sop );
-      }
       for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
         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() ){
@@ -1189,11 +1206,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
           children.push_back( it->second );
         }
       }
-      Kind sk = sop.getKind() != kind::BUILTIN
-                    ? getKindForFunction(sop)
-                    : getExprManager()->operatorToKind(sop);
-      Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl;
-      Expr e = getExprManager()->mkExpr( sk, children );
+      Expr e = applyParseOp(op, children);
       Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
       curr_t = e.getType();
       sygus_to_builtin_expr[t] = e;
@@ -1214,12 +1227,12 @@ void Smt2::setSygusStartIndex(const std::string& fun,
                               int startIndex,
                               std::vector<CVC4::Datatype>& datatypes,
                               std::vector<CVC4::Type>& sorts,
-                              std::vector<std::vector<CVC4::Expr>>& ops)
+                              std::vector<std::vector<ParseOp>>& ops)
 {
   if( startIndex>0 ){
     CVC4::Datatype tmp_dt = datatypes[0];
     Type tmp_sort = sorts[0];
-    std::vector< Expr > tmp_ops;
+    std::vector<ParseOp> tmp_ops;
     tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
     datatypes[0] = datatypes[startIndex];
     sorts[0] = sorts[startIndex];
@@ -1236,10 +1249,13 @@ void Smt2::setSygusStartIndex(const std::string& fun,
   }
 }
 
-void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
-                            std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
-                            std::vector<std::string>& unresolved_gterm_sym,
-                            std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
+void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
+                           std::vector<ParseOp>& ops,
+                           std::vector<std::string>& cnames,
+                           std::vector<std::vector<CVC4::Type>>& cargs,
+                           std::vector<std::string>& unresolved_gterm_sym,
+                           std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin)
+{
   Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
   Debug("parser-sygus") << "  add constructors..." << std::endl;
   
@@ -1293,27 +1309,21 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
         Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
 
         // make the let_body
-        std::vector<Expr> children;
-        if (ops[i].getKind() != kind::BUILTIN)
-        {
-          children.push_back(ops[i]);
-        }
-        children.insert(children.end(), largs.begin(), largs.end());
-        Kind sk = ops[i].getKind() != kind::BUILTIN
-                      ? getKindForFunction(ops[i])
-                      : getExprManager()->operatorToKind(ops[i]);
-        Expr body = getExprManager()->mkExpr(sk, children);
+        Expr body = applyParseOp(ops[i], largs);
         // replace by lambda
-        ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
+        ParseOp pLam;
+        pLam.d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
+        ops[i] = pLam;
         Debug("parser-sygus") << "  ...replace op : " << ops[i] << std::endl;
         // callback prints as the expression
         spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs);
       }
       else
       {
-        if (ops[i].getType().isBitVector() && ops[i].isConst())
+        Expr sop = ops[i].d_expr;
+        if (!sop.isNull() && sop.getType().isBitVector() && sop.isConst())
         {
-          Debug("parser-sygus") << "--> Bit-vector constant " << ops[i] << " ("
+          Debug("parser-sygus") << "--> Bit-vector constant " << sop << " ("
                                 << cnames[i] << ")" << std::endl;
           // Since there are multiple output formats for bit-vectors and
           // we are required by sygus standards to print in the exact input
@@ -1321,22 +1331,22 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
           // the given name.
           spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
         }
-        else if (ops[i].getKind() == kind::VARIABLE)
+        else if (!sop.isNull() && sop.getKind() == kind::VARIABLE)
         {
           Debug("parser-sygus") << "--> Defined function " << ops[i]
                                 << std::endl;
           // turn f into (lammbda (x) (f x))
           // in a degenerate case, ops[i] may be a defined constant,
           // in which case we do not replace by a lambda.
-          if (ops[i].getType().isFunction())
+          if (sop.getType().isFunction())
           {
             std::vector<Type> ftypes =
-                static_cast<FunctionType>(ops[i].getType()).getArgTypes();
+                static_cast<FunctionType>(sop.getType()).getArgTypes();
             std::vector<Expr> largs;
             Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
-            largs.insert(largs.begin(), ops[i]);
+            largs.insert(largs.begin(), sop);
             Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs);
-            ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
+            ops[i].d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
             Debug("parser-sygus") << "  ...replace op : " << ops[i]
                                   << std::endl;
           }
@@ -1359,8 +1369,22 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       cnames[i] = ss.str();
       Debug("parser-sygus") << "  construct the datatype " << cnames[i] << "..."
                             << std::endl;
-      // add the sygus constructor
-      dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc);
+      // Add the sygus constructor, either using the expression operator of
+      // ops[i], or the kind.
+      if (!ops[i].d_expr.isNull())
+      {
+        dt.addSygusConstructor(ops[i].d_expr, cnames[i], cargs[i], spc);
+      }
+      else if (ops[i].d_kind != kind::NULL_EXPR)
+      {
+        dt.addSygusConstructor(ops[i].d_kind, cnames[i], cargs[i], spc);
+      }
+      else
+      {
+        std::stringstream ss;
+        ss << "unexpected parse operator for sygus constructor" << ops[i];
+        parseError(ss.str());
+      }
       Debug("parser-sygus") << "  finished constructing the datatype"
                             << std::endl;
     }
@@ -1400,7 +1424,9 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
           dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc);
 
           //add to operators
-          ops.push_back( id_op );
+          ParseOp idOp;
+          idOp.d_expr = id_op;
+          ops.push_back(idOp);
         }
       }else{
         std::stringstream ss;
@@ -1711,11 +1737,13 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
   {
     // An explicit operator, e.g. an indexed symbol.
     args.insert(args.begin(), p.d_expr);
-    if (p.d_expr.getType().isTester())
+    Kind fkind = getKindForFunction(p.d_expr);
+    if (fkind != kind::UNDEFINED_KIND)
     {
+      // Some operators may require a specific kind.
       // Testers are handled differently than other indexed operators,
       // since they require a kind.
-      kind = kind::APPLY_TESTER;
+      kind = fkind;
     }
   }
   else
@@ -1767,7 +1795,7 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
   // Second phase: apply the arguments to the parse op
   ExprManager* em = getExprManager();
   // handle special cases
-  if (p.d_kind == kind::STORE_ALL)
+  if (p.d_kind == kind::STORE_ALL && !p.d_type.isNull())
   {
     if (args.size() != 1)
     {
@@ -1812,12 +1840,8 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
     }
     return em->mkConst(ArrayStoreAll(p.d_type, constVal));
   }
-  else if (p.d_kind == kind::APPLY_SELECTOR)
+  else if (p.d_kind == kind::APPLY_SELECTOR && !p.d_expr.isNull())
   {
-    if (p.d_expr.isNull())
-    {
-      parseError("Could not process parsed tuple selector.");
-    }
     // tuple selector case
     Integer x = p.d_expr.getConst<Rational>().getNumerator();
     if (!x.fitsUnsignedInt())
@@ -1846,9 +1870,15 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
   }
   else if (p.d_kind != kind::NULL_EXPR)
   {
-    std::stringstream ss;
-    ss << "Could not process parsed qualified identifier kind " << p.d_kind;
-    parseError(ss.str());
+    // it should not have an expression or type specified at this point
+    if (!p.d_expr.isNull() || !p.d_type.isNull())
+    {
+      std::stringstream ss;
+      ss << "Could not process parsed qualified identifier kind " << p.d_kind;
+      parseError(ss.str());
+    }
+    // otherwise it is a simple application
+    kind = p.d_kind;
   }
   else if (isBuiltinOperator)
   {

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 4f09359166982201110a23a3645e0d481cf4f30e..6c12751158d8334b61afb8e21e12b86bcefba7bb 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -26,8 +26,8 @@
 #include <utility>
 
 #include "api/cvc4cpp.h"
+#include "parser/parse_op.h"
 #include "parser/parser.h"
-#include "parser/smt2/parse_op.h"
 #include "smt/command.h"
 #include "theory/logic_info.h"
 #include "util/abstract_value.h"
@@ -372,7 +372,7 @@ class Smt2 : public Parser
       int index,
       std::vector<CVC4::Datatype>& datatypes,
       std::vector<CVC4::Type>& sorts,
-      std::vector<std::vector<CVC4::Expr>>& ops,
+      std::vector<std::vector<ParseOp>>& ops,
       std::vector<std::vector<std::string>>& cnames,
       std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
       std::vector<bool>& allow_const,
@@ -388,7 +388,7 @@ class Smt2 : public Parser
       std::string& dname,
       std::vector<CVC4::Datatype>& datatypes,
       std::vector<CVC4::Type>& sorts,
-      std::vector<std::vector<CVC4::Expr>>& ops,
+      std::vector<std::vector<ParseOp>>& ops,
       std::vector<std::vector<std::string>>& cnames,
       std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
       std::vector<bool>& allow_const,
@@ -397,7 +397,7 @@ class Smt2 : public Parser
   bool popSygusDatatypeDef(
       std::vector<CVC4::Datatype>& datatypes,
       std::vector<CVC4::Type>& sorts,
-      std::vector<std::vector<CVC4::Expr>>& ops,
+      std::vector<std::vector<ParseOp>>& ops,
       std::vector<std::vector<std::string>>& cnames,
       std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
       std::vector<bool>& allow_const,
@@ -407,12 +407,14 @@ class Smt2 : public Parser
                           int startIndex,
                           std::vector<CVC4::Datatype>& datatypes,
                           std::vector<CVC4::Type>& sorts,
-                          std::vector<std::vector<CVC4::Expr>>& ops);
+                          std::vector<std::vector<ParseOp>>& ops);
 
-  void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
-                        std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
-                        std::vector<std::string>& unresolved_gterm_sym,
-                        std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin );
+  void mkSygusDatatype(CVC4::Datatype& dt,
+                       std::vector<ParseOp>& ops,
+                       std::vector<std::string>& cnames,
+                       std::vector<std::vector<CVC4::Type>>& cargs,
+                       std::vector<std::string>& unresolved_gterm_sym,
+                       std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin);
 
   /**
    * Adds a constructor to sygus datatype dt whose sygus operator is term.
@@ -584,15 +586,19 @@ class Smt2 : public Parser
  private:
   std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type;
 
-  Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
-                                std::vector< CVC4::Type>& sorts,
-                                std::vector< std::vector<CVC4::Expr> >& ops,
-                                std::vector< std::vector<std::string> >& cnames,
-                                std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                                std::vector< bool >& allow_const,
-                                std::vector< std::vector< std::string > >& unresolved_gterm_sym,
-                                std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
-                                std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret );
+  Type processSygusNestedGTerm(
+      int sub_dt_index,
+      std::string& sub_dname,
+      std::vector<CVC4::Datatype>& datatypes,
+      std::vector<CVC4::Type>& sorts,
+      std::vector<std::vector<ParseOp>>& ops,
+      std::vector<std::vector<std::string>>& cnames,
+      std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+      std::vector<bool>& allow_const,
+      std::vector<std::vector<std::string>>& unresolved_gterm_sym,
+      std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
+      std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
+      Type sub_ret);
 
   /** make sygus bound var list
    *