From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 22 Jan 2012 12:34:38 +0000 (+0000)
Subject: Mark most of the classes that shouldn't be copied as noncopyable.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=78db846641c2ce6a6afd2143ffb6eaffc2f92292;p=francis%2Fstp.git

Mark most of the classes that shouldn't be copied as noncopyable.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1512 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index 93c5bb6..8cb41da 100644
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -13,12 +13,13 @@
 #include "AST.h"
 #include "../STPManager/STPManager.h"
 #include "../AST/NodeFactory/SimplifyingNodeFactory.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
   class Simplifier;
 
-  class ArrayTransformer 
+  class ArrayTransformer : boost::noncopyable
   {
   public:
 
diff --git a/src/AST/NodeFactory/NodeFactory.h b/src/AST/NodeFactory/NodeFactory.h
index 4976266..a4e75c6 100644
--- a/src/AST/NodeFactory/NodeFactory.h
+++ b/src/AST/NodeFactory/NodeFactory.h
@@ -4,6 +4,7 @@
 
 #include <vector>
 #include "../ASTKind.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
@@ -19,7 +20,7 @@ using BEEV::Kind;
 using BEEV::ASTVec;
 using BEEV::_empty_ASTVec;
 
-class NodeFactory
+class NodeFactory : boost::noncopyable
 {
 protected:
         BEEV::STPMgr& bm;
diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index 49537fa..b4f120c 100644
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -15,8 +15,9 @@
 #include <string>
 #include "../sat/utils/System.h"
 #include <iomanip>
+#include <boost/utility.hpp>
 
-class RunTimes
+class RunTimes : boost::noncopyable
 {
 public:
   enum Category
diff --git a/src/STPManager/DifficultyScore.h b/src/STPManager/DifficultyScore.h
index b647b56..93dba29 100644
--- a/src/STPManager/DifficultyScore.h
+++ b/src/STPManager/DifficultyScore.h
@@ -6,12 +6,13 @@
 #include "../AST/ASTKind.h"
 #include <list>
 #include "../STPManager/NodeIterator.h"
+#include <boost/utility.hpp>
 
 // estimate how difficult that input is to solve based on some simple rules.
 
 namespace BEEV
 {
-    struct DifficultyScore
+    struct DifficultyScore : boost::noncopyable
     {
     private:
         int
diff --git a/src/STPManager/NodeIterator.h b/src/STPManager/NodeIterator.h
index 78f4a2e..44e93da 100644
--- a/src/STPManager/NodeIterator.h
+++ b/src/STPManager/NodeIterator.h
@@ -2,20 +2,19 @@
 #define NODEITERATOR_H_
 
 #include <stack>
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
     // Returns each node once, then returns the sentinal.
     // NB if the sentinel is contained in the node that's passed, then it'll be wrong.
-    class NodeIterator
+    class NodeIterator : boost::noncopyable
     {
         stack<ASTNode> toVisit;
 
         const ASTNode& sentinal;
         uint8_t iteration;
 
-        NodeIterator( const NodeIterator& other ); // non copyable
-        NodeIterator& operator=( const NodeIterator& ); // non copyable
 
     public:
         NodeIterator(const ASTNode &n, const ASTNode &_sentinal, STPMgr& stp) :
diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 7c9b7f6..9d0536e 100644
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -19,10 +19,12 @@
 #include "../parser/LetMgr.h"
 #include "../absrefine_counterexample/AbsRefine_CounterExample.h"
 #include "../simplifier/PropagateEqualities.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
-  class STP {
+  class STP  : boost::noncopyable
+  {
 
     ArrayTransformer * arrayTransformer;
 
diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 5c3a8b4..f95ba09 100644
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -14,6 +14,7 @@
 #include "../AST/AST.h"
 #include "../AST/NodeFactory/HashingNodeFactory.h"
 #include "../sat/SATSolver.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
@@ -22,7 +23,7 @@ namespace BEEV
    * such as unique tables for the various kinds of nodes.
    *****************************************************************/
 
-  class STPMgr
+  class STPMgr : boost::noncopyable
   {
     friend class ASTNode;
     friend class ASTInterior;
diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index c511b61..b7f241f 100644
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -14,6 +14,8 @@
 #include <assert.h>
 #include <iostream>
 #include <set>
+#include <boost/utility.hpp>
+
 namespace BEEV
 {
 	using std::string;
@@ -25,7 +27,8 @@ namespace BEEV
    * options. 
    ******************************************************************/
 
-  struct UserDefinedFlags {
+  struct UserDefinedFlags : boost::noncopyable
+  {
   private:
 	std::set<string> alreadyOutput;
 
diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index c7437fc..d203e0a 100644
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -15,10 +15,11 @@
 #include "../simplifier/simplifier.h"
 #include "../AST/ArrayTransformer.h"
 #include "../to-sat/ToSATBase.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
-  class AbsRefine_CounterExample
+  class AbsRefine_CounterExample : boost::noncopyable
   {
   private:
 
@@ -165,7 +166,7 @@ namespace BEEV
 
   };//End of Class CounterExample
 
-  class CompleteCounterExample
+  class CompleteCounterExample : boost::noncopyable
   {
     ASTNodeMap counterexample;
     STPMgr * bv;
diff --git a/src/simplifier/AIGSimplifyPropositionalCore.h b/src/simplifier/AIGSimplifyPropositionalCore.h
index 4af2f86..7d9ea66 100644
--- a/src/simplifier/AIGSimplifyPropositionalCore.h
+++ b/src/simplifier/AIGSimplifyPropositionalCore.h
@@ -18,11 +18,12 @@
 #include "../extlib-abc/dar.h"
 #include "../to-sat/AIG/BBNodeManagerAIG.h"
 #include "../to-sat/BitBlaster.h"
-
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
-class AIGSimplifyPropositionalCore {
+class AIGSimplifyPropositionalCore : boost::noncopyable
+{
 
 	ASTNodeMap varToNodeMap;
 	STPMgr * bm;
diff --git a/src/simplifier/AlwaysTrue.h b/src/simplifier/AlwaysTrue.h
index 878e01f..e74df19 100644
--- a/src/simplifier/AlwaysTrue.h
+++ b/src/simplifier/AlwaysTrue.h
@@ -7,11 +7,12 @@
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
 #include "../simplifier/simplifier.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
 
-class AlwaysTrue
+class AlwaysTrue : boost::noncopyable
 {
   Simplifier *simplifier;
   STPMgr* stp;
@@ -27,10 +28,6 @@ public:
     nf = nf_;
   }
 
-  virtual
-  ~AlwaysTrue()
-  {}
-
   ASTNode topLevel(ASTNode& n)
   {
     stp->GetRunTimes()->start(RunTimes::AlwaysTrue);
diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h
index bb10cd9..572d986 100644
--- a/src/simplifier/EstablishIntervals.h
+++ b/src/simplifier/EstablishIntervals.h
@@ -8,10 +8,11 @@
 #include "../STPManager/STPManager.h"
 #include "simplifier.h"
 #include "../AST/NodeFactory/SimplifyingNodeFactory.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
-  class EstablishIntervals
+  class EstablishIntervals : boost::noncopyable
   {
   private:
     struct IntervalType
diff --git a/src/simplifier/FindPureLiterals.h b/src/simplifier/FindPureLiterals.h
index 1036dfc..f060b98 100644
--- a/src/simplifier/FindPureLiterals.h
+++ b/src/simplifier/FindPureLiterals.h
@@ -21,11 +21,12 @@
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
 #include "../simplifier/simplifier.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
 
-class FindPureLiterals
+class FindPureLiterals : boost::noncopyable
 {
   typedef char polarity_type;
   const static polarity_type truePolarity = 1;
diff --git a/src/simplifier/PropagateEqualities.h b/src/simplifier/PropagateEqualities.h
index e8d71fc..a42b393 100644
--- a/src/simplifier/PropagateEqualities.h
+++ b/src/simplifier/PropagateEqualities.h
@@ -4,6 +4,7 @@
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
 #include "../simplifier/simplifier.h"
+#include <boost/utility.hpp>
 
 //This finds conjuncts which are one of: (= SYMBOL BVCONST), (= BVCONST (READ SYMBOL BVCONST)),
 // (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL)
@@ -16,8 +17,9 @@ namespace BEEV
     class Simplifier;
     class ArrayTransformer;
 
-    class PropagateEqualities
+    class PropagateEqualities :  boost::noncopyable
     {
+
         Simplifier *simp;
         NodeFactory *nf;
         STPMgr *bm;
diff --git a/src/simplifier/RemoveUnconstrained.h b/src/simplifier/RemoveUnconstrained.h
index a8856dd..62ec1fc 100644
--- a/src/simplifier/RemoveUnconstrained.h
+++ b/src/simplifier/RemoveUnconstrained.h
@@ -11,12 +11,14 @@
 #include "constantBitP/Dependencies.h"
 #include "simplifier.h"
 #include "MutableASTNode.h"
+#include <boost/utility.hpp>
+
 
 namespace BEEV
 {
   using simplifier::constantBitP::Dependencies;
 
-  class RemoveUnconstrained
+  class RemoveUnconstrained :  boost::noncopyable
   {
     STPMgr& bm;
 
diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index 5ed390a..38618fd 100644
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -10,6 +10,7 @@
 #include "../STPManager/STPManager.h"
 #include "../AST/NodeFactory/SimplifyingNodeFactory.h"
 #include "VariablesInExpression.h"
+#include <boost/utility.hpp>
 
 namespace BEEV {
 
@@ -18,7 +19,8 @@ class ArrayTransformer;
 
 const bool debug_substn = false;
 
-class SubstitutionMap {
+class SubstitutionMap  : boost::noncopyable
+{
 
 	ASTNodeMap * SolverMap;
 	Simplifier *simp;
diff --git a/src/simplifier/Symbols.h b/src/simplifier/Symbols.h
index 851ee63..2da313b 100644
--- a/src/simplifier/Symbols.h
+++ b/src/simplifier/Symbols.h
@@ -1,13 +1,12 @@
 #ifndef SYMBOLS_H
 #define SYMBOLS_H
 
-// Each node is either: empty, an ASTNode, or a vector of more than one child nodes.
+#include <boost/utility.hpp>
 
-class Symbols {
-	private:
-		Symbols& operator =(const Symbols& other); // DO NOT IMPLEMENT
-		Symbols(const Symbols& other); // DO NOT IMPLEMENT
+// Each node is either: empty, an ASTNode, or a vector of more than one child nodes.
 
+class Symbols : boost::noncopyable
+{
 	public:
 
 		const ASTNode found;
diff --git a/src/simplifier/UseITEContext.h b/src/simplifier/UseITEContext.h
index 9c19b14..d74d8b0 100644
--- a/src/simplifier/UseITEContext.h
+++ b/src/simplifier/UseITEContext.h
@@ -13,10 +13,11 @@
 
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
-  class UseITEContext
+  class UseITEContext  : boost::noncopyable
   {
     NodeFactory *nf;
     RunTimes *runtimes;
diff --git a/src/simplifier/VariablesInExpression.h b/src/simplifier/VariablesInExpression.h
index 812dd3c..245e8da 100644
--- a/src/simplifier/VariablesInExpression.h
+++ b/src/simplifier/VariablesInExpression.h
@@ -8,15 +8,14 @@
 
 #include "../AST/AST.h"
 #include "Symbols.h"
-
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
 
-class VariablesInExpression {
+class VariablesInExpression : boost::noncopyable
+{
 private:
-	VariablesInExpression(const VariablesInExpression&);
-	VariablesInExpression& operator=(const VariablesInExpression &);
 
 	void insert(const ASTNode& n, Symbols *s);
 
diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index c547a40..79c5405 100644
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -13,6 +13,7 @@
 #include "simplifier.h"
 #include "Symbols.h"
 #include "VariablesInExpression.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
@@ -40,7 +41,7 @@ namespace BEEV
    * 4. Outside the solver, Substitute and Re-normalize the input DAG
    ******************************************************************/
 
-  class BVSolver
+  class BVSolver  : boost::noncopyable
   {
   private:
     // Ptr to toplevel manager that manages bit-vector expressions
diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index f3e938e..9310d0d 100644
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -14,13 +14,14 @@
 #include "../STPManager/STPManager.h"
 #include "../AST/NodeFactory/SimplifyingNodeFactory.h"
 #include "SubstitutionMap.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
   ASTNode NonMemberBVConstEvaluator(const ASTNode& t);
   ASTNode NonMemberBVConstEvaluator(STPMgr* _bm , const Kind k, const ASTVec& input_children, unsigned int inputwidth);
 
-  class Simplifier
+  class Simplifier  : boost::noncopyable
   {
     friend class counterexample;
   private:
diff --git a/src/to-sat/AIG/BBNodeAIG.h b/src/to-sat/AIG/BBNodeAIG.h
index eacd91f..a00208f 100644
--- a/src/to-sat/AIG/BBNodeAIG.h
+++ b/src/to-sat/AIG/BBNodeAIG.h
@@ -20,7 +20,8 @@ namespace BEEV
 
   // This class wraps around a pointer to an AIG (provided by the ABC tool).
   // uses the default copy constructor and assignment operator.
-class BBNodeAIG
+
+  class BBNodeAIG
 {
   // This is only useful for printing small instances for debuging.
     void print(Aig_Obj_t* node) const
diff --git a/src/to-sat/AIG/ToCNFAIG.h b/src/to-sat/AIG/ToCNFAIG.h
index 5e54365..69cb5cd 100644
--- a/src/to-sat/AIG/ToCNFAIG.h
+++ b/src/to-sat/AIG/ToCNFAIG.h
@@ -6,15 +6,12 @@
 #include "../../extlib-abc/dar.h"
 #include "../ToSATBase.h"
 #include "BBNodeManagerAIG.h"
+#include <boost/utility.hpp>
 
 namespace BEEV {
 
-class ToCNFAIG{
-
-    // no copy. no assignment.
-	ToCNFAIG&  operator = (const ToCNFAIG& other);
-	ToCNFAIG(const ToCNFAIG& other);
-
+class ToCNFAIG : boost::noncopyable
+{
 	UserDefinedFlags& uf;
 
 public:
@@ -23,10 +20,6 @@ public:
 	{
 	}
 
-	~ToCNFAIG()
-	{
-	}
-
 	void toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
 			ToSATBase::ASTNodeToSATVar& nodeToVar,
 			bool needAbsRef,  BBNodeManagerAIG& _mgr);
diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h
index 09b19c9..b7d42df 100644
--- a/src/to-sat/BitBlaster.h
+++ b/src/to-sat/BitBlaster.h
@@ -14,7 +14,7 @@
 #include <cassert>
 #include <map>
 #include "../STPManager/STPManager.h"
-//#include "../STPManager/UserDefinedFlags.h"
+#include <boost/utility.hpp>
 #include <list>
 #include "../simplifier/constantBitP/MultiplicationStats.h"
 
@@ -41,7 +41,7 @@ namespace BEEV
     class BitBlaster;
 
   template<class BBNode, class BBNodeManagerT>
-    class BitBlaster
+    class BitBlaster : boost::noncopyable
     {
       BBNode BBTrue, BBFalse;
 
diff --git a/src/to-sat/ToSATBase.h b/src/to-sat/ToSATBase.h
index d2378be..5cff629 100644
--- a/src/to-sat/ToSATBase.h
+++ b/src/to-sat/ToSATBase.h
@@ -3,10 +3,11 @@
 
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
+#include <boost/utility.hpp>
 
 namespace BEEV
 {
-  class ToSATBase
+  class ToSATBase : boost::noncopyable
   {
   protected:
     ASTNode ASTTrue, ASTFalse, ASTUndefined;