diff options
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 | 2 |
4 files changed, 25 insertions, 4 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 26b598413..ca5d23cd1 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -771,7 +771,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 ba3dc9fb0..aab04c32c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -137,6 +137,7 @@ d_presolve_cache_wic(u){ } QuantifiersEngine::~QuantifiersEngine(){ + delete d_alpha_equiv; delete d_builder; delete d_rr_engine; delete d_bint; @@ -1447,4 +1448,3 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, Type } //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth } - |