From 32fdf625f66b8ebf260756962a53d63eec771c12 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 20 Feb 2020 12:07:46 -0800 Subject: [PATCH] Remove unused code (#3782) --- src/cvc4.i | 22 ---------------------- src/expr/datatype.i | 16 ---------------- src/expr/expr_manager.i | 13 ------------- src/smt/command.cpp | 17 ----------------- src/util/CMakeLists.txt | 1 - src/util/debug.h | 37 ------------------------------------- 6 files changed, 106 deletions(-) delete mode 100644 src/util/debug.h diff --git a/src/cvc4.i b/src/cvc4.i index 97462170e..f9f8f5743 100644 --- 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 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 . -# 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 83e21793c..1ac89efcb 100644 --- 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 dbfd01242..f8251e752 100644 --- 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&); - %ignore CVC4::ExprManager::mkExpr(Kind, Expr, const std::vector&); - %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&); -#endif /* SWIGOCAML */ - %ignore CVC4::stats::getStatisticsRegistry(ExprManager*); %ignore CVC4::ExprManager::getResourceManager(); diff --git a/src/smt/command.cpp b/src/smt/command.cpp index ce8d4fa88..c1aa89832 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -41,23 +41,6 @@ using namespace std; namespace CVC4 { -namespace { - -std::vector ExportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap, - const std::vector& exprs) -{ - std::vector 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 cf4a288c3..75597edac 100644 --- 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 index e25ca8168..000000000 --- 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 - -#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 */ -- 2.30.2