summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_conflict_find.cpp
diff options
context:
space:
mode:
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 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback