Patch from Peter Collingbourne to enable compiling with clang. Thanks\!

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

diff --git a/src/sat/mtl/Vec.h b/src/sat/mtl/Vec.h
index fac0a0d83181a02e6d7daccb6e6743bfaa2e3992..9974481e3daf4171708e4fd31fc302125ef2d73c 100644 (file)
--- a/src/sat/mtl/Vec.h
+++ b/src/sat/mtl/Vec.h
@@ -96,7 +96,7 @@ template<class T>
 void vec<T>::capacity(int min_cap) {
     if (cap >= min_cap) return;
     int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1);   // NOTE: grow by approximately 3/2
-    if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
+    if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
         throw OutOfMemoryException();
  }
 

diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp
index 1f2862967eaffa2fffa096a01ba4724ee26e5dfe..824966efd3fda7e97eaf8a566fd720926318e839 100644 (file)
--- a/src/simplifier/RemoveUnconstrained.cpp
+++ b/src/simplifier/RemoveUnconstrained.cpp
@@ -110,7 +110,7 @@ namespace BEEV
         ASTNode& var = extracts[i]->n;
         assert(var.GetKind() == SYMBOL);
         const int size = var.GetValueWidth();
-        ASTNode toVar[size];
+        std::vector<ASTNode> toVar(size);
 
         // Create a mutable copy that we can iterate over.
         vector <MutableASTNode*> mut;

diff --git a/src/simplifier/Symbols.h b/src/simplifier/Symbols.h
index adc0e2ea3fb16bc10ea184ad9d8a8441b14bca1c..851ee63581f1ab1ab35689c685fdfe6b6dd2d830 100644 (file)
--- a/src/simplifier/Symbols.h
+++ b/src/simplifier/Symbols.h
@@ -5,8 +5,8 @@
 
 class Symbols {
        private:
-               Symbols& operator =(const Symbols& other) { /*..*/}
-               Symbols(const Symbols& other) {/*..*/}
+               Symbols& operator =(const Symbols& other); // DO NOT IMPLEMENT
+               Symbols(const Symbols& other); // DO NOT IMPLEMENT
 
        public:
 

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index cfcf304eea10768f4a61955c1e2a57139edd93b4..2045716999f1b3e911acbe7d257e1ed1f6c18dff 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -644,14 +644,14 @@ const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& _term,
                        results.push_back(BBTerm(term[i], support));
 
                      const int bitWidth = term[0].GetValueWidth();
-                     stack<BBNode> products[bitWidth];
+                     std::vector<stack<BBNode> > products(bitWidth);
                      for (int i=0; i < bitWidth;i++)
                        {
                          for (int j=0; j < results.size();j++)
                            products[i].push(results[j][i]);
                        }
 
-                     result = buildAdditionNetworkResult(products,support,bitWidth);
+                     result = buildAdditionNetworkResult(products.data(),support,bitWidth);
                    }
                 break;
        }
@@ -1164,7 +1164,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BB
 // partial products.
 template <class BBNode, class BBNodeManagerT>
 void BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BBNode>* products, set<BBNode>& support,
