Fix. Thanks to Stephan Falke. Last checkin put a dependency on boost being installed...

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

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index 8cb41da47c9dc91204b6b88e8eb61e6dc061b567..40930c05ae1d64ff648a0ae1e3048cb58b0756e6 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -13,7 +13,7 @@
 #include "AST.h"
 #include "../STPManager/STPManager.h"
 #include "../AST/NodeFactory/SimplifyingNodeFactory.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/AST/NodeFactory/NodeFactory.cpp b/src/AST/NodeFactory/NodeFactory.cpp
index 9930c7a6a4e3ebb19caba6d81fc1f026895aefa5..4d8f4d7d9d77e7a810217e90e13edbd5f9ec1929 100644 (file)
--- a/src/AST/NodeFactory/NodeFactory.cpp
+++ b/src/AST/NodeFactory/NodeFactory.cpp
@@ -69,6 +69,16 @@ ASTNode NodeFactory::CreateNode(Kind kind, const ASTNode& child0,
        return CreateNode(kind, front_children);
 }
 
+ASTNode NodeFactory::CreateNodeY(Kind kind, const ASTNode& child0,
+                const ASTNode& child1)
+{
+        ASTVec front_children;
+        front_children.push_back(child0);
+        front_children.push_back(child1);
+        return CreateNode(kind, front_children);
+}
+
+
 ASTNode NodeFactory::CreateNode(Kind kind, const ASTNode& child0,
                const ASTNode& child1, const ASTNode& child2,
                const ASTVec & back_children)

