diff options
author | Tim King <taking@google.com> | 2015-11-05 14:56:49 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-11-05 14:56:49 -0800 |
commit | 0348ee46cb5cfda75fc877e73f176838140fbe61 (patch) | |
tree | 5cec2e2482858fe3f469401b68dd754578174cba /src/theory/quantifiers/quant_conflict_find.cpp | |
parent | e4ac720f865ce499c6f818f0cdb60dfabe913df5 (diff) | |
parent | 859ae93590062ba7fef5577c6577068f0b74c239 (diff) |
Merging the google branch back into master.
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 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; |