/*! \file bv_quick_check.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Paul Meng, Morgan Deters
+ ** Liana Hadarean, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
class BVQuickCheck {
context::Context d_ctx;
- TLazyBitblaster* d_bitblaster;
+ std::unique_ptr<TLazyBitblaster> d_bitblaster;
Node d_conflict;
context::CDO<bool> d_inConflict;
void setConflict();
* @return
*/
uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
- void collectModelInfo(theory::TheoryModel* model, bool fullModel);
+ bool collectModelInfo(theory::TheoryModel* model, bool fullModel);
typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
vars_iterator beginVars();
IntStat d_numConflictsMinimized;
IntStat d_finalPeriod;
AverageStat d_avgMinimizationRatio;
- Statistics(const std::string&);
+ Statistics(const std::string& name);
~Statistics();
};
BVQuickCheck* d_solver;