diff --git a/src/AST/NodeFactory/NodeFactory.h b/src/AST/NodeFactory/NodeFactory.h
index a4e75c6aa3d11efc951a3b7664d7c421f0f1fb15..e683149f4c59569ccbf068b5108eebf345f32c1a 100644 (file)
--- a/src/AST/NodeFactory/NodeFactory.h
+++ b/src/AST/NodeFactory/NodeFactory.h
@@ -4,7 +4,7 @@
 
 #include <vector>
 #include "../ASTKind.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index b4f120ca7ce29c683a9832cb377d964338365843..f606da6639901769987da4df2492629a3409cf43 100644 (file)
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -15,7 +15,7 @@
 #include <string>
 #include "../sat/utils/System.h"
 #include <iomanip>
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 class RunTimes : boost::noncopyable
 {

diff --git a/src/STPManager/DifficultyScore.h b/src/STPManager/DifficultyScore.h
index 93dba29312ef19b5b9d98dfa06d5704d80a7f42a..f3b238c9c08174f6ce6fdc84e6e38c4ba74b97a9 100644 (file)
--- a/src/STPManager/DifficultyScore.h
+++ b/src/STPManager/DifficultyScore.h
@@ -6,7 +6,7 @@
 #include "../AST/ASTKind.h"
 #include <list>
 #include "../STPManager/NodeIterator.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 // estimate how difficult that input is to solve based on some simple rules.
 

diff --git a/src/STPManager/NodeIterator.h b/src/STPManager/NodeIterator.h
index 44e93dae6bf2249216531e890fc27eca468f90e5..eeb958b56d7526d7835db0441c036883bd3ca107 100644 (file)
--- a/src/STPManager/NodeIterator.h
+++ b/src/STPManager/NodeIterator.h
@@ -2,7 +2,7 @@
 #define NODEITERATOR_H_
 
 #include <stack>
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 9d0536e8611cee1bfbbe9b66e36e5d86cdb8cfa7..cb52d30aae4e70591a31593dfe54143044c89c4a 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -19,7 +19,7 @@
 #include "../parser/LetMgr.h"
 #include "../absrefine_counterexample/AbsRefine_CounterExample.h"
 #include "../simplifier/PropagateEqualities.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index f95ba0957bafac8edd936062562560dfd00dbfa3..8542ad00380452f736ec47ca966e99daee68fc79 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -14,7 +14,7 @@
 #include "../AST/AST.h"
 #include "../AST/NodeFactory/HashingNodeFactory.h"
 #include "../sat/SATSolver.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index b7f241f8c778451f3430f01006a8e9e850c62164..d817deecb3570bcedad6b1aaed4235f6383dee1a 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -14,7 +14,7 @@
 #include <assert.h>
 #include <iostream>
 #include <set>
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index d203e0ac551c5be98dc40947d722b4b9eedb37fa..f442c33bc35d7d8d04369c7083ee48aef672a936 100644 (file)
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -15,7 +15,7 @@
 #include "../simplifier/simplifier.h"
 #include "../AST/ArrayTransformer.h"
 #include "../to-sat/ToSATBase.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/boost/noncopyable.hpp b/src/boost/noncopyable.hpp
new file mode 100644 (file)
index 0000000..7770bdb
--- /dev/null
+++ b/src/boost/noncopyable.hpp
@@ -0,0 +1,36 @@
+//  Boost noncopyable.hpp header file  --------------------------------------//
+
+//  (C) Copyright Beman Dawes 1999-2003. Distributed under the Boost
+//  Software License, Version 1.0. (See accompanying file
+//  LICENSE_1_0.txt or copy at http://www.boost.org/LICENSE_1_0.txt)
+
+//  See http://www.boost.org/libs/utility for documentation.
+
+#ifndef BOOST_NONCOPYABLE_HPP_INCLUDED
+#define BOOST_NONCOPYABLE_HPP_INCLUDED
+
+namespace boost {
+
+//  Private copy constructor and copy assignment ensure classes derived from
+//  class noncopyable cannot be copied.
+
+//  Contributed by Dave Abrahams
+
+namespace noncopyable_  // protection from unintended ADL
+{
+  class noncopyable
+  {
+   protected:
+      noncopyable() {}
+      ~noncopyable() {}
+   private:  // emphasize the following members are private
+      noncopyable( const noncopyable& );
+      const noncopyable& operator=( const noncopyable& );
+  };
+}
+
+typedef noncopyable_::noncopyable noncopyable;
+
+} // namespace boost
+
+#endif  // BOOST_NONCOPYABLE_HPP_INCLUDED

diff --git a/src/simplifier/AIGSimplifyPropositionalCore.h b/src/simplifier/AIGSimplifyPropositionalCore.h
index 7d9ea6699c83361bd06db35519ab9e24c61c49a4..99b9dddb631a1626cc258b883d45fa10442d3fa2 100644 (file)
--- a/src/simplifier/AIGSimplifyPropositionalCore.h
+++ b/src/simplifier/AIGSimplifyPropositionalCore.h
@@ -18,7 +18,7 @@
 #include "../extlib-abc/dar.h"
 #include "../to-sat/AIG/BBNodeManagerAIG.h"
 #include "../to-sat/BitBlaster.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/simplifier/AlwaysTrue.h b/src/simplifier/AlwaysTrue.h
index e74df194dd3f7f2fce5f8e437164e1ce81419cfb..b5653247277f99c286f0b917c4c955229473f64a 100644 (file)
--- a/src/simplifier/AlwaysTrue.h
+++ b/src/simplifier/AlwaysTrue.h
@@ -7,7 +7,7 @@
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
 #include "../simplifier/simplifier.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h
index 572d98637be24ac39ab235d6508f6c3ca5a7b1c9..8e7a5f3ff3abc8dd73371a6f741b9afa8044baeb 100644 (file)
--- a/src/simplifier/EstablishIntervals.h
+++ b/src/simplifier/EstablishIntervals.h
@@ -8,7 +8,7 @@
 #include "../STPManager/STPManager.h"
 #include "simplifier.h"
 #include "../AST/NodeFactory/SimplifyingNodeFactory.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/simplifier/FindPureLiterals.h b/src/simplifier/FindPureLiterals.h
index f060b9819daaabc484f25b459d8e605bd5b6e24a..d6a4a46434b9300217ce262f2ad3343a9b7dfef4 100644 (file)
--- a/src/simplifier/FindPureLiterals.h
+++ b/src/simplifier/FindPureLiterals.h
@@ -21,7 +21,7 @@
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
 #include "../simplifier/simplifier.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/simplifier/PropagateEqualities.h b/src/simplifier/PropagateEqualities.h
index a42b39332411213f9a1290750fc23b3c52f7f224..1fcf6d3e429bf8b0b87e5c751453b209104d4665 100644 (file)
--- a/src/simplifier/PropagateEqualities.h
+++ b/src/simplifier/PropagateEqualities.h
@@ -4,7 +4,7 @@
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
 #include "../simplifier/simplifier.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.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)

diff --git a/src/simplifier/RemoveUnconstrained.h b/src/simplifier/RemoveUnconstrained.h
index 62ec1fc15c0c4ff2cef16660b7e1ae8b737ca7e6..34f0961f7396c76007eee9ec2148212ed032b880 100644 (file)
--- a/src/simplifier/RemoveUnconstrained.h
+++ b/src/simplifier/RemoveUnconstrained.h
@@ -11,7 +11,7 @@
 #include "constantBitP/Dependencies.h"
 #include "simplifier.h"
 #include "MutableASTNode.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 
 namespace BEEV

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index 38618fd5c25a67fe5e2b23e6a16fa26531cf3b9c..064fe918b9aadf965ecdb83562b371a588924291 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -10,7 +10,7 @@
 #include "../STPManager/STPManager.h"
 #include "../AST/NodeFactory/SimplifyingNodeFactory.h"
 #include "VariablesInExpression.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV {
 

diff --git a/src/simplifier/Symbols.h b/src/simplifier/Symbols.h
index 2da313be8c1f19399ca932d18793b8c3c61664ca..c520925c9d3e5f97d946b3ecc7a8516a48edcba1 100644 (file)
--- a/src/simplifier/Symbols.h
+++ b/src/simplifier/Symbols.h
@@ -1,7 +1,7 @@
 #ifndef SYMBOLS_H
 #define SYMBOLS_H
 
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 // Each node is either: empty, an ASTNode, or a vector of more than one child nodes.
 

diff --git a/src/simplifier/UseITEContext.h b/src/simplifier/UseITEContext.h
index d74d8b08b6f1c48bb6ab4cb3d7354cb257687491..2769681b728dd1266492140fb0e5a1d8239a25be 100644 (file)
--- a/src/simplifier/UseITEContext.h
+++ b/src/simplifier/UseITEContext.h
@@ -13,7 +13,7 @@
 
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/simplifier/VariablesInExpression.h b/src/simplifier/VariablesInExpression.h
index 245e8da0605252bb87a16a30668cffc5c59bdad9..3373c5afefe961a8f0411b71ef378661fe38dafe 100644 (file)
--- a/src/simplifier/VariablesInExpression.h
+++ b/src/simplifier/VariablesInExpression.h
@@ -8,7 +8,7 @@
 
 #include "../AST/AST.h"
 #include "Symbols.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 79c54056d7441107ef2830f71a27eb51f38f44d9..5b250b6d78fe7307bfb731f79cd54fac2ae54f3d 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -13,7 +13,7 @@
 #include "simplifier.h"
 #include "Symbols.h"
 #include "VariablesInExpression.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 9310d0dd2593aeb7eb98525e888787b2fb74562c..cc3f864b90be72426b7ac1cf3ee67f015d16130f 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -14,7 +14,7 @@
 #include "../STPManager/STPManager.h"
 #include "../AST/NodeFactory/SimplifyingNodeFactory.h"
 #include "SubstitutionMap.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {

diff --git a/src/to-sat/AIG/ToCNFAIG.h b/src/to-sat/AIG/ToCNFAIG.h
index 69cb5cd34cf3cd0de2b6d9b07dddb675b49d1678..d7310a9a8f71fb049e753b359bb2f518cb05ec57 100644 (file)
--- a/src/to-sat/AIG/ToCNFAIG.h
+++ b/src/to-sat/AIG/ToCNFAIG.h
@@ -6,7 +6,7 @@
 #include "../../extlib-abc/dar.h"
 #include "../ToSATBase.h"
 #include "BBNodeManagerAIG.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV {
 

diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h
index b7d42df3754bccb9bce444d52bac470fafdc58f0..50058c607f2b796142d46b13ff55aa39392a9752 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 <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 #include <list>
 #include "../simplifier/constantBitP/MultiplicationStats.h"
 

diff --git a/src/to-sat/ToSATBase.h b/src/to-sat/ToSATBase.h
index 5cff629cc9501f733dd6017ebe175594c01d81d9..19ad15e80c6d57a48a90f875a046d9bf1ef5d809 100644 (file)
--- a/src/to-sat/ToSATBase.h
+++ b/src/to-sat/ToSATBase.h
@@ -3,7 +3,7 @@
 
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
-#include <boost/utility.hpp>
+#include "../boost/noncopyable.hpp"
 
 namespace BEEV
 {