summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/context/cdchunk_list.h4
-rw-r--r--src/context/cdhashmap.h4
-rw-r--r--src/context/cdinsert_hashmap.h2
-rw-r--r--src/context/cdlist.h2
-rw-r--r--src/context/cdo.h2
-rw-r--r--src/context/cdtrail_hashmap.h2
-rw-r--r--src/context/context.cpp4
-rw-r--r--src/context/context.h10
-rw-r--r--src/context/context_mm.cpp2
-rw-r--r--src/context/context_mm.h4
-rw-r--r--src/context/stacking_vector.h2
-rw-r--r--src/expr/node.h4
-rw-r--r--src/expr/type_node.h4
-rw-r--r--src/prop/bvminisat/bvminisat.cpp4
-rw-r--r--src/prop/bvminisat/bvminisat.h2
-rw-r--r--src/prop/cryptominisat.cpp2
-rw-r--r--src/prop/cryptominisat.h6
-rw-r--r--src/prop/minisat/minisat.cpp2
-rw-r--r--src/prop/minisat/minisat.h2
-rw-r--r--src/prop/sat_solver.h4
-rw-r--r--src/theory/bv/bv_inequality_graph.h2
-rw-r--r--src/theory/shared_terms_database.cpp2
-rw-r--r--src/theory/shared_terms_database.h2
-rw-r--r--src/theory/uf/equality_engine.cpp2
-rw-r--r--src/theory/uf/equality_engine.h2
25 files changed, 36 insertions, 42 deletions
diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h
index 3fa3c6b5d..e75f4de4d 100644
--- a/src/context/cdchunk_list.h
+++ b/src/context/cdchunk_list.h
@@ -137,7 +137,7 @@ protected:
d_size(size),
d_sizeAlloc(sizeAlloc) {
}
- ~CDChunkListSave() throw() {
+ ~CDChunkListSave() {
this->destroy();
}
ContextObj* save(ContextMemoryManager* pCMM) {
@@ -322,7 +322,7 @@ public:
/**
* Destructor: delete the list
*/
- ~CDChunkList() throw(AssertionException) {
+ ~CDChunkList() {
this->destroy();
if(this->d_callDestructor) {
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 884234eb8..6ae74fbde 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -236,7 +236,7 @@ public:
}
}
- ~CDOhash_map() throw(AssertionException) {
+ ~CDOhash_map() {
destroy();
}
@@ -327,7 +327,7 @@ public:
d_trash() {
}
- ~CDHashMap() throw(AssertionException) {
+ ~CDHashMap() {
Debug("gc") << "cdhashmap" << this
<< " disappearing, destroying..." << std::endl;
destroy();
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index 6e772068b..e901e9413 100644
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -271,7 +271,7 @@ public:
/**
* Destructor: delete the d_insertMap
*/
- ~CDInsertHashMap() throw(AssertionException) {
+ ~CDInsertHashMap() {
this->destroy();
delete d_insertMap;
}
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 4e42c4688..4a5ebfd30 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -257,7 +257,7 @@ public:
/**
* Destructor: delete the list
*/
- ~CDList() throw(AssertionException) {
+ ~CDList() {
this->destroy();
if(this->d_callDestructor) {
diff --git a/src/context/cdo.h b/src/context/cdo.h
index e2fdcf9bd..21465181c 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -140,7 +140,7 @@ public:
/**
* Destructor - call destroy() method
*/
- ~CDO() throw(AssertionException) { destroy(); }
+ ~CDO() { destroy(); }
/**
* Set the data in the CDO. First call makeCurrent.
diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h
index e89c1b528..90816d542 100644
--- a/src/context/cdtrail_hashmap.h
+++ b/src/context/cdtrail_hashmap.h
@@ -452,7 +452,7 @@ public:
/**
* Destructor: delete the map
*/
- ~CDTrailHashMap() throw(AssertionException) {
+ ~CDTrailHashMap() {
this->destroy();
delete d_trailMap;
}
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 9c0416ce8..8f151ad08 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -35,7 +35,7 @@ Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
}
-Context::~Context() throw(AssertionException) {
+Context::~Context() {
// Delete all Scopes
popto(0);
@@ -306,7 +306,7 @@ ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
}
-ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) {
+ContextNotifyObj::~ContextNotifyObj() {
if(d_pCNOnext != NULL) {
d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
}
diff --git a/src/context/context.h b/src/context/context.h
index 4f45e8954..f7707bdec 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -152,7 +152,7 @@ public:
/**
* Destructor: pop all scopes, delete ContextMemoryManager
*/
- ~Context() throw(AssertionException);
+ ~Context();
/**
* Return the current (top) scope
@@ -277,7 +277,7 @@ public:
* Destructor: Restore all of the objects in ContextObjList. Defined inline
* below.
*/
- ~Scope() throw(AssertionException);
+ ~Scope();
/**
* Get the Context for this Scope
@@ -615,7 +615,7 @@ public:
/**
* Destructor does nothing: subclass must explicitly call destroy() instead.
*/
- virtual ~ContextObj() throw(AssertionException) {}
+ virtual ~ContextObj() {}
/**
* If you want to allocate a ContextObj object on the heap, use this
@@ -711,7 +711,7 @@ public:
/**
* Destructor: removes object from list
*/
- virtual ~ContextNotifyObj() throw(AssertionException);
+ virtual ~ContextNotifyObj();
};/* class ContextNotifyObj */
@@ -725,7 +725,7 @@ inline void ContextObj::makeSaveRestorePoint() throw(AssertionException) {
update();
}
-inline Scope::~Scope() throw(AssertionException) {
+inline Scope::~Scope() {
// Call restore() method on each ContextObj object in the list.
// Note that it is the responsibility of restore() to return the
// next item in the list.
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index 0a6b08b6a..2dc2c03bb 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -63,7 +63,7 @@ ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) {
}
-ContextMemoryManager::~ContextMemoryManager() throw() {
+ContextMemoryManager::~ContextMemoryManager() {
// Delete all chunks
while(!d_chunkList.empty()) {
free(d_chunkList.back());
diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index 99b448cf2..673fb9098 100644
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -118,7 +118,7 @@ public:
/**
* Destructor - deletes all memory in all regions
*/
- ~ContextMemoryManager() throw();
+ ~ContextMemoryManager();
/**
* Allocate size bytes from the current region
@@ -161,7 +161,7 @@ public:
ContextMemoryAllocator(ContextMemoryManager* mm) throw() : d_mm(mm) {}
template <class U>
ContextMemoryAllocator(const ContextMemoryAllocator<U>& alloc) throw() : d_mm(alloc.getCMM()) {}
- ~ContextMemoryAllocator() throw() {}
+ ~ContextMemoryAllocator() {}
ContextMemoryManager* getCMM() const { return d_mm; }
T* address(T& v) const { return &v; }
diff --git a/src/context/stacking_vector.h b/src/context/stacking_vector.h
index b737c40ae..4b482c9b0 100644
--- a/src/context/stacking_vector.h
+++ b/src/context/stacking_vector.h
@@ -50,7 +50,7 @@ public:
d_offset(ctxt, 0) {
}
- ~StackingVector() throw() { }
+ ~StackingVector() { }
/**
* Return a value from the vector. If n is not a key in
diff --git a/src/expr/node.h b/src/expr/node.h
index 998294da3..c9bfb75a4 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -308,7 +308,7 @@ public:
* Destructor. If ref_count is true it will decrement the reference count
* and, if zero, collect the NodeValue.
*/
- ~NodeTemplate() throw(AssertionException);
+ ~NodeTemplate();
/**
* Return the null node.
@@ -1089,7 +1089,7 @@ NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
}
template <bool ref_count>
-NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) {
+NodeTemplate<ref_count>::~NodeTemplate() {
Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
if(ref_count) {
// shouldn't ever fail
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 46fdaa143..0cada0df2 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -116,7 +116,7 @@ public:
* Destructor. If ref_count is true it will decrement the reference count
* and, if zero, collect the NodeValue.
*/
- ~TypeNode() throw(AssertionException);
+ ~TypeNode();
/**
* Assignment operator for nodes, copies the relevant information from node
@@ -785,7 +785,7 @@ inline TypeNode::TypeNode(const TypeNode& typeNode) {
d_nv->inc();
}
-inline TypeNode::~TypeNode() throw(AssertionException) {
+inline TypeNode::~TypeNode() {
Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
d_nv->dec();
}
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 54e3f2e8b..368a79b80 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -39,7 +39,7 @@ BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Co
}
-BVMinisatSatSolver::~BVMinisatSatSolver() throw(AssertionException) {
+BVMinisatSatSolver::~BVMinisatSatSolver() {
delete d_minisat;
delete d_minisatNotify;
}
@@ -309,5 +309,3 @@ void toSatClause< BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_
}
}
-
-
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 56a7c61e2..732bd0313 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -72,7 +72,7 @@ protected:
public:
BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = "");
- ~BVMinisatSatSolver() throw(AssertionException);
+ virtual ~BVMinisatSatSolver();
void setNotify(Notify* notify);
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index d8f25a786..eff079cc9 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -45,7 +45,7 @@ CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
}
-CryptoMinisatSolver::~CryptoMinisatSolver() throw(AssertionException) {
+CryptoMinisatSolver::~CryptoMinisatSolver() {
delete d_solver;
}
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index 54d52af0e..7ad861def 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -38,7 +38,7 @@ private:
public:
CryptoMinisatSolver(StatisticsRegistry* registry,
const std::string& name = "");
- ~CryptoMinisatSolver() throw(AssertionException);
+ virtual ~CryptoMinisatSolver();
ClauseId addClause(SatClause& clause, bool removable);
ClauseId addXorClause(SatClause& clause, bool rhs, bool removable);
@@ -132,7 +132,3 @@ public:
} // CVC4
#endif // CVC4_USE_CRYPTOMINISAT
-
-
-
-
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index ff726e299..a88a872c8 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -38,7 +38,7 @@ MinisatSatSolver::MinisatSatSolver(StatisticsRegistry* registry) :
d_statistics(registry)
{}
-MinisatSatSolver::~MinisatSatSolver() throw()
+MinisatSatSolver::~MinisatSatSolver()
{
delete d_minisat;
}
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index ec5297bb7..1627a6575 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -29,7 +29,7 @@ class MinisatSatSolver : public DPLLSatSolverInterface {
public:
MinisatSatSolver(StatisticsRegistry* registry);
- ~MinisatSatSolver() throw();
+ virtual ~MinisatSatSolver();
;
static SatVariable toSatVariable(Minisat::Var var);
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 81fb94242..4afaea5a0 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -43,7 +43,7 @@ class SatSolver {
public:
/** Virtual destructor */
- virtual ~SatSolver() throw(AssertionException) { }
+ virtual ~SatSolver() { }
/** Assert a clause in the solver. */
virtual ClauseId addClause(SatClause& clause,
@@ -99,7 +99,7 @@ public:
class BVSatSolverInterface: public SatSolver {
public:
- virtual ~BVSatSolverInterface() throw(AssertionException) {}
+ virtual ~BVSatSolverInterface() {}
/** Interface for notifications */
class Notify {
public:
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 452172586..923e1d8c5 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -242,7 +242,7 @@ public:
*/
bool addDisequality(TNode a, TNode b, TNode reason);
void getConflict(std::vector<TNode>& conflict);
- virtual ~InequalityGraph() throw(AssertionException) {}
+ virtual ~InequalityGraph() {}
/**
* Check that the currently asserted disequalities that have not been split on
* are still true in the current model.
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 0dc6cc7a1..b78109dfb 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -37,7 +37,7 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Co
smtStatisticsRegistry()->registerStat(&d_statSharedTerms);
}
-SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException)
+SharedTermsDatabase::~SharedTermsDatabase()
{
smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms);
}
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index c108122ef..cc8959165 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -149,7 +149,7 @@ private:
public:
SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);
- ~SharedTermsDatabase() throw(AssertionException);
+ ~SharedTermsDatabase();
/**
* Asserts the equality to the shared terms database,
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 09d348584..f98ad556f 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -97,7 +97,7 @@ void EqualityEngine::init() {
d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS;
}
-EqualityEngine::~EqualityEngine() throw(AssertionException) {
+EqualityEngine::~EqualityEngine() {
free(d_triggerDatabase);
}
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 843e7ce7f..18e83bd1a 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -186,7 +186,7 @@ public:
/**
* Just a destructor.
*/
- virtual ~EqualityEngine() throw(AssertionException);
+ virtual ~EqualityEngine();
/**
* Set the master equality engine for this one. Master engine will get copies of all
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback