From b2ff9864ed706911022d7468cde7ba55d07ab1fd Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 22 Oct 2010 23:19:14 +0000 Subject: [PATCH] removing unused functionality from util; related to bug #222 --- src/smt/smt_engine.h | 1 - src/util/Makefile.am | 3 --- src/util/model.h | 31 ------------------------------- src/util/triple.h | 43 ------------------------------------------- src/util/unique_id.h | 44 -------------------------------------------- 5 files changed, 122 deletions(-) delete mode 100644 src/util/model.h delete mode 100644 src/util/triple.h delete mode 100644 src/util/unique_id.h diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 35bfb0bcc..a73dbdad9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -32,7 +32,6 @@ #include "smt/modal_exception.h" #include "smt/no_such_function_exception.h" #include "util/hash.h" -#include "util/model.h" #include "util/options.h" #include "util/result.h" #include "util/sexpr.h" diff --git a/src/util/Makefile.am b/src/util/Makefile.am index e75735f82..af3457550 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -17,14 +17,12 @@ libutil_la_SOURCES = \ exception.h \ hash.h \ bool.h \ - model.h \ options.h \ options.cpp \ output.cpp \ output.h \ result.h \ result.cpp \ - unique_id.h \ configuration.h \ configuration_private.h \ configuration.cpp \ @@ -36,7 +34,6 @@ libutil_la_SOURCES = \ sexpr.h \ stats.h \ stats.cpp \ - triple.h \ dynamic_array.h \ language.h diff --git a/src/util/model.h b/src/util/model.h deleted file mode 100644 index 31fed1f31..000000000 --- a/src/util/model.h +++ /dev/null @@ -1,31 +0,0 @@ -/********************* */ -/*! \file model.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief A model. - ** - ** A model. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__MODEL_H -#define __CVC4__MODEL_H - -namespace CVC4 { - -class CVC4_PUBLIC Model { -};/* class Model */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__MODEL_H */ diff --git a/src/util/triple.h b/src/util/triple.h deleted file mode 100644 index 3a6f841c4..000000000 --- a/src/util/triple.h +++ /dev/null @@ -1,43 +0,0 @@ -/********************* */ -/*! \file triple.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Similar to std::pair<>, for triples - ** - ** Similar to std::pair<>, for triples. Once we move to c++0x, this - ** can be removed in favor of (standard-provided) N-ary tuples. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__TRIPLE_H -#define __CVC4__TRIPLE_H - -namespace CVC4 { - -template -class triple { -public: - T1 first; - T2 second; - T3 third; -}; - -template -inline triple -make_triple(const T1& t1, const T2& t2, const T3& t3) { - return triple(t1, t2, t3); -} - -}/* CVC4 namespace */ - -#endif /* __CVC4__TRIPLE_H */ diff --git a/src/util/unique_id.h b/src/util/unique_id.h deleted file mode 100644 index 67a6c5cff..000000000 --- a/src/util/unique_id.h +++ /dev/null @@ -1,44 +0,0 @@ -/********************* */ -/*! \file unique_id.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief A mechanism for getting a compile-time unique ID. - ** - ** A mechanism for getting a compile-time unique ID. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__UNIQUE_ID_H -#define __CVC4__UNIQUE_ID_H - -namespace CVC4 { - -// NOTE that UniqueID is intended for startup registration; it -// shouldn't be used in multi-threaded contexts. - -template -class UniqueID { - static unsigned s_topID; - const unsigned d_thisID; - -public: - UniqueID() : d_thisID( s_topID++ ) { } - operator unsigned() const { return d_thisID; } -}; - -template -unsigned UniqueID::s_topID = 0; - -}/* CVC4 namespace */ - -#endif /* __CVC4__UNIQUE_ID_H */ -- 2.30.2