summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/quantifiers/model_builder.cpp24
1 files changed, 14 insertions, 10 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 8fd659009..a72293ea1 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -34,11 +34,11 @@ using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-
-QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) :
-TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_qe( qe ){
-
-}
+QModelBuilder::QModelBuilder(context::Context* c, QuantifiersEngine* qe)
+ : TheoryEngineModelBuilder(qe->getTheoryEngine()),
+ d_qe(qe),
+ d_addedLemmas(0),
+ d_triedLemmas(0) {}
bool QModelBuilder::optUseModel() {
return options::mbqiMode()!=MBQI_NONE || options::fmfBound();
@@ -163,11 +163,15 @@ bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex)
}
}
-
-QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) :
-QModelBuilder( c, qe ), d_basisNoMatch( c ) {
-
-}
+QModelBuilderIG::QModelBuilderIG(context::Context* c, QuantifiersEngine* qe)
+ : QModelBuilder(c, qe),
+ d_basisNoMatch(c),
+ d_didInstGen(false),
+ d_numQuantSat(0),
+ d_numQuantInstGen(0),
+ d_numQuantNoInstGen(0),
+ d_numQuantNoSelForm(0),
+ d_instGenMatches(0) {}
/*
Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback