d_size(size),
d_sizeAlloc(sizeAlloc) {
}
- ~CDChunkListSave() throw() {
+ ~CDChunkListSave() {
this->destroy();
}
ContextObj* save(ContextMemoryManager* pCMM) {
/**
* Destructor: delete the list
*/
- ~CDChunkList() throw(AssertionException) {
+ ~CDChunkList() {
this->destroy();
if(this->d_callDestructor) {
}
}
- ~CDOhash_map() throw(AssertionException) {
+ ~CDOhash_map() {
destroy();
}
d_trash() {
}
- ~CDHashMap() throw(AssertionException) {
+ ~CDHashMap() {
Debug("gc") << "cdhashmap" << this
<< " disappearing, destroying..." << std::endl;
destroy();
/**
* Destructor: delete the d_insertMap
*/
- ~CDInsertHashMap() throw(AssertionException) {
+ ~CDInsertHashMap() {
this->destroy();
delete d_insertMap;
}
/**
* Destructor: delete the list
*/
- ~CDList() throw(AssertionException) {
+ ~CDList() {
this->destroy();
if(this->d_callDestructor) {
/**
* Destructor - call destroy() method
*/
- ~CDO() throw(AssertionException) { destroy(); }
+ ~CDO() { destroy(); }
/**
* Set the data in the CDO. First call makeCurrent.
/**
* Destructor: delete the map
*/
- ~CDTrailHashMap() throw(AssertionException) {
+ ~CDTrailHashMap() {
this->destroy();
delete d_trailMap;
}
}
-Context::~Context() throw(AssertionException) {
+Context::~Context() {
// Delete all Scopes
popto(0);
}
-ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) {
+ContextNotifyObj::~ContextNotifyObj() {
if(d_pCNOnext != NULL) {
d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
}
/**
* Destructor: pop all scopes, delete ContextMemoryManager
*/
- ~Context() throw(AssertionException);
+ ~Context();
/**
* Return the current (top) scope
* Destructor: Restore all of the objects in ContextObjList. Defined inline
* below.
*/
- ~Scope() throw(AssertionException);
+ ~Scope();
/**
* Get the Context for this Scope
/**
* 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
/**
* Destructor: removes object from list
*/
- virtual ~ContextNotifyObj() throw(AssertionException);
+ virtual ~ContextNotifyObj();
};/* class ContextNotifyObj */
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.
}
-ContextMemoryManager::~ContextMemoryManager() throw() {
+ContextMemoryManager::~ContextMemoryManager() {
// Delete all chunks
while(!d_chunkList.empty()) {
free(d_chunkList.back());
/**
* Destructor - deletes all memory in all regions
*/
- ~ContextMemoryManager() throw();
+ ~ContextMemoryManager();
/**
* Allocate size bytes from the current region
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; }
d_offset(ctxt, 0) {
}
- ~StackingVector() throw() { }
+ ~StackingVector() { }
/**
* Return a value from the vector. If n is not a key in
* 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.
}
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
* 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
d_nv->inc();
}
-inline TypeNode::~TypeNode() throw(AssertionException) {
+inline TypeNode::~TypeNode() {
Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
d_nv->dec();
}
}
-BVMinisatSatSolver::~BVMinisatSatSolver() throw(AssertionException) {
+BVMinisatSatSolver::~BVMinisatSatSolver() {
delete d_minisat;
delete d_minisatNotify;
}
}
}
-
-
public:
BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = "");
- ~BVMinisatSatSolver() throw(AssertionException);
+ virtual ~BVMinisatSatSolver();
void setNotify(Notify* notify);
}
-CryptoMinisatSolver::~CryptoMinisatSolver() throw(AssertionException) {
+CryptoMinisatSolver::~CryptoMinisatSolver() {
delete d_solver;
}
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);
} // CVC4
#endif // CVC4_USE_CRYPTOMINISAT
-
-
-
-
d_statistics(registry)
{}
-MinisatSatSolver::~MinisatSatSolver() throw()
+MinisatSatSolver::~MinisatSatSolver()
{
delete d_minisat;
}
public:
MinisatSatSolver(StatisticsRegistry* registry);
- ~MinisatSatSolver() throw();
+ virtual ~MinisatSatSolver();
;
static SatVariable toSatVariable(Minisat::Var var);
public:
/** Virtual destructor */
- virtual ~SatSolver() throw(AssertionException) { }
+ virtual ~SatSolver() { }
/** Assert a clause in the solver. */
virtual ClauseId addClause(SatClause& clause,
class BVSatSolverInterface: public SatSolver {
public:
- virtual ~BVSatSolverInterface() throw(AssertionException) {}
+ virtual ~BVSatSolverInterface() {}
/** Interface for notifications */
class Notify {
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.
smtStatisticsRegistry()->registerStat(&d_statSharedTerms);
}
-SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException)
+SharedTermsDatabase::~SharedTermsDatabase()
{
smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms);
}
public:
SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);
- ~SharedTermsDatabase() throw(AssertionException);
+ ~SharedTermsDatabase();
/**
* Asserts the equality to the shared terms database,
d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS;
}
-EqualityEngine::~EqualityEngine() throw(AssertionException) {
+EqualityEngine::~EqualityEngine() {
free(d_triggerDatabase);
}
/**
* Just a destructor.
*/
- virtual ~EqualityEngine() throw(AssertionException);
+ virtual ~EqualityEngine();
/**
* Set the master equality engine for this one. Master engine will get copies of all
projects / cvc5.git / commitdiff