From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 23 Jan 2012 12:43:59 +0000 (+0000)
Subject: Fix. Thanks to Stephan Falke. Last checkin put a dependency on boost being installed... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=fe053a7f83c35f6ee8441101f211c69832423236;p=francis%2Fstp.git

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

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 8cb41da..40930c0 100644
--- 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 9930c7a..4d8f4d7 100644
--- 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 a4e75c6..e683149 100644
--- 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 b4f120c..f606da6 100644
--- 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 93dba29..f3b238c 100644
--- 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 44e93da..eeb958b 100644
--- 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 9d0536e..cb52d30 100644
--- 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 f95ba09..8542ad0 100644
--- 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 b7f241f..d817dee 100644
--- 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 d203e0a..f442c33 100644
--- 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
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 7d9ea66..99b9ddd 100644
--- 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 e74df19..b565324 100644
--- 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 572d986..8e7a5f3 100644
--- 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 f060b98..d6a4a46 100644
--- 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 a42b393..1fcf6d3 100644
--- 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 62ec1fc..34f0961 100644
--- 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 38618fd..064fe91 100644
--- 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 2da313b..c520925 100644
--- 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 d74d8b0..2769681 100644
--- 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 245e8da..3373c5a 100644
--- 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 79c5405..5b250b6 100644
--- 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 9310d0d..cc3f864 100644
--- 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 69cb5cd..d7310a9 100644
--- 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 b7d42df..50058c6 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 <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 5cff629..19ad15e 100644
--- 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
 {