Remove sygus1 parser (#4651)

We no longer support sygus v1 inputs. This PR removes support for sygus v1 (as well as a deprecated "z3str" variant of smt lib 2 which is subsumed by the new strings standard).

As mentioned in the release notes, CVC4 1.8 supports a conversion from sygus v1 to v2 script.

This removal is required for further updates to the new API. Further infrastructure (e.g. the sygus print callback) will be removed in a separate PR.

FYI @abdoo8080 .

1 files changed, 4 insertions, 561 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a7eb218af..68b1945fc 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -568,16 +568,6 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     }
   }
 
-  if (sygus_v1())
-  {
-    // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2)
-    if(name == "Arrays") {
-      name = "A";
-    }else if(name == "Reals") {
-      name = "LRA";
-    }
-  }
-
   d_logicSet = true;
   d_logic = name;
 
@@ -752,13 +742,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
 bool Smt2::sygus() const
 {
   InputLanguage ilang = getLanguage();
-  return ilang == language::input::LANG_SYGUS_V1
-         || ilang == language::input::LANG_SYGUS_V2;
-}
-
-bool Smt2::sygus_v1() const
-{
-  return getLanguage() == language::input::LANG_SYGUS_V1;
+  return ilang == language::input::LANG_SYGUS_V2;
 }
 
 bool Smt2::sygus_v2() const
@@ -899,538 +883,6 @@ api::Term Smt2::mkAbstractValue(const std::string& name)
   return d_solver->mkAbstractValue(name.substr(1));
 }
 
