Properly parse qualified identifiers (#3111)

5 files changed, 387 insertions, 176 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index dec4ebc97..c8e09b8e0 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -110,7 +110,7 @@ Expr Parser::getExpressionForName(const std::string& name) {
 }
 
 Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) {
-  assert( isDeclared(name) );
+  assert(isDeclared(name));
   // first check if the variable is declared and not overloaded
   Expr expr = getVariable(name);
   if(expr.isNull()) {
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 663594ce8..2a736402e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1860,17 +1860,50 @@ symbolicExpr[CVC4::SExpr& sexpr]
 
 /**
  * Matches a term.
- * @return the expression representing the formula
+ * @return the expression representing the term.
  */
 term[CVC4::Expr& expr, CVC4::Expr& expr2]
 @init {
+  Kind kind = kind::NULL_EXPR;
+  Expr f;
   std::string name;
+  Type type;
 }
 : termNonVariable[expr, expr2]
-    /* a variable */
-  | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
-    { expr = PARSER_STATE->getExpressionForName(name);
-      assert( !expr.isNull() );
+
+  // a qualified identifier (section 3.6 of SMT-LIB version 2.6)
+
+  | qualIdentifier[kind,name,f,type]
+    {
+      if (kind != kind::NULL_EXPR || !type.isNull())
+      {
+        PARSER_STATE->parseError(
+            "Bad syntax for qualified identifier operator in term position.");
+      }
+      else if (!f.isNull())
+      {
+        expr = f;
+      }
+      else if (!PARSER_STATE->isDeclared(name,SYM_VARIABLE))
+      {
+        if (PARSER_STATE->sygus_v1() && name[0] == '-'
+            && name.find_first_not_of("0123456789", 1) == std::string::npos)
+        {
+          // allow unary minus in sygus version 1
+          expr = MK_CONST(Rational(name));
+        }
+        else
+        {
+          std::stringstream ss;
+          ss << "Symbol " << name << " is not declared.";
+          PARSER_STATE->parseError(ss.str());
+        }
+      }
+      else
+      {
+        expr = PARSER_STATE->getExpressionForName(name);
+      }
+      assert(!expr.isNull());
     }
   ;
 
@@ -1883,11 +1916,13 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
 @init {
   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
   Kind kind = kind::NULL_EXPR;
-  Expr op;
+  Kind qkind = kind::NULL_EXPR;
   std::string name;
   std::vector<Expr> args;
   std::vector< std::pair<std::string, Type> > sortedVarNames;
   Expr f, f2, f3;
+  Expr qexpr;
+  Type qtype;
   std::string attr;
   Expr attexpr;
   std::vector<Expr> patexprs;
@@ -1896,56 +1931,13 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
   std::vector< std::pair<std::string, Expr> > binders;
   bool isBuiltinOperator = false;
   bool isOverloadedFunction = false;
-  bool readVariable = false;
   int match_vindex = -1;
   std::vector<Type> match_ptypes;
   Type type;
   Type type2;
   api::Term atomTerm;
 }
-  : LPAREN_TOK AS_TOK ( termNonVariable[f, f2] | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { readVariable = true; } )
-    sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
-    {
-      if(readVariable) {
-        Trace("parser-overloading") << "Getting variable expression of type " << name << " with type " << type << std::endl;
-        // get the variable expression for the type
-        f = PARSER_STATE->getExpressionForNameAndType(name, type);
-        assert( !f.isNull() );
-      }
-      if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) {
-        // could be a parametric type constructor or just an overloaded constructor
-        if(((DatatypeType)type).isParametric()) {
-          std::vector<CVC4::Expr> v;
-          Expr e = f.getOperator();
-          const DatatypeConstructor& dtc =
-              Datatype::datatypeOf(e)[Datatype::indexOf(e)];
-          v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
-                               MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() ));
-          v.insert(v.end(), f.begin(), f.end());
-          expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
-        }else{
-          expr = f;
-        }
-      } else if(f.getKind() == CVC4::kind::EMPTYSET) {
-        Debug("parser") << "Empty set encountered: " << f << " "
-                          << f2 << " " << type <<  std::endl;
-        expr = MK_CONST( ::CVC4::EmptySet(type) );
-      } else if(f.getKind() == CVC4::kind::UNIVERSE_SET) {
-        expr = EXPR_MANAGER->mkNullaryOperator(type, kind::UNIVERSE_SET);
-      } else if(f.getKind() == CVC4::kind::SEP_NIL) {
-        //We don't want the nil reference to be a constant: for instance, it
-        //could be of type Int but is not a const rational. However, the
-        //expression has 0 children. So we convert to a SEP_NIL variable.
-        expr = EXPR_MANAGER->mkNullaryOperator(type, kind::SEP_NIL);
-      } else {
-        if(f.getType() != type) {
-          PARSER_STATE->parseError("Type ascription not satisfied.");
-        }else{
-          expr = f;
-        }
-      }
-    }
-  | LPAREN_TOK quantOp[kind]
+  : LPAREN_TOK quantOp[kind]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     {
       PARSER_STATE->pushScope(true);
@@ -1982,31 +1974,62 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_EXPR(kind, args);
       }
     }
-  | LPAREN_TOK functionName[name, CHECK_NONE]
-    { isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
-      if(isBuiltinOperator) {
-        /* A built-in operator */
-        kind = PARSER_STATE->getOperatorKind(name);
-      } else {
-        /* A non-built-in function application */
-        PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
-        expr = PARSER_STATE->getVariable(name);
-        if(!expr.isNull()) {
-          PARSER_STATE->checkFunctionLike(expr);
-          kind = PARSER_STATE->getKindForFunction(expr);
-          args.push_back(expr);
-        }else{
-          isOverloadedFunction = true;
+  | LPAREN_TOK qualIdentifier[qkind,name,qexpr,qtype]
+    {
+      // process the operator
+      Debug("parser") << "Parsed qual id: " << qkind << "/" << name << "/"
+                      << qexpr << "/" << qtype << std::endl;
+      if (qkind != kind::NULL_EXPR)
+      {
+        // It is a special case, e.g. tupSel or array constant specification.
+        // We have to wait until the arguments are parsed to resolve it.
+      }
+      else if (!qexpr.isNull())
+      {
+        // An explicit operator, e.g. an indexed symbol.
+        args.push_back(qexpr);
+        if (qexpr.getType().isTester())
+        {
+          kind = kind::APPLY_TESTER;
+        }
+      }
+      else
+      {
+        isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
+        if (isBuiltinOperator)
+        {
+          // a builtin operator, convert to kind
+          kind = PARSER_STATE->getOperatorKind(name);
+        }
+        else
+        {
+          // A non-built-in function application, get the expression
+          PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
+          expr = PARSER_STATE->getVariable(name);
+          if (!expr.isNull())
+          {
+            PARSER_STATE->checkFunctionLike(expr);
+            kind = PARSER_STATE->getKindForFunction(expr);
+            args.push_back(expr);
+          }
+          else
+          {
+            // Could not find the expression. It may be an overloaded symbol,
+            // in which case we may find it after knowing the types of its
+            // arguments.
+            isOverloadedFunction = true;
+          }
         }
       }
     }
-    //(termList[args,expr])? RPAREN_TOK
     termList[args,expr] RPAREN_TOK
     { Debug("parser") << "args has size " << args.size() << std::endl
                       << "expr is " << expr << std::endl;
       for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
         Debug("parser") << "++ " << *i << std::endl;
       }
+      // We now can figure out what the operator is, if we guessed it was
+      // overloaded.
       if(isOverloadedFunction) {
         std::vector< Type > argTypes;
         for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
@@ -2021,10 +2044,79 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
           PARSER_STATE->parseError("Cannot find unambiguous overloaded function for argument types.");
         }
       }
-
-      bool done = false;
-      if (isBuiltinOperator)
+      // handle special cases
+      if (qkind == kind::STORE_ALL)
       {
+        if (args.size() != 1)
+        {
+          PARSER_STATE->parseError("Too many arguments to array constant.");
+        }
+        if (!args[0].isConst())
+        {
+          std::stringstream ss;
+          ss << "expected constant term inside array constant, but found "
+             << "nonconstant term:" << std::endl
+             << "the term: " << args[0];
+          PARSER_STATE->parseError(ss.str());
+        }
+        ArrayType aqtype = static_cast<ArrayType>(qtype);
+        if (!aqtype.getConstituentType().isComparableTo(args[0].getType()))
+        {
+          std::stringstream ss;
+          ss << "type mismatch inside array constant term:" << std::endl
+             << "array type:          " << qtype << std::endl
+             << "expected const type: " << aqtype.getConstituentType()
+             << std::endl
+             << "computed const type: " << args[0].getType();
+          PARSER_STATE->parseError(ss.str());
+        }
+        expr = MK_CONST(CVC4::ArrayStoreAll(qtype, args[0]));
+      }
+      else if (qkind == kind::APPLY_SELECTOR)
+      {
+        if (qexpr.isNull())
+        {
+          PARSER_STATE->parseError("Could not process parsed tuple selector.");
+        }
+        // tuple selector case
+        Integer x = qexpr.getConst<CVC4::Rational>().getNumerator();
+        if (!x.fitsUnsignedInt())
+        {
+          PARSER_STATE->parseError(
+              "index of tupSel is larger than size of unsigned int");
+        }
+        unsigned int n = x.toUnsignedInt();
+        if (args.size() > 1)
+        {
+          PARSER_STATE->parseError(
+              "tupSel applied to more than one tuple argument");
+        }
+        Type t = args[0].getType();
+        if (!t.isTuple())
+        {
+          PARSER_STATE->parseError("tupSel applied to non-tuple");
+        }
+        size_t length = ((DatatypeType)t).getTupleLength();
+        if (n >= length)
+        {
+          std::stringstream ss;
+          ss << "tuple is of length " << length << "; cannot access index "
+             << n;
+          PARSER_STATE->parseError(ss.str());
+        }
+        const Datatype& dt = ((DatatypeType)t).getDatatype();
+        expr = dt[0][n].getSelector();
+        expr = MK_EXPR(kind::APPLY_SELECTOR, expr, args);
+      }
+      else if (qkind != kind::NULL_EXPR)
+      {
+        std::stringstream ss;
+        ss << "Could not process parsed qualified identifier kind " << qkind;
+        PARSER_STATE->parseError(ss.str());
+      }
+      else if (isBuiltinOperator)
+      {
+        bool done = false;
         if (args.size() > 2)
         {
           if (kind == CVC4::kind::INTS_DIVISION || kind == CVC4::kind::XOR
@@ -2083,6 +2175,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
       }
       else
       {
+        bool done = false;
         if (args.size() >= 2)
         {
           // may be partially applied function, in this case we use HO_APPLY
@@ -2105,73 +2198,18 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
 
         if (!done)
         {
-          expr = MK_EXPR(kind, args);
-        }
-      }
-    }
-  | LPAREN_TOK
-    ( /* An indexed function application */
-      indexedFunctionName[op, kind] termList[args,expr] RPAREN_TOK {
-        if(kind==CVC4::kind::APPLY_SELECTOR) {
-          //tuple selector case
-          Integer x = op.getConst<CVC4::Rational>().getNumerator();
-          if (!x.fitsUnsignedInt()) {
-            PARSER_STATE->parseError("index of tupSel is larger than size of unsigned int");
-          }
-          unsigned int n = x.toUnsignedInt();
-          if (args.size()>1) {
-            PARSER_STATE->parseError("tupSel applied to more than one tuple argument");
-          }
-          Type t = args[0].getType();
-          if (!t.isTuple()) {
-            PARSER_STATE->parseError("tupSel applied to non-tuple");
+          if (kind == kind::NULL_EXPR)
+          {
+            std::vector<Expr> eargs(args.begin() + 1, args.end());
+            expr = MK_EXPR(args[0], eargs);
           }
-          size_t length = ((DatatypeType)t).getTupleLength();
-          if (n >= length) {
-            std::stringstream ss;
-            ss << "tuple is of length " << length << "; cannot access index " << n;
-            PARSER_STATE->parseError(ss.str());
+          else
+          {
+            expr = MK_EXPR(kind, args);
           }
-          const Datatype & dt = ((DatatypeType)t).getDatatype();
-          op = dt[0][n].getSelector();
         }
-        if (kind!=kind::NULL_EXPR) {
-          expr = MK_EXPR( kind, op, args );
-        } else {
-          expr = MK_EXPR(op, args);
-        }
-        PARSER_STATE->checkOperator(expr.getKind(), args.size());
       }
-    | /* Array constant (in Z3 syntax) */
-      LPAREN_TOK AS_TOK CONST_TOK sortSymbol[type, CHECK_DECLARED]
-      RPAREN_TOK term[f, f2] RPAREN_TOK
-      {
-        if(!type.isArray()) {
-          std::stringstream ss;
-          ss << "expected array constant term, but cast is not of array type"
-             << std::endl
-             << "cast type: " << type;
-          PARSER_STATE->parseError(ss.str());
-        }
-        if(!f.isConst()) {
-          std::stringstream ss;
-          ss << "expected constant term inside array constant, but found "
-             << "nonconstant term:" << std::endl
-             << "the term: " << f;
-          PARSER_STATE->parseError(ss.str());
-        }
-        if(!ArrayType(type).getConstituentType().isComparableTo(f.getType())) {
-          std::stringstream ss;
-          ss << "type mismatch inside array constant term:" << std::endl
-             << "array type:          " << type << std::endl
-             << "expected const type: " << ArrayType(type).getConstituentType()
-             << std::endl
-             << "computed const type: " << f.getType();
-          PARSER_STATE->parseError(ss.str());
-        }
-        expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) );
-      }
-    )
+    }
   | /* a let or sygus let binding */
     LPAREN_TOK (
       LET_TOK LPAREN_TOK
@@ -2401,7 +2439,6 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
       PARSER_STATE->popScope();
       expr = MK_EXPR( CVC4::kind::LAMBDA, args );
     }
-
   | LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK
   {
     std::vector<api::Sort> sorts;
@@ -2419,6 +2456,211 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
 
 
 /**
+ * Matches a qualified identifier, which can be a combination of one or more of
+ * the following:
+ * (1) A kind.
+ * (2) A string name.
+ * (3) An expression expr.
+ * (4) A type t.
+ *
+ * A qualified identifier is the generic case of function heads.
+ * With respect to the standard definition (Section 3.6 of SMT-LIB version 2.6)
+ * of qualified identifiers, we additionally parse:
+ * - "Array constant specifications" of the form (as const (Array T1 T2)),
+ * which notice are used as function heads e.g. ((as const (Array Int Int)) 0)
+ * specifies the constant array over integers consisting of constant 0. This
+ * is handled as if it were a special case of an operator here.
+ *
+ * Examples:
+ *
+ * (Identifiers)
+ *
+ * - For declared functions f, we return (2).
+ * - For indexed functions like testers (_ is C) and bitvector extract
+ * (_ extract n m), we return (3) for the appropriate operator.
+ * - For tuple selectors (_ tupSel n), we return (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.
+ *
+ * (Ascripted Identifiers)
+ *
+ * - For ascripted nullary parametric datatype constructors like
+ * (as nil (List Int)), we return (APPLY_CONSTRUCTOR C) for the appropriate
+ * specialized constructor C as (3).
+ * - For ascripted non-nullary parametric datatype constructors like
+ * (as cons (List Int)), we return the appropriate specialized constructor C
+ * as (3).
+ * - Overloaded non-parametric constructors (as C T) return the appropriate
+ * expression, analogous to the parametric cases above.
+ * - For other ascripted nullary constants like (as emptyset (Set T)),
+ * (as sep.nil T), we return the appropriate expression (3).
+ * - For array constant specifications (as const (Array T1 T2)), we return (1)
+ * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2),
+ * where this is to be interpreted by the caller as converting the next parsed
+ * constant of type T2 to an Array of type (Array T1 T2) over that constant.
+ * - For ascriptions on normal symbols (as f T), we return the appropriate
+ * expression (3), which may involve disambiguating f based on type T if it is
+ * overloaded.
+ */
+qualIdentifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr, CVC4::Type& t]
+@init {
+  Kind k;
+  std::string baseName;
+  Expr f;
+  Type type;
+}
+: identifier[kind,name,expr]
+  | LPAREN_TOK AS_TOK
+    ( CONST_TOK sortSymbol[t, CHECK_DECLARED]
+      {
+        if (!t.isArray())
+        {
+          std::stringstream ss;
+          ss << "expected array constant term, but cast is not of array type"
+             << std::endl
+             << "cast type: " << t;
+          PARSER_STATE->parseError(ss.str());
+        }
+        kind = kind::STORE_ALL;
+      }
+    | identifier[k,baseName,f]
+      sortSymbol[type, CHECK_DECLARED]
+      {
+        if (f.isNull())
+        {
+          Trace("parser-overloading")
+              << "Getting variable expression with name " << baseName
+              << " and type " << type << std::endl;
+          // get the variable expression for the type
+          if (PARSER_STATE->isDeclared(baseName, SYM_VARIABLE))
+          {
+            f = PARSER_STATE->getExpressionForNameAndType(baseName, type);
+          }
+          if(f.isNull())
+          {
+            std::stringstream ss;
+            ss << "Could not resolve expression with name " << baseName
+               << " and type " << type << std::endl;
+            PARSER_STATE->parseError(ss.str());
+          }
+        }
+        Trace("parser-qid") << "Resolve ascription " << type << " on " << f;
+        Trace("parser-qid") << " " << f.getKind() << " " << f.getType();
+        Trace("parser-qid") << std::endl;
+        // by default, we take f itself
+        expr = f;
+        if (f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype())
+        {
+          // nullary constructors with a type ascription
+          // could be a parametric constructor or just an overloaded constructor
+          DatatypeType dtype = static_cast<DatatypeType>(type);
+          if (dtype.isParametric())
+          {
+            std::vector<CVC4::Expr> v;
+            Expr e = f.getOperator();
+            const DatatypeConstructor& dtc =
+                Datatype::datatypeOf(e)[Datatype::indexOf(e)];
+            v.push_back(MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION,
+                                MK_CONST(AscriptionType(
+                                    dtc.getSpecializedConstructorType(type))),
+                                f.getOperator()));
+            v.insert(v.end(), f.begin(), f.end());
+            expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
+          }
+        }
+        else if (f.getType().isConstructor())
+        {
+          // a non-nullary constructor with a type ascription
+          DatatypeType dtype = static_cast<DatatypeType>(type);
+          if (dtype.isParametric())
+          {
+            const DatatypeConstructor& dtc =
+                Datatype::datatypeOf(f)[Datatype::indexOf(f)];
+            expr = MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION,
+                           MK_CONST(AscriptionType(
+                               dtc.getSpecializedConstructorType(type))),
+                           f);
+          }
+        }
+        else if (f.getKind() == CVC4::kind::EMPTYSET)
+        {
+          Debug("parser") << "Empty set encountered: " << f << " " << type
+                          << std::endl;
+          expr = MK_CONST(::CVC4::EmptySet(type));
+        }
+        else if (f.getKind() == CVC4::kind::UNIVERSE_SET)
+        {
+          expr = EXPR_MANAGER->mkNullaryOperator(type, kind::UNIVERSE_SET);
+        }
+        else if (f.getKind() == CVC4::kind::SEP_NIL)
+        {
+          // We don't want the nil reference to be a constant: for instance, it
+          // could be of type Int but is not a const rational. However, the
+          // expression has 0 children. So we convert to a SEP_NIL variable.
+          expr = EXPR_MANAGER->mkNullaryOperator(type, kind::SEP_NIL);
+        }
+        else if (f.getType() != type)
+        {
+          PARSER_STATE->parseError("Type ascription not satisfied.");
+        }
+      }
+    )
+    RPAREN_TOK
+  ;
+
+/**
+ * Matches an identifier, which can be a combination of one or more of the
+ * following:
+ * (1) A kind.
+ * (2) A string name.
+ * (3) An expression expr.
+ * For examples, see documentation of qualIdentifier.
+ */
+identifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr]
+@init {
+  Expr f;
+  Expr f2;
+  std::vector<uint64_t> numerals;
+}
+: functionName[name, CHECK_NONE]
+
+  // indexed functions
+
+  | LPAREN_TOK INDEX_TOK
+    ( TESTER_TOK term[f, f2]
+      {
+        if (f.getKind() == kind::APPLY_CONSTRUCTOR && f.getNumChildren() == 0)
+        {
+          // for nullary constructors, must get the operator
+          f = f.getOperator();
+        }
+        if (!f.getType().isConstructor())
+        {
+          PARSER_STATE->parseError(
+              "Bad syntax for test (_ is X), X must be a constructor.");
+        }
+        expr = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getTester();
+      }
+    | TUPLE_SEL_TOK m=INTEGER_LITERAL
+      {
+        // we adopt a special syntax (_ tupSel n)
+        kind = CVC4::kind::APPLY_SELECTOR;
+        // put m in expr so that the caller can deal with this case
+        expr = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m)));
+      }
+    | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
+      {
+        expr = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals)
+                   .getExpr();
+      }
+    )
+    RPAREN_TOK
+  ;
+
+/**
  * Matches an atomic term (a term with no subterms).
  * @return the expression expr representing the term or formula.
  */
