4 files changed, 0 insertions, 93 deletions
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