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/theory/quantifiers/quant_conflict_find.cpp | |
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/theory/quantifiers/quant_conflict_find.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 23 |
1 files changed, 22 insertions, 1 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; |