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 .

18 files changed, 22 insertions, 1206 deletions

diff --git a/src/options/language.cpp b/src/options/language.cpp
index c03ae1cbb..b00d5c102 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -29,15 +29,12 @@ Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6;
 
 bool isInputLang_smt2(InputLanguage lang)
 {
-  return (lang >= input::LANG_SMTLIB_V2_0 && lang <= input::LANG_SMTLIB_V2_END)
-         || lang == input::LANG_Z3STR;
+  return lang >= input::LANG_SMTLIB_V2_0 && lang <= input::LANG_SMTLIB_V2_END;
 }
 
 bool isOutputLang_smt2(OutputLanguage lang)
 {
-  return (lang >= output::LANG_SMTLIB_V2_0
-          && lang <= output::LANG_SMTLIB_V2_END)
-         || lang == output::LANG_Z3STR;
+  return lang >= output::LANG_SMTLIB_V2_0 && lang <= output::LANG_SMTLIB_V2_END;
 }
 
 bool isInputLang_smt2_5(InputLanguage lang, bool exact)
@@ -70,12 +67,12 @@ bool isOutputLang_smt2_6(OutputLanguage lang, bool exact)
 
 bool isInputLangSygus(InputLanguage lang)
 {
-  return lang == input::LANG_SYGUS_V1 || lang == input::LANG_SYGUS_V2;
+  return lang == input::LANG_SYGUS_V2;
 }
 
 bool isOutputLangSygus(OutputLanguage lang)
 {
-  return lang == output::LANG_SYGUS_V1 || lang == output::LANG_SYGUS_V2;
+  return lang == output::LANG_SYGUS_V2;
 }
 
 InputLanguage toInputLanguage(OutputLanguage language) {
@@ -85,8 +82,6 @@ InputLanguage toInputLanguage(OutputLanguage language) {
   case output::LANG_SMTLIB_V2_6:
   case output::LANG_TPTP:
   case output::LANG_CVC4:
-  case output::LANG_Z3STR:
-  case output::LANG_SYGUS_V1:
   case output::LANG_SYGUS_V2:
     // these entries directly correspond (by design)
     return InputLanguage(int(language));
@@ -107,8 +102,6 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   case input::LANG_SMTLIB_V2_6:
   case input::LANG_TPTP:
   case input::LANG_CVC4:
-  case input::LANG_Z3STR:
-  case input::LANG_SYGUS_V1:
   case input::LANG_SYGUS_V2:
     // these entries directly correspond (by design)
     return OutputLanguage(int(language));
@@ -152,13 +145,6 @@ OutputLanguage toOutputLanguage(std::string language) {
     return output::LANG_SMTLIB_V2_6;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return output::LANG_TPTP;
-  } else if(language == "z3str" || language == "z3-str" ||
-            language == "LANG_Z3STR") {
-    return output::LANG_Z3STR;
-  }
-  else if (language == "sygus1" || language == "LANG_SYGUS_V1")
-  {
-    return output::LANG_SYGUS_V1;
   }
   else if (language == "sygus" || language == "LANG_SYGUS"
            || language == "sygus2" || language == "LANG_SYGUS_V2")
@@ -195,13 +181,6 @@ InputLanguage toInputLanguage(std::string language) {
     return input::LANG_SMTLIB_V2_6;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return input::LANG_TPTP;
-  } else if(language == "z3str" || language == "z3-str" ||
-            language == "LANG_Z3STR") {
-    return input::LANG_Z3STR;
-  }
-  else if (language == "sygus1" || language == "LANG_SYGUS_V1")
-  {
-    return input::LANG_SYGUS_V1;
   }
   else if (language == "sygus2" || language == "LANG_SYGUS_V2")
   {
diff --git a/src/options/language.h b/src/options/language.h
index 7dc1cf987..0a0f63ca6 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -56,10 +56,6 @@ enum CVC4_PUBLIC Language
   LANG_TPTP,
   /** The CVC4 input language */
   LANG_CVC4,
-  /** The Z3-str input language */
-  LANG_Z3STR,
-  /** The SyGuS input language version 1.0 */
-  LANG_SYGUS_V1,
   /** The SyGuS input language version 2.0 */
   LANG_SYGUS_V2,
 
@@ -91,10 +87,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_CVC4:
     out << "LANG_CVC4";
     break;
-  case LANG_Z3STR:
-    out << "LANG_Z3STR";
-    break;
-  case LANG_SYGUS_V1: out << "LANG_SYGUS_V1"; break;
   case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
   default:
     out << "undefined_input_language";
@@ -132,10 +124,6 @@ enum CVC4_PUBLIC Language
   LANG_TPTP = input::LANG_TPTP,
   /** The CVC4 output language */
   LANG_CVC4 = input::LANG_CVC4,
-  /** The Z3-str output language */
-  LANG_Z3STR = input::LANG_Z3STR,
-  /** The sygus output language version 1.0 */
-  LANG_SYGUS_V1 = input::LANG_SYGUS_V1,
   /** The sygus output language version 2.0 */
   LANG_SYGUS_V2 = input::LANG_SYGUS_V2,
 
@@ -167,10 +155,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_CVC4:
     out << "LANG_CVC4";
     break;
-  case LANG_Z3STR:
-    out << "LANG_Z3STR";
-    break;
-  case LANG_SYGUS_V1: out << "LANG_SYGUS_V1"; break;
   case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
   case LANG_AST:
     out << "LANG_AST";
diff --git a/src/options/language.i b/src/options/language.i
index 639cb0bda..7f81ea7c6 100644
--- a/src/options/language.i
+++ b/src/options/language.i
@@ -26,8 +26,6 @@ namespace CVC4 {
 %rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP;
 %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4;
 %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX;
-%rename(INPUT_LANG_Z3STR) CVC4::language::input::LANG_Z3STR;
-%rename(INPUT_LANG_SYGUS_V1) CVC4::language::input::LANG_SYGUS_V1;
 %rename(INPUT_LANG_SYGUS_V2) CVC4::language::input::LANG_SYGUS_V2;
 
 %rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO;
@@ -39,8 +37,6 @@ namespace CVC4 {
 %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4;
 %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST;
 %rename(OUTPUT_LANG_MAX) CVC4::language::output::LANG_MAX;
-%rename(OUTPUT_LANG_Z3STR) CVC4::language::output::LANG_Z3STR;
-%rename(OUTPUT_LANG_SYGUS_V1) CVC4::language::output::LANG_SYGUS_V1;
 %rename(OUTPUT_LANG_SYGUS_V2) CVC4::language::output::LANG_SYGUS_V2;
 
 %include "options/language.h"
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index a49ede98e..234ddd5b4 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -418,7 +418,6 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format (cnf, fof and tff)\n\
-  sygus1                         SyGuS version 1.0 \n\
   sygus | sygus2                 SyGuS version 2.0\n\
 \n\
 Languages currently supported as arguments to the --output-lang option:\n\
@@ -430,7 +429,6 @@ Languages currently supported as arguments to the --output-lang option:\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format\n\
-  z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
   ast                            internal format (simple syntax trees)\n\
 ";
 
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 273b9fd93..1d5190e3f 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -247,7 +247,6 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     break;
   }
 
-  case LANG_SYGUS_V1:
   case LANG_SYGUS_V2: input = new SygusInput(inputStream); break;
 
   case LANG_TPTP:
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 729d3b9a3..f65618267 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -89,7 +89,6 @@ Parser* ParserBuilder::build()
   Parser* parser = NULL;
   switch (d_lang)
   {
-    case language::input::LANG_SYGUS_V1:
     case language::input::LANG_SYGUS_V2:
       parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly);
       break;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a11b9670b..3e8234a86 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -305,14 +305,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
         PARSER_STATE->checkLogicAllowsFunctions();
       }
       // we allow overloading for function declarations
-      if (PARSER_STATE->sygus_v1())
-      {
-        // it is a higher-order universal variable
-        api::Term func = PARSER_STATE->bindBoundVar(name, t);
-        cmd->reset(
-            new DeclareSygusFunctionCommand(name, func.getExpr(), t.getType()));
-      }
-      else if( PARSER_STATE->sygus() )
+      if( PARSER_STATE->sygus() )
       {
         PARSER_STATE->parseErrorLogic("declare-fun are not allowed in sygus "
                                       "version 2.0");
@@ -567,40 +560,8 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
       api::Term var = PARSER_STATE->bindBoundVar(name, t);
       cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType()));
     }
-  | /* declare-primed-var */
-    DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
-    { PARSER_STATE->checkUserSymbol(name); }
-    sortSymbol[t,CHECK_DECLARED]
-    {
-      // spurious command, we do not need to create a variable. We only keep
-      // track of the command for sanity checking / dumping
-      cmd.reset(new DeclareSygusPrimedVarCommand(name, t.getType()));
-    }
 
   | /* synth-fun */
-    ( SYNTH_FUN_V1_TOK { isInv = false; }
-      | SYNTH_INV_V1_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
-    )
-    { PARSER_STATE->checkThatLogicIsSet(); }
-    symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
-    LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
-    ( sortSymbol[range,CHECK_DECLARED] )?
-    {
-      synthFunFactory.reset(new Smt2::SynthFunFactory(
-          PARSER_STATE, fun, isInv, range, sortedVarNames));
-    }
-    (
-      // optionally, read the sygus grammar
-      //
-      // `grammar` specifies the required grammar for the function to
-      // synthesize, expressed as a type
-      sygusGrammarV1[grammar, synthFunFactory->getSygusVars(), fun]
-    )?
-    {
-      cmd = synthFunFactory->mkCommand(grammar);
-    }
-  | /* synth-fun */
     ( SYNTH_FUN_TOK { isInv = false; }
       | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
     )
@@ -647,292 +608,6 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
   | command[&cmd]
   ;
 
-/** Reads a sygus grammar
- *
- * The resulting sygus datatype encoding the grammar is stored in ret.
- * The argument sygus_vars indicates the sygus bound variable list, which is
- * the argument list of the function-to-synthesize (or null if the grammar
- * has bound variables).
- * The argument fun is a unique identifier to avoid naming clashes for the
- * datatypes constructed by this call.
- */
-sygusGrammarV1[CVC4::api::Sort & ret,
-               const std::vector<CVC4::api::Term>& sygus_vars,
-               const std::string& fun]
-@declarations
-{
-  CVC4::api::Sort t;
-  std::string name;
-  unsigned startIndex = 0;
-  std::vector<std::vector<CVC4::SygusGTerm>> sgts;
-  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<CVC4::api::Sort>>> cargs;
-  std::vector<bool> allow_const;
-  std::vector<std::vector<std::string>> unresolved_gterm_sym;
-  std::map<CVC4::api::Sort, CVC4::api::Sort> sygus_to_builtin;
-  std::map<CVC4::api::Sort, CVC4::api::Term> sygus_to_builtin_expr;
-}
-  : LPAREN_TOK { PARSER_STATE->pushScope(); }
-  (LPAREN_TOK
-       symbol[name, CHECK_NONE, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED] {
-         if (name == "Start")
-         {
-           startIndex = datatypes.size();
-         }
-         sgts.push_back(std::vector<CVC4::SygusGTerm>());
-         sgts.back().push_back(CVC4::SygusGTerm());
-         PARSER_STATE->pushSygusDatatypeDef(t,
-                                            name,
-                                            datatypes,
-                                            sorts,
-                                            ops,
-                                            cnames,
-                                            cargs,
-                                            allow_const,
-                                            unresolved_gterm_sym);
-         api::Sort unres_t;
-         if (!PARSER_STATE->isUnresolvedType(name))
-         {
-           // if not unresolved, must be undeclared
-           Debug("parser-sygus") << "Make unresolved type : " << name
-                                 << std::endl;
-           PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
-           unres_t = PARSER_STATE->mkUnresolvedType(name);
-         }
-         else
-         {
-           Debug("parser-sygus") << "Get sort : " << name << std::endl;
-           unres_t = PARSER_STATE->getSort(name);
-         }
-         sygus_to_builtin[unres_t] = t;
-         Debug("parser-sygus") << "--- Read sygus grammar " << name
-                               << " under function " << fun << "..."
-                               << std::endl
-                               << "    type to resolve " << unres_t << std::endl
-                               << "    builtin type " << t << std::endl;
-       }
-   // Note the official spec for NTDef is missing the ( parens )
-   // but they are necessary to parse SyGuS examples
-   LPAREN_TOK(sygusGTerm[sgts.back().back(), fun] {
-     sgts.back().push_back(CVC4::SygusGTerm());
-   })
-   + RPAREN_TOK { sgts.back().pop_back(); } RPAREN_TOK)
-      + RPAREN_TOK
-  {
-    unsigned numSTerms = sgts.size();
-    Debug("parser-sygus") << "--- Process " << numSTerms << " sygus gterms..."
-                          << std::endl;
-    for (unsigned i = 0; i < numSTerms; i++)
-    {
-      for (unsigned j = 0, size = sgts[i].size(); j < size; j++)
-      {
-        api::Sort sub_ret;
-        PARSER_STATE->processSygusGTerm(sgts[i][j],
-                                        i,
-                                        datatypes,
-                                        sorts,
-                                        ops,
-                                        cnames,
-                                        cargs,
-                                        allow_const,
-                                        unresolved_gterm_sym,
-                                        sygus_vars,
-                                        sygus_to_builtin,
-                                        sygus_to_builtin_expr,
-                                        sub_ret);
-      }
-    }
-    // swap index if necessary
-    Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl;
-    unsigned ndatatypes = datatypes.size();
-    for (unsigned i = 0; i < ndatatypes; i++)
-    {
-      Debug("parser-sygus") << "..." << datatypes[i].getName()
-                            << " has builtin sort " << sorts[i] << std::endl;
-    }
-    api::Term bvl;
-    if (!sygus_vars.empty())
-    {
-      bvl = MK_TERM(api::BOUND_VAR_LIST, sygus_vars);
-    }
-    for (unsigned i = 0; i < ndatatypes; i++)
-    {
-      Debug("parser-sygus") << "...make " << datatypes[i].getName()
-                            << " with builtin sort " << sorts[i] << std::endl;
-      if (sorts[i].isNull())
-      {
-        PARSER_STATE->parseError(
-            "Internal error : could not infer "
-            "builtin sort for nested gterm.");
-      }
-      datatypes[i].getDatatype().setSygus(
-          sorts[i].getType(), bvl.getExpr(), allow_const[i], false);
-      PARSER_STATE->mkSygusDatatype(datatypes[i],
-                                    ops[i],
-                                    cnames[i],
-                                    cargs[i],
-                                    unresolved_gterm_sym[i],
-                                    sygus_to_builtin);
-    }
-    PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, ops);
-    PARSER_STATE->popScope();
-    Debug("parser-sygus") << "--- Make " << ndatatypes
-                          << " mutual datatypes..." << std::endl;
-    for (unsigned i = 0; i < ndatatypes; i++)
-    {
-      Debug("parser-sygus") << "  " << i << " : " << datatypes[i].getName()
-                            << std::endl;
-    }
-
-    std::vector<CVC4::Datatype> dtypes;
-    dtypes.reserve(ndatatypes);
-
-    for (api::DatatypeDecl i : datatypes)
-    {
-      dtypes.push_back(i.getDatatype());
-    }
-
-    std::set<Type> tset =
-        api::sortSetToTypes(PARSER_STATE->getUnresolvedSorts());
-
-    std::vector<DatatypeType> datatypeTypes =
-        SOLVER->getExprManager()->mkMutualDatatypeTypes(
-            dtypes, tset, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
-
-    PARSER_STATE->getUnresolvedSorts().clear();
-
-    ret = api::Sort(SOLVER, datatypeTypes[0]);
-  };
-
-// SyGuS grammar term.
-//
-// fun is the name of the synth-fun this grammar term is for.
-// 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.
-sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
-@declarations {
-  std::string name, name2;
-  CVC4::api::Kind k;
-  CVC4::api::Sort t;
-  std::string sname;
-  std::vector< CVC4::api::Term > let_vars;
-  std::string s;
-  CVC4::api::Term atomTerm;
-}
-  : LPAREN_TOK
-    //read operator
-    ( SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED]
-      { sgt.d_gterm_type = SygusGTerm::gterm_constant;
-        sgt.d_type = t;
-        Debug("parser-sygus") << "Sygus grammar constant." << std::endl;
-      }
-    | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
-      { sgt.d_gterm_type = SygusGTerm::gterm_variable;
-        sgt.d_type = t;
-        Debug("parser-sygus") << "Sygus grammar variable." << std::endl;
-      }
-    | SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
-      { sgt.d_gterm_type = SygusGTerm::gterm_local_variable;
-        sgt.d_type = t;
-        Debug("parser-sygus") << "Sygus grammar local variable...ignore."
-                              << std::endl;
-      }
-    | SYGUS_INPUT_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
-      { sgt.d_gterm_type = SygusGTerm::gterm_input_variable;
-        sgt.d_type = t;
-        Debug("parser-sygus") << "Sygus grammar (input) variable."
-                              << std::endl;
-      }
-    | symbol[name,CHECK_NONE,SYM_VARIABLE] {
-        bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
-        if(isBuiltinOperator) {
-          Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : "
-                                << name << std::endl;
-          k = PARSER_STATE->getOperatorKind(name);
-          sgt.d_name = api::kindToString(k);
-          sgt.d_gterm_type = SygusGTerm::gterm_op;
-          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
-          // fail, but we need an operator to continue here..
-          Debug("parser-sygus")
-              << "Sygus grammar " << fun << " : op (declare="
-              << PARSER_STATE->isDeclared(name) << ") : " << name
-              << std::endl;
-          if (!PARSER_STATE->isDeclared(name))
-          {
-            PARSER_STATE->parseError("Functions in sygus grammars must be "
-                                     "defined.");
-          }
-          sgt.d_name = name;
-          sgt.d_gterm_type = SygusGTerm::gterm_op;
-          sgt.d_op.d_expr = PARSER_STATE->getVariable(name) ;
-        }
-      }
-    )
-    //read arguments
-    { Debug("parser-sygus") << "Read arguments under " << sgt.d_name
-                            << std::endl;
-      sgt.addChild();
-    }
-    ( sygusGTerm[sgt.d_children.back(), fun]
-      { Debug("parser-sygus") << "Finished read argument #"
-                              << sgt.d_children.size() << "..." << std::endl;
-        sgt.addChild();
-      }
-    )*
-    RPAREN_TOK {
-      //pop last child index
-      sgt.d_children.pop_back();
-    }
-    | termAtomic[atomTerm]
-      {
-        Debug("parser-sygus") << "Sygus grammar " << fun << " : atomic "
-                              << "expression " << atomTerm << std::endl;
-        std::stringstream ss;
-        ss << atomTerm;
-        sgt.d_op.d_expr = atomTerm;
-        sgt.d_name = ss.str();
-        sgt.d_gterm_type = SygusGTerm::gterm_op;
-      }
-  | symbol[name,CHECK_NONE,SYM_VARIABLE]
-    {
-      if( name[0] == '-' ){  //hack for unary minus
-        Debug("parser-sygus") << "Sygus grammar " << fun
-                              << " : unary minus integer literal " << name
-                              << std::endl;
-        sgt.d_op.d_expr = SOLVER->mkReal(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_op.d_expr = PARSER_STATE->getExpressionForName(name);
-        sgt.d_name = name;
-        sgt.d_gterm_type = SygusGTerm::gterm_op;
-      }else{
-        if( PARSER_STATE->isDeclared(name, SYM_SORT) ){
-          Debug("parser-sygus") << "Sygus grammar " << fun
-                                << " : nested sort " << name << std::endl;
-          sgt.d_type = PARSER_STATE->getSort(name);
-          sgt.d_gterm_type = SygusGTerm::gterm_nested_sort;
-        }else{
-          Debug("parser-sygus") << "Sygus grammar " << fun
-                                << " : unresolved symbol " << name
-                                << std::endl;
-          sgt.d_gterm_type = SygusGTerm::gterm_unresolved;
-          sgt.d_name = name;
-        }
-      }
-    }
-  ;
-
 
 /** Reads a sygus grammar in the sygus version 2 format
  *
@@ -1780,7 +1455,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
       expr = PARSER_STATE->applyParseOp(p, args);
     }
   | /* a let or sygus let binding */
-    LPAREN_TOK (
+    LPAREN_TOK 
       LET_TOK LPAREN_TOK
       { PARSER_STATE->pushScope(true); }
       ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
@@ -1796,24 +1471,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
           } else {
             names.insert(name);
           }
-          binders.push_back(std::make_pair(name, expr)); } )+ |
-      SYGUS_LET_TOK LPAREN_TOK
-      { PARSER_STATE->pushScope(true); }
-      ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
-        sortSymbol[type,CHECK_DECLARED]
-        term[expr, f2]
-        RPAREN_TOK
-        // this is a parallel let, so we have to save up all the contributions
-        // of the let and define them only later on
-        { if(names.count(name) == 1) {
-            std::stringstream ss;
-            ss << "warning: symbol `" << name << "' bound multiple times by let;"
-               << " the last binding will be used, shadowing earlier ones";
-            PARSER_STATE->warning(ss.str());
-          } else {
-            names.insert(name);
-          }
-          binders.push_back(std::make_pair(name, expr)); } )+ )
+          binders.push_back(std::make_pair(name, expr)); } )+
     { // now implement these bindings
       for (const std::pair<std::string, api::Term>& binder : binders)
       {
@@ -2398,8 +2056,9 @@ sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check]
   | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;})
     symbol[name,CHECK_NONE,SYM_SORT]
     ( nonemptyNumeralList[numerals]
-      { // allow sygus inputs to elide the `_'
-        if( !indexed && !PARSER_STATE->sygus_v1() ) {
+      { 
+        if (!indexed) 
+        {
           std::stringstream ss;
           ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name
              << " ...)";
@@ -2615,8 +2274,7 @@ GET_UNSAT_CORE_TOK : 'get-unsat-core';
 EXIT_TOK : 'exit';
 RESET_TOK : { PARSER_STATE->v2_5() }? 'reset';
 RESET_ASSERTIONS_TOK : 'reset-assertions';
-LET_TOK : { !PARSER_STATE->sygus_v1() }? 'let';
-SYGUS_LET_TOK : { PARSER_STATE->sygus_v1() }? 'let';
+LET_TOK : 'let';
 ATTRIBUTE_TOK : '!';
 LPAREN_TOK : '(';
 RPAREN_TOK : ')';
@@ -2660,20 +2318,15 @@ GET_ABDUCT_TOK : 'get-abduct';
 DECLARE_HEAP : 'declare-heap';
 
 // SyGuS commands
-SYNTH_FUN_V1_TOK : { PARSER_STATE->sygus_v1() }?'synth-fun';
-SYNTH_FUN_TOK : { PARSER_STATE->sygus() && !PARSER_STATE->sygus_v1() }?'synth-fun';
-SYNTH_INV_V1_TOK : { PARSER_STATE->sygus_v1()}?'synth-inv';
-SYNTH_INV_TOK : { PARSER_STATE->sygus() && !PARSER_STATE->sygus_v1()}?'synth-inv';
+SYNTH_FUN_TOK : { PARSER_STATE->sygus() }?'synth-fun';
+SYNTH_INV_TOK : { PARSER_STATE->sygus()}?'synth-inv';
 CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth';
 DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var';
-DECLARE_PRIMED_VAR_TOK : { PARSER_STATE->sygus_v1() }?'declare-primed-var';
 CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint';
 INV_CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'inv-constraint';
 SET_OPTIONS_TOK : { PARSER_STATE->sygus() }? 'set-options';
 SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
 SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable';
-SYGUS_INPUT_VARIABLE_TOK : { PARSER_STATE->sygus_v1() }? 'InputVariable';
-SYGUS_LOCAL_VARIABLE_TOK : { PARSER_STATE->sygus_v1() }? 'LocalVariable';
 
 // attributes
 ATTRIBUTE_PATTERN_TOK : ':pattern';
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
   {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 868177d27..579fa90ce 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -60,9 +60,6 @@ class Smt2 : public Parser
    */
   std::unordered_map<std::string, api::Kind> d_indexedOpKindMap;
   std::pair<api::Term, std::string> d_lastNamedTerm;
-  // for sygus
-  std::vector<api::Term> d_sygusVars, d_sygusVarPrimed, d_sygusConstraints,
-      d_sygusFunSymbols;
 
  protected:
   Smt2(api::Solver* solver,
@@ -282,8 +279,6 @@ class Smt2 : public Parser
   }
   /** Are we using a sygus language? */
   bool sygus() const;
-  /** Are we using the sygus version 1.0 format? */
-  bool sygus_v1() const;
   /** Are we using the sygus version 2.0 format? */
   bool sygus_v2() const;
 
@@ -350,58 +345,6 @@ class Smt2 : public Parser
    */
   api::Term mkAbstractValue(const std::string& name);
 
-  void mkSygusConstantsForType(const api::Sort& type,
-                               std::vector<api::Term>& ops);
-
-  void 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 = false);
-
-  bool 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);
-
-  bool 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);
-
-  void setSygusStartIndex(const std::string& fun,
-                          int startIndex,
-                          std::vector<api::DatatypeDecl>& datatypes,
-                          std::vector<api::Sort>& sorts,
-                          std::vector<std::vector<ParseOp>>& ops);
-
-  void 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);
-
   /**
    * Adds a constructor to sygus datatype dt whose sygus operator is term.
    *
@@ -427,7 +370,6 @@ class Smt2 : public Parser
   void addSygusConstructorVariables(api::DatatypeDecl& dt,
                                     const std::vector<api::Term>& sygusVars,
                                     api::Sort type) const;
-
   /**
    * Smt2 parser provides its own checkDeclaration, which does the
    * same as the base, but with some more helpful errors.
@@ -442,11 +384,6 @@ class Smt2 : public Parser
     if (name.length() > 1 && name[0] == '-'
         && name.find_first_not_of("0123456789", 1) == std::string::npos)
     {
-      if (sygus_v1())
-      {
-        // "-1" is allowed in SyGuS version 1.0
-        return;
-      }
       std::stringstream ss;
       ss << notes << "You may have intended to apply unary minus: `(- "
          << name.substr(1) << ")'\n";
@@ -537,34 +474,6 @@ class Smt2 : public Parser
   api::Term applyParseOp(ParseOp& p, std::vector<api::Term>& args);
   //------------------------- end processing parse operators
  private:
-  std::map<api::Term, api::Sort> d_sygus_bound_var_type;
-
-  api::Sort 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, api::Term>& sygus_to_builtin_expr,
-      api::Sort sub_ret);
-
-  /** make sygus bound var list
-   *
-   * This is used for converting non-builtin sygus operators to lambda
-   * expressions. It takes as input a datatype and constructor index (for
-   * naming) and a vector of type ltypes.
-   * It appends a bound variable to lvars for each type in ltypes, and returns
-   * a bound variable list whose children are lvars.
-   */
-  api::Term makeSygusBoundVarList(api::DatatypeDecl& dt,
-                                  unsigned i,
-                                  const std::vector<api::Sort>& ltypes,
-                                  std::vector<api::Term>& lvars);
 
   /** Purify sygus grammar term
    *
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index c17684b15..5d54759b9 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -52,14 +52,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
   case LANG_CVC4:
     return unique_ptr<Printer>(new printer::cvc::CvcPrinter());
 
-  case LANG_Z3STR:
-    return unique_ptr<Printer>(
-        new printer::smt2::Smt2Printer(printer::smt2::z3str_variant));
-
-  case LANG_SYGUS_V1:
-    return unique_ptr<Printer>(
-        new printer::smt2::Smt2Printer(printer::smt2::sygus_variant));
-
   case LANG_SYGUS_V2:
     // sygus version 2.0 does not have discrepancies with smt2, hence we use
     // a normal smt2 variant here.
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 31aa67ff9..784e321a0 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -593,35 +593,10 @@ void Smt2Printer::toStream(std::ostream& out,
 
   // string theory
   case kind::STRING_CONCAT:
-    if(d_variant == z3str_variant) {
-      out << "Concat ";
-      for(unsigned i = 0; i < n.getNumChildren(); ++i) {
-        toStream(out, n[i], -1, types, TypeNode::null());
-        if(i + 1 < n.getNumChildren()) {
-          out << ' ';
-        }
-        if(i + 2 < n.getNumChildren()) {
-          out << "(Concat ";
-        }
-      }
-      for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) {
-        out << ")";
-      }
-      return;
-    }
     out << "str.++ ";
     break;
   case kind::STRING_IN_REGEXP: {
     stringstream ss;
-    if(d_variant == z3str_variant && stringifyRegexp(n[1], ss)) {
-      out << "= ";
-      toStream(out, n[0], -1, types, TypeNode::null());
-      out << " ";
-      Node str = NodeManager::currentNM()->mkConst(String(ss.str()));
-      toStream(out, str, -1, types, TypeNode::null());
-      out << ")";
-      return;
-    }
     out << smtKindString(k, d_variant) << " ";
     break;
   }
@@ -1188,7 +1163,7 @@ static string smtKindString(Kind k, Variant v)
 
   //string theory
   case kind::STRING_CONCAT: return "str.++";
-  case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len";
+  case kind::STRING_LENGTH: return "str.len";
   case kind::STRING_SUBSTR: return "str.substr" ;
   case kind::STRING_STRCTN: return "str.contains" ;
   case kind::STRING_CHARAT: return "str.at" ;
@@ -1285,7 +1260,6 @@ void Smt2Printer::toStream(std::ostream& out,
       || tryToStream<EmptyCommand>(out, c)
       || tryToStream<EchoCommand>(out, c, d_variant)
       || tryToStream<SynthFunCommand>(out, c)
-      || tryToStream<DeclareSygusPrimedVarCommand>(out, c)
       || tryToStream<DeclareSygusFunctionCommand>(out, c)
       || tryToStream<DeclareSygusVarCommand>(out, c)
       || tryToStream<SygusConstraintCommand>(out, c)
@@ -1852,12 +1826,7 @@ static void toStream(std::ostream& out,
                      const SetBenchmarkLogicCommand* c,
                      Variant v)
 {
-  // Z3-str doesn't have string-specific logic strings(?), so comment it
-  if(v == z3str_variant) {
-    out << "; (set-logic " << c->getLogic() << ")";
-  } else {
-    out << "(set-logic " << c->getLogic() << ")";
-  }
+  out << "(set-logic " << c->getLogic() << ")";
 }
 
 static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v)
@@ -2021,7 +1990,7 @@ static void toStream(std::ostream& out, const CommentCommand* c, Variant v)
   string s = c->getComment();
   size_t pos = 0;
   while((pos = s.find_first_of('"', pos)) != string::npos) {
-    s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
+    s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
     pos += 2;
   }
   out << "(set-info :notes \"" << s << "\")";
@@ -2035,7 +2004,7 @@ static void toStream(std::ostream& out, const EchoCommand* c, Variant v)
   // escape all double-quotes
   size_t pos = 0;
   while((pos = s.find('"', pos)) != string::npos) {
-    s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
+    s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
     pos += 2;
   }
   out << "(echo \"" << s << "\")";
@@ -2155,12 +2124,6 @@ static void toStream(std::ostream& out, const DeclareSygusFunctionCommand* c)
   out << " (" << argTypes << ") " << ft.getRangeType() << ')';
 }
 
-static void toStream(std::ostream& out, const DeclareSygusPrimedVarCommand* c)
-{
-  out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol())
-      << ' ' << c->getType() << ')';
-}
-
 static void toStream(std::ostream& out, const DeclareSygusVarCommand* c)
 {
   out << '(' << c->getCommandName() << ' ' << c->getVar() << ' ' << c->getType()
@@ -2240,7 +2203,7 @@ static void errorToStream(std::ostream& out, std::string message, Variant v) {
   // escape all double-quotes
   size_t pos = 0;
   while((pos = message.find('"', pos)) != string::npos) {
-    message.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
+    message.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
     pos += 2;
   }
   out << "(error \"" << message << "\")" << endl;
@@ -2270,9 +2233,6 @@ static OutputLanguage variantToLanguage(Variant variant)
   switch(variant) {
   case smt2_0_variant:
     return language::output::LANG_SMTLIB_V2_0;
-  case z3str_variant:
-    return language::output::LANG_Z3STR;
-  case sygus_variant: return language::output::LANG_SYGUS_V1;
   case no_variant:
   default: return language::output::LANG_SMTLIB_V2_6;
   }
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 1330bf79f..398e510cb 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -33,7 +33,6 @@ enum Variant
   smt2_0_variant,  // old-style 2.0 syntax, when it makes a difference
   smt2_6_variant,  // new-style 2.6 syntax, when it makes a difference, with
                    // support for the string standard
-  z3str_variant,   // old-style 2.0 and also z3str syntax
   sygus_variant    // variant for sygus
 };                 /* enum Variant */
 class Smt2Printer : public CVC4::Printer {
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 962882309..cbb2076dd 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -606,48 +606,6 @@ std::string DeclareSygusVarCommand::getCommandName() const
 }
 
 /* -------------------------------------------------------------------------- */
-/* class DeclareSygusPrimedVarCommand */
-/* -------------------------------------------------------------------------- */
-
-DeclareSygusPrimedVarCommand::DeclareSygusPrimedVarCommand(
-    const std::string& id, Type t)
-    : DeclarationDefinitionCommand(id), d_type(t)
-{
-}
-
-Type DeclareSygusPrimedVarCommand::getType() const { return d_type; }
-
-void DeclareSygusPrimedVarCommand::invoke(SmtEngine* smtEngine)
-{
-  try
-  {
-    smtEngine->declareSygusPrimedVar(d_symbol, d_type);
-    d_commandStatus = CommandSuccess::instance();
-  }
-  catch (exception& e)
-  {
-    d_commandStatus = new CommandFailure(e.what());
-  }
-}
-
-Command* DeclareSygusPrimedVarCommand::exportTo(
-    ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
-  return new DeclareSygusPrimedVarCommand(
-      d_symbol, d_type.exportTo(exprManager, variableMap));
-}
-
-Command* DeclareSygusPrimedVarCommand::clone() const
-{
-  return new DeclareSygusPrimedVarCommand(d_symbol, d_type);
-}
-
-std::string DeclareSygusPrimedVarCommand::getCommandName() const
-{
-  return "declare-primed-var";
-}
-
-/* -------------------------------------------------------------------------- */
 /* class DeclareSygusFunctionCommand                                          */
 /* -------------------------------------------------------------------------- */
 
diff --git a/src/smt/command.h b/src/smt/command.h
index f7c780dee..efb4f2f4a 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -675,38 +675,6 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
   Type d_type;
 };
 
-/** Declares a sygus primed variable, for invariant problems
- *
- * We do not actually build expressions for the declared variables because they
- * are unnecessary for building SyGuS problems.
- */
-class CVC4_PUBLIC DeclareSygusPrimedVarCommand
-    : public DeclarationDefinitionCommand
-{
- public:
-  DeclareSygusPrimedVarCommand(const std::string& id, Type type);
-  /** returns the declared primed variable's type */
-  Type getType() const;
-
-  /** invokes this command
-   *
-   * The type of the primed variable is communicated to the SMT engine for
-   * debugging purposes when a synthesis conjecture is built later on.
-   */
-  void invoke(SmtEngine* smtEngine) override;
-  /** exports command to given expression manager */
-  Command* exportTo(ExprManager* exprManager,
-                    ExprManagerMapCollection& variableMap) override;
-  /** creates a copy of this command */
-  Command* clone() const override;
-  /** returns this command's name */
-  std::string getCommandName() const override;
-
- protected:
-  /** the type of the declared primed variable */
-  Type d_type;
-};
-
 /** Declares a sygus universal function variable */
 class CVC4_PUBLIC DeclareSygusFunctionCommand
     : public DeclarationDefinitionCommand
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b826ef23d..a6d89aaf5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1873,15 +1873,6 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
   // don't need to set that the conjecture is stale
 }
 
-void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type)
-{
-  SmtScope smts(this);
-  finalOptionsAreSet();
-  // do nothing (the command is spurious)
-  Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n";
-  // don't need to set that the conjecture is stale
-}
-
 void SmtEngine::declareSygusFunctionVar(const std::string& id,
                                         Expr var,
                                         Type type)
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index b1e3313d8..8a9a60251 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -404,16 +404,6 @@ class CVC4_PUBLIC SmtEngine
   void declareSygusVar(const std::string& id, Expr var, Type type);
 
   /**
-   * Store information for debugging sygus invariants setup.
-   *
-   * Since in SyGuS the commands "declare-primed-var" are not necessary for
-   * building invariant constraints, we only use them to check that the number
-   * of variables declared corresponds to the number of arguments of the
-   * invariant-to-synthesize.
-   */
-  void declareSygusPrimedVar(const std::string& id, Type type);
-
-  /**
    * Add a function variable declaration.
    *
    * Is SyGuS semantics declared functions are treated in the same manner as
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 8b527d322..0ed063ebc 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -374,7 +374,6 @@ void Result::toStreamTptp(std::ostream& out) const {
 
 void Result::toStream(std::ostream& out, OutputLanguage language) const {
   switch (language) {
-    case language::output::LANG_SYGUS_V1:
     case language::output::LANG_SYGUS_V2: toStreamSmt2(out); break;
     case language::output::LANG_TPTP:
       toStreamTptp(out);
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index 9b8ad81b8..6f2da480e 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -272,7 +272,6 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr,
 
 bool SExpr::languageQuotesKeywords(OutputLanguage language) {
   switch (language) {
-    case language::output::LANG_SYGUS_V1:
     case language::output::LANG_TPTP:
       return true;
     case language::output::LANG_AST: