From 280911ddcc4967d8a8f0fc99e0327f9391265ae6 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 12 Jul 2011 05:09:42 +0000 Subject: [PATCH] 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 --- src/sat/mtl/Vec.h | 2 +- src/simplifier/RemoveUnconstrained.cpp | 2 +- src/simplifier/Symbols.h | 4 +-- src/to-sat/BitBlaster.cpp | 38 +++++++++++++------------- src/to-sat/BitBlaster.h | 4 +-- 5 files changed, 25 insertions(+), 25 deletions(-) diff --git a/src/sat/mtl/Vec.h b/src/sat/mtl/Vec.h index fac0a0d..9974481 100644 --- a/src/sat/mtl/Vec.h +++ b/src/sat/mtl/Vec.h @@ -96,7 +96,7 @@ template void vec::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 1f28629..824966e 100644 --- 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 toVar(size); // Create a mutable copy that we can iterate over. vector mut; diff --git a/src/simplifier/Symbols.h b/src/simplifier/Symbols.h index adc0e2e..851ee63 100644 --- 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 cfcf304..2045716 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -644,14 +644,14 @@ const BBNodeVec BitBlaster::BBTerm(const ASTNode& _term, results.push_back(BBTerm(term[i], support)); const int bitWidth = term[0].GetValueWidth(); - stack products[bitWidth]; + std::vector > 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::buildAdditionNetworkResult(stack void BitBlaster::buildAdditionNetworkResult(stack* products, set& 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::mult_normal(const BBNodeVec& x, void BitBlaster::mult_SortingNetwork( BBNodeSet& support, stack& current, vector& currentSorted, vector& 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::BBMult(const BBNodeVec& _x, const B string mv = uf->get("multiplication_variant","3"); const int bitWidth = x.size(); - stack products[bitWidth]; + std::vector > products(bitWidth); if (mv == "1") { //cerr << "v1"; @@ -1611,19 +1611,19 @@ BBNodeVec BitBlaster::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 prior; for (int i = 0; i < bitWidth; i++) @@ -1633,19 +1633,19 @@ BBNodeVec BitBlaster::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::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; -template class BitBlaster; - 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; +template class BitBlaster; + #undef BBNodeVec #undef BBNodeVecMap #undef BBNodeSet diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index 18eb476..d9ffa24 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -83,9 +83,9 @@ class BitBlaster { void mult_SortingNetwork( set& support, stack& currentColumn, vector& currentSorted, vector& priorSorted, - const int minTrue , const int maxTrue ); + const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 ); - void buildAdditionNetworkResult(stack* products, set& support, const int bitWidth, const int index, const int minTrue, const int maxTrue ); + void buildAdditionNetworkResult(stack* products, set& support, const int bitWidth, const int index, const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 ); vector buildAdditionNetworkResult(stack* products, set& support, int bitWidth); vector BBAndBit(const vector& y, BBNode b); -- 2.47.3