-               const int bitWidth, const int i, const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 )
+               const int bitWidth, const int i, const int minTrue, const int maxTrue )
 {
       while (products[i].size() >= 2) {
               BBNode c;
@@ -1477,7 +1477,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::mult_normal(const BBNodeVec& x,
     void
     BitBlaster<BBNode, BBNodeManagerT>::mult_SortingNetwork(
         BBNodeSet& support, stack<BBNode>& current, vector<BBNode>& currentSorted, vector<BBNode>& priorSorted,
-        const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 )
+        const int minTrue, const int maxTrue )
     {
 
       // Add the carry from the prior column. i.e. each second sorted formula.
@@ -1603,7 +1603,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBMult(const BBNodeVec& _x, const B
          string mv = uf->get("multiplication_variant","3");
 
       const int bitWidth = x.size();
-      stack<BBNode> products[bitWidth];
+      std::vector<stack<BBNode> > products(bitWidth);
 
       if (mv == "1") {
               //cerr << "v1";
@@ -1611,19 +1611,19 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBMult(const BBNodeVec& _x, const B
       }
       else   if (mv == "2") {
               //cout << "v2";
-              mult_allPairs(x, y, support,products);
-              return buildAdditionNetworkResult(products,support, bitWidth);
+              mult_allPairs(x, y, support,products.data());
+              return buildAdditionNetworkResult(products.data(),support, bitWidth);
       }
 
       else   if (mv == "3") {
               //cout << "v3" << endl;
-              mult_Booth(_x, _y, support,n[0],n[1],products);
-              return buildAdditionNetworkResult(products,support,bitWidth);
+              mult_Booth(_x, _y, support,n[0],n[1],products.data());
+              return buildAdditionNetworkResult(products.data(),support,bitWidth);
       }
       else   if (mv == "4")
       {
         //cerr << "v4";
-        mult_Booth(_x, _y, support,n[0],n[1],products);
+        mult_Booth(_x, _y, support,n[0],n[1],products.data());
         vector<BBNode> prior;
 
         for (int i = 0; i < bitWidth; i++)
@@ -1633,19 +1633,19 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBMult(const BBNodeVec& _x, const B
               prior = output;
               assert(products[i].size() == 1);
           }
-        return buildAdditionNetworkResult(products,support, bitWidth);
+        return buildAdditionNetworkResult(products.data(),support, bitWidth);
       }
       else   if (mv == "5")
         {
         //cout << "v5";
           if (!statsFound(n))
             {
-              mult_Booth(_x, _y, support, n[0], n[1], products);
-              return buildAdditionNetworkResult(products, support, bitWidth);
+              mult_Booth(_x, _y, support, n[0], n[1], products.data());
+              return buildAdditionNetworkResult(products.data(), support, bitWidth);
             }
 
-          mult_allPairs(x, y, support, products);
-          return multWithBounds(n, products, support);
+          mult_allPairs(x, y, support, products.data());
+          return multWithBounds(n, products.data(), support);
         }
       else
          FatalError("sda44f");
@@ -2045,16 +2045,16 @@ BBNode BitBlaster<BBNode,BBNodeManagerT>::BBEQ(const BBNodeVec& left, const BBNo
                return nf->CreateNode(IFF, *lit, *rit);
 }
 
-// This creates all the specialisations of the class that are ever needed.
-template class BitBlaster<ASTNode, BBNodeManagerASTNode>;
-template class BitBlaster<BBNodeAIG, BBNodeManagerAIG>;
-
 std::ostream& operator<<(std::ostream& output, const BBNodeAIG& h)
 {
   FatalError("This isn't implemented  yet sorry;");
   return output;
 }
 
+// This creates all the specialisations of the class that are ever needed.
+template class BitBlaster<ASTNode, BBNodeManagerASTNode>;
+template class BitBlaster<BBNodeAIG, BBNodeManagerAIG>;
+
 #undef BBNodeVec
 #undef BBNodeVecMap
 #undef BBNodeSet

diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h
index 18eb47662c7c0d99eb3204aa814e19ae42e386cd..d9ffa243587c953ab771dbf50fc9d973ade42f70 100644 (file)
--- a/src/to-sat/BitBlaster.h
+++ b/src/to-sat/BitBlaster.h
@@ -83,9 +83,9 @@ class BitBlaster {
         void
         mult_SortingNetwork(
             set<BBNode>& support, stack<BBNode>& currentColumn, vector<BBNode>& currentSorted, vector<BBNode>& priorSorted,
-                const int minTrue , const int maxTrue  );
+                const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 );
 
-       void buildAdditionNetworkResult(stack<BBNode>* products, set<BBNode>& support, const int bitWidth, const int index, const int minTrue, const int maxTrue );
+       void buildAdditionNetworkResult(stack<BBNode>* products, set<BBNode>& support, const int bitWidth, const int index, const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 );
        vector<BBNode> buildAdditionNetworkResult(stack<BBNode>* products, set<BBNode>& support, int bitWidth);
 
        vector<BBNode> BBAndBit(const vector<BBNode>& y, BBNode b);