diff options
author | Tim King <taking@google.com> | 2015-11-05 14:18:03 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-11-05 14:18:03 -0800 |
commit | 859ae93590062ba7fef5577c6577068f0b74c239 (patch) | |
tree | 81d2d257c28414d10a261c242c1801f3eaadce78 /src | |
parent | b455f5cde8b84b7951d309604b75a76afd8b8bfa (diff) |
Fixes some initialization and desctruction problems in quantifiers. Also restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 23 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_equality_engine.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 1 |
4 files changed, 25 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 9e13ef5eb..cd304c6d4 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -770,7 +770,28 @@ void QuantInfo::debugPrintMatch( const char * c ) { } } -MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){ +MatchGen::MatchGen() + : d_matched_basis(), + d_binding(), + d_tgt(), + d_tgt_orig(), + d_wasSet(), + d_n(), + d_type( typ_invalid ), + d_type_not() +{} + + +MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) + : d_matched_basis(), + d_binding(), + d_tgt(), + d_tgt_orig(), + d_wasSet(), + d_n(), + d_type(), + d_type_not() +{ Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl; std::vector< Node > qni_apps; d_qni_size = 0; diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index d2a982781..11299b532 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -78,7 +78,7 @@ public: }; void debugPrintType( const char * c, short typ, bool isTrace = false ); public: - MatchGen() : d_type( typ_invalid ){} + MatchGen(); MatchGen( QuantInfo * qi, Node n, bool isVar = false ); bool d_tgt; bool d_tgt_orig; diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h index 0de6341cb..35a328147 100755 --- a/src/theory/quantifiers/quant_equality_engine.h +++ b/src/theory/quantifiers/quant_equality_engine.h @@ -64,7 +64,7 @@ private: void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); public: QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ); - ~QuantEqualityEngine(){} + virtual ~QuantEqualityEngine() throw (){} /* whether this module needs to check this round */ bool needsCheck( Theory::Effort e ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 9ae3b1d40..cfe53dd0f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -229,6 +229,7 @@ d_presolve_cache_wic(u){ } QuantifiersEngine::~QuantifiersEngine(){ + delete d_alpha_equiv; delete d_builder; delete d_rr_engine; delete d_bint; |