summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_conflict_find.cpp
diff options
context:
space:
mode:
authorTim King <taking@google.com>2015-11-05 14:56:49 -0800
committerTim King <taking@google.com>2015-11-05 14:56:49 -0800
commit0348ee46cb5cfda75fc877e73f176838140fbe61 (patch)
tree5cec2e2482858fe3f469401b68dd754578174cba /src/theory/quantifiers/quant_conflict_find.cpp
parente4ac720f865ce499c6f818f0cdb60dfabe913df5 (diff)
parent859ae93590062ba7fef5577c6577068f0b74c239 (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.cpp23
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback