summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2017-11-07 20:18:30 -0800
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-11-07 22:18:30 -0600
commit9444927c027e96f0fce22398611b97c274eff6b3 (patch)
tree225fa57b324402f46ece25b34c8c5ec0dab074b6 /src
parent9b9f849471b752a4188230153d1b8b7b8a0a930b (diff)
Initializing QModelBuilder members. (#1334)
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