diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2015-04-24 00:35:08 -0700 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2015-04-24 00:35:08 -0700 |
commit | 0bf9566178b30b81ee27ead42bcbfaa668f738e1 (patch) | |
tree | 993c7c8750f1a42080b139ac216ecdb7b1780ae3 /src | |
parent | 9f2ff7173d434162d49814ba3f24a9f9db21d476 (diff) |
Fix compiler errors due to unbalanced throw specifiers.
Diffstat (limited to 'src')
-rw-r--r-- | src/context/cdchunk_list.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 3 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 4 |
5 files changed, 9 insertions, 5 deletions
diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h index 16aa32176..8c2e4066e 100644 --- a/src/context/cdchunk_list.h +++ b/src/context/cdchunk_list.h @@ -136,7 +136,7 @@ protected: d_size(size), d_sizeAlloc(sizeAlloc) { } - ~CDChunkListSave() { + ~CDChunkListSave() throw() { this->destroy(); } ContextObj* save(ContextMemoryManager* pCMM) { diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index b896b03fb..53ab2eccf 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -32,7 +32,8 @@ MinisatSatSolver::MinisatSatSolver() : d_context(NULL) {} -MinisatSatSolver::~MinisatSatSolver() { +MinisatSatSolver::~MinisatSatSolver() throw() +{ delete d_minisat; } diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index a355702bc..2564572c2 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -37,7 +37,8 @@ class MinisatSatSolver : public DPLLSatSolverInterface { public: MinisatSatSolver(); - ~MinisatSatSolver(); + ~MinisatSatSolver() throw(); +; static SatVariable toSatVariable(Minisat::Var var); static Minisat::Lit toMinisatLit(SatLiteral lit); diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index fbcaf938f..25d71984d 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -136,6 +136,7 @@ private: //the following functions are for evaluating quantifier bodies public: FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name); + ~FirstOrderModelIG() throw() {} FirstOrderModelIG * asFirstOrderModelIG() { return this; } // initialize the model void processInitialize( bool ispre ); @@ -218,6 +219,7 @@ private: void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars ); public: FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name); + ~FirstOrderModelAbs() throw() {} FirstOrderModelAbs * asFirstOrderModelAbs() { return this; } void processInitialize( bool ispre ); unsigned getRepresentativeId( TNode n ); diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 47de4e581..a3d239d18 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -123,7 +123,7 @@ protected: //helper functions bool hasConstantDefinition( Node n ); public: QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); - virtual ~QModelBuilderIG(){} + virtual ~QModelBuilderIG() throw() {} public: //whether to add inst-gen lemmas virtual bool optInstGen(); @@ -192,7 +192,7 @@ protected: void constructModelUf( FirstOrderModel* fm, Node op ); public: QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} - ~QModelBuilderDefault(){} + ~QModelBuilderDefault() throw() {} //options bool optReconsiderFuncConstants() { return true; } //has inst gen |