-void Smt2::mkSygusConstantsForType(const api::Sort& type,
-                                   std::vector<api::Term>& ops)
-{
-  if( type.isInteger() ){
-    ops.push_back(d_solver->mkReal(0));
-    ops.push_back(d_solver->mkReal(1));
-  }else if( type.isBitVector() ){
-    uint32_t sz = type.getBVSize();
-    ops.push_back(d_solver->mkBitVector(sz, 0));
-    ops.push_back(d_solver->mkBitVector(sz, 1));
-  }else if( type.isBoolean() ){
-    ops.push_back(d_solver->mkTrue());
-    ops.push_back(d_solver->mkFalse());
-  }
-  //TODO : others?
-}
-
-//  This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
-//  This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
-void Smt2::processSygusGTerm(
-    CVC4::SygusGTerm& sgt,
-    int index,
-    std::vector<api::DatatypeDecl>& datatypes,
-    std::vector<api::Sort>& sorts,
-    std::vector<std::vector<ParseOp>>& ops,
-    std::vector<std::vector<std::string>>& cnames,
-    std::vector<std::vector<std::vector<api::Sort>>>& cargs,
-    std::vector<bool>& allow_const,
-    std::vector<std::vector<std::string>>& unresolved_gterm_sym,
-    const std::vector<api::Term>& sygus_vars,
-    std::map<api::Sort, api::Sort>& sygus_to_builtin,
-    std::map<api::Sort, api::Term>& sygus_to_builtin_expr,
-    api::Sort& ret,
-    bool isNested)
-{
-  if (sgt.d_gterm_type == SygusGTerm::gterm_op)
-  {
-    Debug("parser-sygus") << "Add " << sgt.d_op << " to datatype "
-                          << index << std::endl;
-    api::Kind oldKind;
-    api::Kind newKind = api::UNDEFINED_KIND;
-    //convert to UMINUS if one child of MINUS
-    if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == api::MINUS)
-    {
-      oldKind = api::MINUS;
-      newKind = api::UMINUS;
-    }
-    if (newKind != api::UNDEFINED_KIND)
-    {
-      Debug("parser-sygus")
-          << "Replace " << sgt.d_op.d_kind << " with " << newKind << std::endl;
-      sgt.d_op.d_kind = newKind;
-      std::string oldName = api::kindToString(oldKind);
-      std::string newName = api::kindToString(newKind);
-      size_t pos = 0;
-      if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){
-        sgt.d_name.replace(pos, oldName.length(), newName);
-      }
-    }
-    ops[index].push_back(sgt.d_op);
-    cnames[index].push_back( sgt.d_name );
-    cargs[index].push_back(std::vector<api::Sort>());
-    for( unsigned i=0; i<sgt.d_children.size(); i++ ){
-      std::stringstream ss;
-      ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
-      std::string sub_dname = ss.str();
-      //add datatype for child
-      api::Sort null_type;
-      pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
-      int sub_dt_index = datatypes.size()-1;
-      //process child
-      api::Sort sub_ret;
-      processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
-                         sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
-      //process the nested gterm (either pop the last datatype, or flatten the argument)
-      api::Sort tt = processSygusNestedGTerm(sub_dt_index,
-                                             sub_dname,
-                                             datatypes,
-                                             sorts,
-                                             ops,
-                                             cnames,
-                                             cargs,
-                                             allow_const,
-                                             unresolved_gterm_sym,
-                                             sygus_to_builtin,
-                                             sygus_to_builtin_expr,
-                                             sub_ret);
-      cargs[index].back().push_back(tt);
-    }
-  }
-  else if (sgt.d_gterm_type == SygusGTerm::gterm_constant)
-  {
-    if( sgt.getNumChildren()!=0 ){
-      parseError("Bad syntax for Sygus Constant.");
-    }
-    std::vector<api::Term> consts;
-    mkSygusConstantsForType( sgt.d_type, consts );
-    Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
-    for( unsigned i=0; i<consts.size(); i++ ){
-      std::stringstream ss;
-      ss << consts[i];
-      Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
-      ParseOp constOp;
-      constOp.d_expr = consts[i];
-      ops[index].push_back(constOp);
-      cnames[index].push_back( ss.str() );
-      cargs[index].push_back(std::vector<api::Sort>());
-    }
-    allow_const[index] = true;
-  }
-  else if (sgt.d_gterm_type == SygusGTerm::gterm_variable
-           || sgt.d_gterm_type == SygusGTerm::gterm_input_variable)
-  {
-    if( sgt.getNumChildren()!=0 ){
-      parseError("Bad syntax for Sygus Variable.");
-    }
-    Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
-    for( unsigned i=0; i<sygus_vars.size(); i++ ){
-      if (sygus_vars[i].getSort() == sgt.d_type)
-      {
-        std::stringstream ss;
-        ss << sygus_vars[i];
-        Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
-        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<api::Sort>());
-      }
-    }
-  }
-  else if (sgt.d_gterm_type == SygusGTerm::gterm_nested_sort)
-  {
-    ret = sgt.d_type;
-  }
-  else if (sgt.d_gterm_type == SygusGTerm::gterm_unresolved)
-  {
-    if( isNested ){
-      if( isUnresolvedType(sgt.d_name) ){
-        ret = getSort(sgt.d_name);
-      }else{
-        //nested, unresolved symbol...fail
-        std::stringstream ss;
-        ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl;
-        parseError(ss.str());
-      }
-    }else{
-      //will resolve when adding constructors
-      unresolved_gterm_sym[index].push_back(sgt.d_name);
-    }
-  }
-  else if (sgt.d_gterm_type == SygusGTerm::gterm_ignore)
-  {
-    // do nothing
-  }
-}
-
-bool Smt2::pushSygusDatatypeDef(
-    api::Sort t,
-    std::string& dname,
-    std::vector<api::DatatypeDecl>& datatypes,
-    std::vector<api::Sort>& sorts,
-    std::vector<std::vector<ParseOp>>& ops,
-    std::vector<std::vector<std::string>>& cnames,
-    std::vector<std::vector<std::vector<api::Sort>>>& cargs,
-    std::vector<bool>& allow_const,
-    std::vector<std::vector<std::string>>& unresolved_gterm_sym)
-{
-  sorts.push_back(t);
-  datatypes.push_back(d_solver->mkDatatypeDecl(dname));
-  ops.push_back(std::vector<ParseOp>());
-  cnames.push_back(std::vector<std::string>());
-  cargs.push_back(std::vector<std::vector<api::Sort>>());
-  allow_const.push_back(false);
-  unresolved_gterm_sym.push_back(std::vector< std::string >());
-  return true;
-}
-
-bool Smt2::popSygusDatatypeDef(
-    std::vector<api::DatatypeDecl>& datatypes,
-    std::vector<api::Sort>& sorts,
-    std::vector<std::vector<ParseOp>>& ops,
-    std::vector<std::vector<std::string>>& cnames,
-    std::vector<std::vector<std::vector<api::Sort>>>& cargs,
-    std::vector<bool>& allow_const,
-    std::vector<std::vector<std::string>>& unresolved_gterm_sym)
-{
-  sorts.pop_back();
-  datatypes.pop_back();
-  ops.pop_back();
-  cnames.pop_back();
-  cargs.pop_back();
-  allow_const.pop_back();
-  unresolved_gterm_sym.pop_back();
-  return true;
-}
-
-api::Sort Smt2::processSygusNestedGTerm(
-    int sub_dt_index,
-    std::string& sub_dname,
-    std::vector<api::DatatypeDecl>& datatypes,
-    std::vector<api::Sort>& sorts,
-    std::vector<std::vector<ParseOp>>& ops,
-    std::vector<std::vector<std::string>>& cnames,
-    std::vector<std::vector<std::vector<api::Sort>>>& cargs,
-    std::vector<bool>& allow_const,
-    std::vector<std::vector<std::string>>& unresolved_gterm_sym,
-    std::map<api::Sort, api::Sort>& sygus_to_builtin,
-    std::map<api::Sort, CVC4::api::Term>& sygus_to_builtin_expr,
-    api::Sort sub_ret)
-{
-  api::Sort t = sub_ret;
-  Debug("parser-sygus") << "Argument is ";
-  if( t.isNull() ){
-    //then, it is the datatype we constructed, which should have a single constructor
-    t = mkUnresolvedType(sub_dname);
-    Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t << std::endl;
-    Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs[sub_dt_index].size() << std::endl;
-    if( cargs[sub_dt_index].empty() ){
-      parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
-    }
-    ParseOp op = ops[sub_dt_index][0];
-    api::Sort curr_t;
-    if (!op.d_expr.isNull()
-        && (op.d_expr.isConst() || cargs[sub_dt_index][0].empty()))
-    {
-      api::Term sop = op.d_expr;
-      curr_t = sop.getSort();
-      Debug("parser-sygus")
-          << ": it is constant/0-arg cons " << sop << " with type "
-          << sop.getSort() << ", debug=" << sop.isConst() << " "
-          << cargs[sub_dt_index][0].size() << std::endl;
-      // only cache if it is a singleton datatype (has unique expr)
-      if (ops[sub_dt_index].size() == 1)
-      {
-        sygus_to_builtin_expr[t] = sop;
-        // 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<api::Term> children;
-      for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
-        std::map<api::Sort, CVC4::api::Term>::iterator it =
-            sygus_to_builtin_expr.find(cargs[sub_dt_index][0][i]);
-        if( it==sygus_to_builtin_expr.end() ){
-          if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){
-            std::stringstream ss;
-            ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl;
-            ss << "Builtin types are currently : " << std::endl;
-            for (std::map<api::Sort, api::Sort>::iterator itb =
-                     sygus_to_builtin.begin();
-                 itb != sygus_to_builtin.end();
-                 ++itb)
-            {
-              ss << "  " << itb->first << " -> " << itb->second << std::endl;
-            }
-            parseError(ss.str());
-          }
-          api::Sort bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
-          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;
-          api::Term bv = bindBoundVar(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 );
-        }
-      }
-      api::Term e = applyParseOp(op, children);
-      Debug("parser-sygus") << ": constructed " << e << ", which has type "
-                            << e.getSort() << std::endl;
-      curr_t = e.getSort();
-      sygus_to_builtin_expr[t] = e;
-    }
-    sorts[sub_dt_index] = curr_t;
-    sygus_to_builtin[t] = curr_t;
-  }else{
-    Debug("parser-sygus") << "simple argument " << t << std::endl;
-    Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl;
-    //otherwise, datatype was unecessary
-    //pop argument datatype definition
-    popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
-  }
-  return t;
-}
-
-void Smt2::setSygusStartIndex(const std::string& fun,
-                              int startIndex,
-                              std::vector<api::DatatypeDecl>& datatypes,
-                              std::vector<api::Sort>& sorts,
-                              std::vector<std::vector<ParseOp>>& ops)
-{
-  if( startIndex>0 ){
-    api::DatatypeDecl tmp_dt = datatypes[0];
-    api::Sort tmp_sort = sorts[0];
-    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];
-    ops[0].clear();
-    ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
-    datatypes[startIndex] = tmp_dt;
-    sorts[startIndex] = tmp_sort;
-    ops[startIndex].clear();
-    ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
-  }else if( startIndex<0 ){
-    std::stringstream ss;
-    ss << "warning: no symbol named Start for synth-fun " << fun << std::endl;
-    warning(ss.str());
-  }
-}
-
-void Smt2::mkSygusDatatype(api::DatatypeDecl& dt,
-                           std::vector<ParseOp>& ops,
-                           std::vector<std::string>& cnames,
-                           std::vector<std::vector<api::Sort>>& cargs,
-                           std::vector<std::string>& unresolved_gterm_sym,
-                           std::map<api::Sort, api::Sort>& sygus_to_builtin)
-{
-  Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
-  Debug("parser-sygus") << "  add constructors..." << std::endl;
-  
-  Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl;
-  Debug("parser-sygus") << "  add constructors..." << std::endl;
-  // size of cnames changes, this loop must check size
-  for (unsigned i = 0; i < cnames.size(); i++)
-  {
-    bool is_dup = false;
-    bool is_dup_op = false;
-    for (unsigned j = 0; j < i; j++)
-    {
-      if( ops[i]==ops[j] ){
-        is_dup_op = true;
-        if( cargs[i].size()==cargs[j].size() ){
-          is_dup = true;
-          for( unsigned k=0; k<cargs[i].size(); k++ ){
-            if( cargs[i][k]!=cargs[j][k] ){
-              is_dup = false;
-              break;
-            }
-          }
-        }
-        if( is_dup ){
-          break;
-        }
-      }
-    }
-    Debug("parser-sygus") << "SYGUS CONS " << i << " : ";
-    if( is_dup ){
-      Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl;
-      ops.erase( ops.begin() + i, ops.begin() + i + 1 );
-      cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 );
-      cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 );
-      i--;
-    }
-    else
-    {
-      std::shared_ptr<SygusPrintCallback> spc;
-      if (is_dup_op)
-      {
-        Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i]
-                              << std::endl;
-        // make into define-fun
-        std::vector<api::Sort> ltypes;
-        for (unsigned j = 0, size = cargs[i].size(); j < size; j++)
-        {
-          ltypes.push_back(sygus_to_builtin[cargs[i][j]]);
-        }
-        std::vector<api::Term> largs;
-        api::Term lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
-
-        // make the let_body
-        std::vector<api::Term> largsApply = largs;
-        api::Term body = applyParseOp(ops[i], largsApply);
-        // replace by lambda
-        ParseOp pLam;
-        pLam.d_expr = d_solver->mkTerm(api::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.getExpr(), api::termVectorToExprs(largs));
-      }
-      else
-      {
-        api::Term sop = ops[i].d_expr;
-        if (!sop.isNull() && sop.getSort().isBitVector() && sop.isConst())
-        {
-          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
-          // format given by the user, we use a print callback to custom print
-          // the given name.
-          spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
-        }
-        else if (!sop.isNull() && sop.getKind() == api::CONSTANT)
-        {
-          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 (sop.getSort().isFunction())
-          {
-            std::vector<api::Sort> ftypes =
-                sop.getSort().getFunctionDomainSorts();
-            std::vector<api::Term> largs;
-            api::Term lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
-            largs.insert(largs.begin(), sop);
-            api::Term body = d_solver->mkTerm(api::APPLY_UF, largs);
-            ops[i].d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body);
-            Debug("parser-sygus") << "  ...replace op : " << ops[i]
-                                  << std::endl;
-          }
-          else
-          {
-            Debug("parser-sygus") << "  ...replace op : " << ops[i]
-                                  << std::endl;
-          }
-          // keep a callback to say it should be printed with the defined name
-          spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
-        }
-        else
-        {
-          Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl;
-        }
-      }
-      // must rename to avoid duplication
-      std::stringstream ss;
-      ss << dt.getName() << "_" << i << "_" << cnames[i];
-      cnames[i] = ss.str();
-      Debug("parser-sygus") << "  construct the datatype " << cnames[i] << "..."
-                            << std::endl;
-
-      // Add the sygus constructor, either using the expression operator of
-      // ops[i], or the kind.
-      if (!ops[i].d_expr.isNull())
-      {
-        dt.getDatatype().addSygusConstructor(ops[i].d_expr.getExpr(),
-                                             cnames[i],
-                                             api::sortVectorToTypes(cargs[i]),
-                                             spc);
-      }
-      else if (ops[i].d_kind != api::NULL_EXPR)
-      {
-        dt.getDatatype().addSygusConstructor(extToIntKind(ops[i].d_kind),
-                                             cnames[i],
-                                             api::sortVectorToTypes(cargs[i]),
-                                             spc);
-      }
-      else
-      {
-        std::stringstream ess;
-        ess << "unexpected parse operator for sygus constructor" << ops[i];
-        parseError(ess.str());
-      }
-      Debug("parser-sygus") << "  finished constructing the datatype"
-                            << std::endl;
-    }
-  }
-
-  Debug("parser-sygus") << "  add constructors for unresolved symbols..." << std::endl;
-  if( !unresolved_gterm_sym.empty() ){
-    std::vector<api::Sort> types;
-    Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl;
-    for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){
-      Debug("parser-sygus") << "  resolve : " << unresolved_gterm_sym[i] << std::endl;
-      if( isUnresolvedType(unresolved_gterm_sym[i]) ){
-        Debug("parser-sygus") << "    it is an unresolved type." << std::endl;
-        api::Sort t = getSort(unresolved_gterm_sym[i]);
-        if( std::find( types.begin(), types.end(), t )==types.end() ){
-          types.push_back( t );
-          //identity element
-          api::Sort bt = api::Sort(d_solver, dt.getDatatype().getSygusType());
-          Debug("parser-sygus") << ":  make identity function for " << bt << ", argument type " << t << std::endl;
-
-          std::stringstream ss;
-          ss << t << "_x";
-          api::Term var = bindBoundVar(ss.str(), bt);
-          std::vector<api::Term> lchildren;
-          lchildren.push_back(d_solver->mkTerm(api::BOUND_VAR_LIST, var));
-          lchildren.push_back(var);
-          api::Term id_op = d_solver->mkTerm(api::LAMBDA, lchildren);
-
-          // empty sygus callback (should not be printed)
-          std::shared_ptr<SygusPrintCallback> sepc =
-              std::make_shared<printer::SygusEmptyPrintCallback>();
-
-          //make the sygus argument list
-          std::vector<api::Sort> id_carg;
-          id_carg.push_back( t );
-          dt.getDatatype().addSygusConstructor(id_op.getExpr(),
-                                               unresolved_gterm_sym[i],
-                                               api::sortVectorToTypes(id_carg),
-                                               sepc);
-
-          //add to operators
-          ParseOp idOp;
-          idOp.d_expr = id_op;
-          ops.push_back(idOp);
-        }
-      }else{
-        std::stringstream ss;
-        ss << "Unhandled sygus constructor " << unresolved_gterm_sym[i];
-        throw ParserException(ss.str());
-      }
-    }
-  }
-}
-
-api::Term Smt2::makeSygusBoundVarList(api::DatatypeDecl& dt,
-                                      unsigned i,
-                                      const std::vector<api::Sort>& ltypes,
-                                      std::vector<api::Term>& lvars)
-{
-  for (unsigned j = 0, size = ltypes.size(); j < size; j++)
-  {
-    std::stringstream ss;
-    ss << dt.getName() << "_x_" << i << "_" << j;
-    api::Term v = bindBoundVar(ss.str(), ltypes[j]);
-    lvars.push_back(v);
-  }
-  return d_solver->mkTerm(api::BOUND_VAR_LIST, lvars);
-}
 
 void Smt2::addSygusConstructorTerm(
     api::DatatypeDecl& dt,
@@ -1592,18 +1044,9 @@ api::Term Smt2::parseOpToExpr(ParseOp& p)
   }
   else if (!isDeclared(p.d_name, SYM_VARIABLE))
   {
-    if (sygus_v1() && p.d_name[0] == '-'
-        && p.d_name.find_first_not_of("0123456789", 1) == std::string::npos)
-    {
-      // allow unary minus in sygus version 1
-      expr = d_solver->mkReal(p.d_name);
-    }
-    else
-    {
-      std::stringstream ss;
-      ss << "Symbol " << p.d_name << " is not declared.";
-      parseError(ss.str());
-    }
+    std::stringstream ss;
+    ss << "Symbol " << p.d_name << " is not declared.";
+    parseError(ss.str());
   }
   else
   {