Remove unused code (#3782)

diff --git a/src/cvc4.i b/src/cvc4.i
index 97462170e905684c29410cd2c244a0fcba578fe9..f9f8f574368ce47ab44e86be00d9771464d4f7a1 100644 (file)
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -15,28 +15,6 @@ namespace std {
 }
 
 %{
-// Perl's headers define "seed" to Perl_seed, which breaks
-// gmpxx.h; undo the damage for our CVC4 module.
-#ifdef SWIGPERL
-#  undef seed
-#endif /* SWIGPERL */
-
-// OCaml's headers define "invalid_argument" and "flush" to
-// caml_invalid_argument and caml_flush, which breaks C++
-// standard headers; undo this damage
-//
-// Unfortunately, this code isn't inserted early enough.  swig puts
-// an include <stdexcept> very early, which breaks linking due to a
-// nonexistent std::caml_invalid_argument symbol.. ridiculous!
-//
-#ifdef SWIGOCAML
-#  if defined(flush) || defined(invalid_argument)
-#    error "flush" or "invalid_argument" (or both) is defined by the ocaml headers.  You must #undef it above before inclusion of <stdexcept>.
-#  endif /* flush */
-#  undef flush
-#  undef invalid_argument
-#endif /* SWIGOCAML */
-
 namespace CVC4 {}
 using namespace CVC4;
 

diff --git a/src/expr/datatype.i b/src/expr/datatype.i
index 83e21793cf077c16e5e2b318ba0617d07fb29610..1ac89efcb1cb2604a56e53476c570e4663e27550 100644 (file)
--- a/src/expr/datatype.i
+++ b/src/expr/datatype.i
@@ -12,14 +12,6 @@
 %include "expr/kind.i"
 
 %extend std::vector< CVC4::Datatype > {
-  /* These member functions have slightly different signatures in
-   * different swig language packages.  The underlying issue is that
-   * DatatypeConstructor doesn't have a default constructor */
-#if defined(SWIGOCAML) || defined(SWIGPERL) || defined(SWIGTCL)
-  %ignore vector(unsigned int size = 0);
-  %ignore set( int i, const CVC4::Datatype &x );
-  %ignore to_array();
-#endif /* SWIGOCAML || SWIGPERL || SWIGTCL */
   %ignore vector(size_type);// java/python/perl/others?
   %ignore resize(size_type);// java/python/perl/others?
   %ignore set(int i, const CVC4::Datatype& x);
@@ -28,14 +20,6 @@
 %template(vectorDatatype) std::vector< CVC4::Datatype >;
 
 %extend std::vector< CVC4::DatatypeConstructor > {
-  /* These member functions have slightly different signatures in
-   * different swig language packages.  The underlying issue is that
-   * DatatypeConstructor doesn't have a default constructor */
-#if defined(SWIGOCAML) || defined(SWIGPERL) || defined(SWIGTCL)
-  %ignore vector(unsigned int size = 0);
-  %ignore set( int i, const CVC4::DatatypeConstructor &x );
-  %ignore to_array();
-#endif /* SWIGOCAML || SWIGPERL || SWIGTCL */
   %ignore vector(size_type);// java/python/perl/others?
   %ignore resize(size_type);// java/python/perl/others?
   %ignore set(int i, const CVC4::Datatype::Constructor& x);

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index dbfd01242e254c2a0dfd12d5d71582575ef25303..f8251e752a0a718bb6a866f9d1d98330ceb46dab 100644 (file)
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -23,19 +23,6 @@
     }
   }
 
-#ifdef SWIGOCAML
-  /* OCaml bindings cannot deal with this degree of overloading */
-  %ignore CVC4::ExprManager::mkExpr(Kind, const std::vector<Expr>&);
-  %ignore CVC4::ExprManager::mkExpr(Kind, Expr, const std::vector<Expr>&);
-  %ignore CVC4::ExprManager::mkExpr(Expr);
-  %ignore CVC4::ExprManager::mkExpr(Expr, Expr);
-  %ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr);
-  %ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr, Expr);
-  %ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr, Expr, Expr);
-  %ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr, Expr, Expr, Expr);
-  %ignore CVC4::ExprManager::mkExpr(Expr, const std::vector<Expr>&);
-#endif /* SWIGOCAML */
-
 %ignore CVC4::stats::getStatisticsRegistry(ExprManager*);
 %ignore CVC4::ExprManager::getResourceManager();
 

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index ce8d4fa88f7dc68372ce64f0c0f278225a22c625..c1aa89832ef918aa516c731d5bd72bb771db1256 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -41,23 +41,6 @@ using namespace std;
 
 namespace CVC4 {
 
-namespace {
-
-std::vector<Expr> ExportTo(ExprManager* exprManager,
-                           ExprManagerMapCollection& variableMap,
-                           const std::vector<Expr>& exprs)
-{
-  std::vector<Expr> exported;
-  exported.reserve(exprs.size());
-  for (const Expr& expr : exprs)
-  {
-    exported.push_back(expr.exportTo(exprManager, variableMap));
-  }
-  return exported;
-}
-
-}  // namespace
-
 const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
 const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
 const CommandInterrupted* CommandInterrupted::s_instance =

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index cf4a288c3512940f65a3d6ba83123d411272dcd2..75597edac62935325206e1e32f1fa01baa134143 100644 (file)
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -11,7 +11,6 @@ libcvc4_add_sources(
   bool.h
   cardinality.cpp
   cardinality.h
-  debug.h
   dense_map.h
   divisible.cpp
   divisible.h

diff --git a/src/util/debug.h b/src/util/debug.h
deleted file mode 100644 (file)
index e25ca81..0000000
--- a/src/util/debug.h
+++ /dev/null
@@ -1,37 +0,0 @@
-/*********************                                                        */
-/*! \file debug.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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.\endverbatim
- **
- ** \brief Debugging things.
- **
- ** Debugging things.
- **
- ** These are low-level assertions!  Generally you should use
- ** CVC4::Assert() instead (they throw an exception!).  See
- ** util/Assert.h.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__DEBUG_H
-#define CVC4__DEBUG_H
-
-#include <cassert>
-
-#ifdef CVC4_ASSERTIONS
-// the __builtin_expect() helps us if assert is built-in or a macro
-#  define cvc4assert(x) assert(__builtin_expect( ( x ), true ))
-#else
-// TODO: use a compiler annotation when assertions are off ?
-// (to improve optimization)
-#  define cvc4assert(x) /*__builtin_expect( ( x ), true )*/
-#endif /* CVC4_ASSERTIONS */
-
-#endif /* CVC4__DEBUG_H */