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 93c5bb65f92b90b71b7afbc3562617582e1866ec..8cb41da47c9dc91204b6b88e8eb61e6dc061b567 100644 (file)
--- 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 49762665aa3377de3d2dbc33f2b3b515166b2500..a4e75c6aa3d11efc951a3b7664d7c421f0f1fb15 100644 (file)
--- 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 49537fa084dba3bf10c6de731f899f83c8697308..b4f120ca7ce29c683a9832cb377d964338365843 100644 (file)
--- 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 b647b56433c037802eb0f7fad18b8b9036f32362..93dba29312ef19b5b9d98dfa06d5704d80a7f42a 100644 (file)
--- 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 78f4a2edc2b2a60a69459d2b8d798ed2433840d3..44e93dae6bf2249216531e890fc27eca468f90e5 100644 (file)
--- 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 7c9b7f6662150034fc88925fb589728870e465ad..9d0536e8611cee1bfbbe9b66e36e5d86cdb8cfa7 100644 (file)
--- 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 5c3a8b4be2204e374ab8050a0726d8dd5a0d663a..f95ba0957bafac8edd936062562560dfd00dbfa3 100644 (file)
--- 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 c511b611109d9404ab054416b87f17fcccdeeb23..b7f241f8c778451f3430f01006a8e9e850c62164 100644 (file)
--- 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 c7437fc31836e15e9f2e26e326dd3321a5ddfc3e..d203e0ac551c5be98dc40947d722b4b9eedb37fa 100644 (file)
--- 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 4af2f865a3b9e98f9594e02d717598f837089596..7d9ea6699c83361bd06db35519ab9e24c61c49a4 100644 (file)
--- 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 878e01fc48504778a3d3b3648309576d445512d7..e74df194dd3f7f2fce5f8e437164e1ce81419cfb 100644 (file)
--- 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 bb10cd963432b7ae6f0f47d18403d8c1b1eac292..572d98637be24ac39ab235d6508f6c3ca5a7b1c9 100644 (file)
--- 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 1036dfc0c52f2aa13277e925c2fad220e57a0a91..f060b9819daaabc484f25b459d8e605bd5b6e24a 100644 (file)
--- 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 e8d71fc994463d529b7e625c0d3ccf1473b0170e..a42b39332411213f9a1290750fc23b3c52f7f224 100644 (file)
--- 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 a8856ddb0264febb58fa9b9b5fceffa2fd0641d5..62ec1fc15c0c4ff2cef16660b7e1ae8b737ca7e6 100644 (file)
--- 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 5ed390a0f8741651e0c5c46a2ecbb62955d1eb64..38618fd5c25a67fe5e2b23e6a16fa26531cf3b9c 100644 (file)
--- 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 851ee63581f1ab1ab35689c685fdfe6b6dd2d830..2da313be8c1f19399ca932d18793b8c3c61664ca 100644 (file)
--- 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 9c19b147cb081545bc2357dfbe5dc9ad79433789..d74d8b08b6f1c48bb6ab4cb3d7354cb257687491 100644 (file)
--- 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 812dd3c6880e1b3cf16e6060339592cb3f96f3d8..245e8da0605252bb87a16a30668cffc5c59bdad9 100644 (file)
--- 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 c547a400295bda48485202b8a8c06c91ad6753d7..79c54056d7441107ef2830f71a27eb51f38f44d9 100644 (file)
--- 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 f3e938efc93744002fd18d0d2c82e2506d1dc455..9310d0dd2593aeb7eb98525e888787b2fb74562c 100644 (file)
--- 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 eacd91f476ad9705d27b476339b5c1e46bb2c3ac..a00208f6d62cecf3513ca0ac42d964e984b419f2 100644 (file)
--- 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 5e54365ea8953ff92bfd9e06dcf260a5c870454b..69cb5cd34cf3cd0de2b6d9b07dddb675b49d1678 100644 (file)
--- 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 09b19c929ce57f9a79d0b7f1cfc6eab491b359e1..b7d42df3754bccb9bce444d52bac470fafdc58f0 100644 (file)
--- 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 d2378bee39472b662f71ad08d0a6d4cf0f8f21a6..5cff629cc9501f733dd6017ebe175594c01d81d9 100644 (file)
--- 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;