1 files changed, 0 insertions, 61 deletions
diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h
deleted file mode 100644
index 89e636a65..000000000
--- a/src/smt/defined_function.h
+++ /dev/null
@@ -1,61 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Morgan Deters
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Defined function data structure.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__SMT__DEFINED_FUNCTION_H
-#define CVC5__SMT__DEFINED_FUNCTION_H
-
-#include <vector>
-
-#include "expr/node.h"
-
-namespace cvc5 {
-namespace smt {
-
-/**
- * Representation of a defined function.  We keep these around in
- * SmtEngine to permit expanding definitions late (and lazily), to
- * support getValue() over defined functions, to support user output
- * in terms of defined functions, etc.
- */
-class DefinedFunction
-{
- public:
-  DefinedFunction() {}
-  DefinedFunction(Node func, const std::vector<Node>& formals, Node formula)
-      : d_func(func), d_formals(formals), d_formula(formula)
-  {
-  }
-  /** get the function */
-  Node getFunction() const { return d_func; }
-  /** get the formal argument list of the function */
-  const std::vector<Node>& getFormals() const { return d_formals; }
-  /** get the formula that defines it */
-  Node getFormula() const { return d_formula; }
-
- private:
-  /** the function */
-  Node d_func;
-  /** the formal argument list */
-  std::vector<Node> d_formals;
-  /** the formula */
-  Node d_formula;
-}; /* class DefinedFunction */
-
-}  // namespace smt
-}  // namespace cvc5
-
-#endif /* CVC5__SMT__DEFINED_FUNCTION_H */