Use std:unique_ptr instead of raw pointers in theory/bv. (#2385)

[cvc5.git] / src / theory / bv / bv_quick_check.h

diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 8d2a6228763cfea83b5ea4f8306d341d7f83ab38..b2c31edcbab4678dafa3e10e67f2bfba7deb7747 100644 (file)
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \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.
  **
@@ -20,7 +20,7 @@
 #define __CVC4__BV_QUICK_CHECK_H
 
 #include <vector>
-#include <ext/hash_map>
+#include <unordered_set>
 
 #include "context/cdo.h"
 #include "expr/node.h"
@@ -40,7 +40,7 @@ class TheoryBV;
 
 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();
@@ -97,9 +97,9 @@ public:
    * @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(); 
 
@@ -117,7 +117,7 @@ class QuickXPlain {
     IntStat d_numConflictsMinimized;
     IntStat d_finalPeriod;
     AverageStat d_avgMinimizationRatio;
-    Statistics(const std::string&);
+    Statistics(const std::string& name);
     ~Statistics();
   };
   BVQuickCheck* d_solver;