1 files changed, 0 insertions, 67 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index c4046b7c2..2fd61aabc 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -630,20 +630,6 @@ void Smt2::includeFile(const std::string& filename) {
   }
 }
 
-void Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed)
-{
-  if (!isPrimed)
-  {
-    d_sygusVars.push_back(mkBoundVar(name, type));
-  }
-#ifdef CVC4_ASSERTIONS
-  else
-  {
-    d_sygusVarPrimed.push_back(mkBoundVar(name, type));
-  }
-#endif
-}
-
 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
   if( type.isInteger() ){
     ops.push_back(getExprManager()->mkConst(Rational(0)));
@@ -1234,59 +1220,6 @@ Expr Smt2::makeSygusBoundVarList(Datatype& dt,
   return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
 }
 
-const void Smt2::getSygusInvVars(FunctionType t,
-                                 std::vector<Expr>& vars,
-                                 std::vector<Expr>& primed_vars)
-{
-  std::vector<Type> argTypes = t.getArgTypes();
-  ExprManager* em = getExprManager();
-  for (const Type& ti : argTypes)
-  {
-    vars.push_back(em->mkBoundVar(ti));
-    d_sygusVars.push_back(vars.back());
-    std::stringstream ss;
-    ss << vars.back() << "'";
-    primed_vars.push_back(em->mkBoundVar(ss.str(), ti));
-    d_sygusVars.push_back(primed_vars.back());
-#ifdef CVC4_ASSERTIONS
-    bool find_new_declared_var = false;
-    for (const Expr& e : d_sygusVarPrimed)
-    {
-      if (e.getType() == ti)
-      {
-        d_sygusVarPrimed.erase(
-            std::find(d_sygusVarPrimed.begin(), d_sygusVarPrimed.end(), e));
-        find_new_declared_var = true;
-        break;
-      }
-    }
-    if (!find_new_declared_var)
-    {
-      ss.str("");
-      ss << "warning: decleared primed variables do not match invariant's "
-            "type\n";
-      warning(ss.str());
-    }
-#endif
-  }
-}
-
-const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){
-  // When constructing the synthesis conjecture, we quantify on the
-  // (higher-order) bound variable synth_fun.
-  d_sygusFunSymbols.push_back(synth_fun);
-
-  // Variable "sfproxy" carries the type, which may be a SyGuS datatype
-  // that corresponds to syntactic restrictions.
-  Expr sym = mkBoundVar("sfproxy", t);
-  std::vector< Expr > attr_value;
-  attr_value.push_back(sym);
-  Command* cattr =
-      new SetUserAttributeCommand("sygus-synth-grammar", synth_fun, attr_value);
-  cattr->setMuted(true);
-  preemptCommand(cattr);
-}
-
 InputLanguage Smt2::getLanguage() const
 {
   ExprManager* em = getExprManager();