/********************* */
/*! \file bv_quick_check.h
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** 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
**
** \brief Sandboxed sat solver for bv quickchecks.
**
#define __CVC4__BV_QUICK_CHECK_H
#include <vector>
-#include <ext/hash_map>
+#include <unordered_set>
#include "context/cdo.h"
#include "expr/node.h"
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 __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
+ typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
vars_iterator beginVars();
vars_iterator endVars();
IntStat d_numConflictsMinimized;
IntStat d_finalPeriod;
AverageStat d_avgMinimizationRatio;
- Statistics(const std::string&);
+ Statistics(const std::string& name);
~Statistics();
};
BVQuickCheck* d_solver;