@@ -2633,41 +2875,6 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr]
   ;
 
 /**
- * Matches a bit-vector operator (the ones parametrized by numbers)
- */
-indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind]
-@init {
-  Expr expr;
-  Expr expr2;
-  std::vector<uint64_t> numerals;
-}
-  : LPAREN_TOK INDEX_TOK
-    ( TESTER_TOK term[expr, expr2] {
-        if( expr.getKind()==kind::APPLY_CONSTRUCTOR && expr.getNumChildren()==0 ){
-          //for nullary constructors, must get the operator
-          expr = expr.getOperator();
-        }
-        if( !expr.getType().isConstructor() ){
-          PARSER_STATE->parseError("Bad syntax for test (_ is X), X must be a constructor.");
-        }
-        op = Datatype::datatypeOf(expr)[Datatype::indexOf(expr)].getTester();
-        kind = CVC4::kind::APPLY_TESTER;
-      }
-    | TUPLE_SEL_TOK m=INTEGER_LITERAL {
-        kind = CVC4::kind::APPLY_SELECTOR;
-        //put m in op so that the caller (termNonVariable) can deal with this case
-        op = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m)));
-      }
-    | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
-      {
-        op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals)
-                 .getExpr();
-      }
-    )
-    RPAREN_TOK
-  ;
-
-/**
  * Matches a sequence of terms and puts them into the formulas
  * vector.
  * @param formulas the vector to fill with terms
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 752bf58b4..039f573f9 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -502,13 +502,7 @@ bool Smt2::logicIsSet() {
 }
 
 Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
-  if (sygus_v1() && name[0] == '-'
-      && name.find_first_not_of("0123456789", 1) == std::string::npos)
-  {
-    // allow unary minus in sygus version 1
-    return getExprManager()->mkConst(Rational(name));
-  }
-  else if (isAbstractValue(name))
+  if (isAbstractValue(name))
   {
     return mkAbstractValue(name);
   }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index df553b8bd..37e6e3414 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -505,6 +505,7 @@ set(regress_0_tests
   regress0/issue1063-overloading-dt-cons.smt2
   regress0/issue1063-overloading-dt-fun.smt2
   regress0/issue1063-overloading-dt-sel.smt2
+  regress0/issue2832-qualId.smt2
   regress0/ite.cvc
   regress0/ite2.smt2
   regress0/ite3.smt2
diff --git a/test/regress/regress0/issue2832-qualId.smt2 b/test/regress/regress0/issue2832-qualId.smt2
new file mode 100644
index 000000000..ff6e6e881
--- /dev/null
+++ b/test/regress/regress0/issue2832-qualId.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((D 2)) ((par (T1 T2)
+                                    ((CL  (get_CL  T1))
+                                     (CR (get_CR T2))))))
+(declare-sort U 0)
+(declare-fun s0 () U)
+(define-fun s1 () (D U U) ((as CL (D U U)) s0))
+(check-sat)