diff options
author | Tim King <taking@cs.nyu.edu> | 2017-11-07 20:18:30 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-07 22:18:30 -0600 |
commit | 9444927c027e96f0fce22398611b97c274eff6b3 (patch) | |
tree | 225fa57b324402f46ece25b34c8c5ec0dab074b6 /src | |
parent | 9b9f849471b752a4188230153d1b8b7b8a0a930b (diff) |
Initializing QModelBuilder members. (#1334)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 24 |
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 ) { |