diff --git a/sources b/sources index 7ed9a01..8052399 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -e23ce5a6ef6cc34ce289c2d4eb948efe stp-0.1.tar.xz +23ee46548b338443fd741ba2e50000e3 stp-0.1.tar.xz diff --git a/stp-gcc47.patch b/stp-gcc47.patch deleted file mode 100644 index f522a00..0000000 --- a/stp-gcc47.patch +++ /dev/null @@ -1,25 +0,0 @@ ---- ./src/sat/mtl/Map.h.orig 2010-11-27 19:45:43.000000000 -0700 -+++ ./src/sat/mtl/Map.h 2012-01-10 16:30:55.918767977 -0700 -@@ -29,17 +29,17 @@ namespace Minisat { - // Default hash/equals functions - // - -+static inline uint32_t hash(uint32_t x){ return x; } -+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; } -+static inline uint32_t hash(int32_t x) { return (uint32_t)x; } -+static inline uint32_t hash(int64_t x) { return (uint32_t)x; } -+ - template struct Hash { uint32_t operator()(const K& k) const { return hash(k); } }; - template struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } }; - - template struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } }; - template struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } }; - --static inline uint32_t hash(uint32_t x){ return x; } --static inline uint32_t hash(uint64_t x){ return (uint32_t)x; } --static inline uint32_t hash(int32_t x) { return (uint32_t)x; } --static inline uint32_t hash(int64_t x) { return (uint32_t)x; } -- - - //================================================================================================= - // Some primes diff --git a/stp-unbundle.patch b/stp-unbundle.patch new file mode 100644 index 0000000..5a34543 --- /dev/null +++ b/stp-unbundle.patch @@ -0,0 +1,394 @@ +--- ./src/to-sat/ToSATBase.h.orig 2012-01-23 05:43:59.000000000 -0700 ++++ ./src/to-sat/ToSATBase.h 2012-08-07 16:22:05.823811600 -0600 +@@ -3,7 +3,7 @@ + + #include "../AST/AST.h" + #include "../STPManager/STPManager.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/to-sat/AIG/ToCNFAIG.h.orig 2012-01-23 15:51:23.000000000 -0700 ++++ ./src/to-sat/AIG/ToCNFAIG.h 2012-08-07 16:22:05.823811600 -0600 +@@ -6,7 +6,7 @@ + #include "../../extlib-abc/dar.h" + #include "../ToSATBase.h" + #include "BBNodeManagerAIG.h" +-#include "../../boost/noncopyable.hpp" ++#include + + namespace BEEV { + +--- ./src/to-sat/ASTNode/ToCNF.h.orig 2012-01-27 21:08:17.000000000 -0700 ++++ ./src/to-sat/ASTNode/ToCNF.h 2012-08-07 16:22:05.823811600 -0600 +@@ -15,7 +15,7 @@ + #include "../../AST/AST.h" + #include "../../STPManager/STPManager.h" + #include "ClauseList.h" +-#include "../../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/to-sat/BitBlaster.h.orig 2012-04-09 07:21:26.000000000 -0600 ++++ ./src/to-sat/BitBlaster.h 2012-08-07 16:22:05.824811583 -0600 +@@ -14,7 +14,7 @@ + #include + #include + #include "../STPManager/STPManager.h" +-#include "../boost/noncopyable.hpp" ++#include + #include + #include "../simplifier/constantBitP/MultiplicationStats.h" + +--- ./src/absrefine_counterexample/AbsRefine_CounterExample.h.orig 2012-04-25 07:40:33.000000000 -0600 ++++ ./src/absrefine_counterexample/AbsRefine_CounterExample.h 2012-08-07 16:22:05.825811565 -0600 +@@ -15,7 +15,7 @@ + #include "../simplifier/simplifier.h" + #include "../AST/ArrayTransformer.h" + #include "../to-sat/ToSATBase.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/sat/CryptoMinisat.cpp.orig 2010-08-20 06:07:42.000000000 -0600 ++++ ./src/sat/CryptoMinisat.cpp 2012-08-07 16:22:39.477306573 -0600 +@@ -7,15 +7,25 @@ + #undef l_Undef + + +-#include "cryptominisat2/Solver.h" +-#include "cryptominisat2/SolverTypes.h" ++#include + + namespace BEEV + { ++ class CryptoMinisatSolver : public CMSat::Solver ++ { ++ public: ++ uint64_t getConflicts() const { return conflicts; } ++ uint64_t getDecisions() const { return decisions; } ++ uint64_t getMaxLiterals() const { return max_literals; } ++ uint64_t getPropagations() const { return propagations; } ++ uint64_t getRndDecisions() const { return rnd_decisions; } ++ uint64_t getStarts() const { return starts; } ++ uint64_t getTotLiterals() const { return tot_literals; } ++ }; + + CryptoMinisat::CryptoMinisat() + { +- s = new MINISAT::Solver(); ++ s = new CryptoMinisatSolver(); + } + + CryptoMinisat::~CryptoMinisat() +@@ -30,9 +40,9 @@ namespace BEEV + // Cryptominisat uses a slightly different Lit class too. + + // VERY SLOW> +- MINISAT::vec v; ++ CMSat::vec v; + for (int i =0; iaddClause(v); + } +@@ -63,7 +73,7 @@ namespace BEEV + + int CryptoMinisat::setVerbosity(int v) + { +- s->verbosity = v; ++ s->conf.verbosity = v; + } + + int CryptoMinisat::nVars() +@@ -73,11 +83,11 @@ namespace BEEV + { + double cpu_time = Minisat::cpuTime(); + double mem_used = Minisat::memUsedPeak(); +- printf("restarts : %"PRIu64"\n", s->starts); +- printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", s->conflicts , s->conflicts /cpu_time); +- printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", s->decisions, (float)s->rnd_decisions*100 / (float)s->decisions, s->decisions /cpu_time); +- printf("propagations : %-12"PRIu64" (%.0f /sec)\n", s->propagations, s->propagations/cpu_time); +- printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", s->tot_literals, (s->max_literals - s->tot_literals)*100 / (double)s->max_literals); ++ printf("restarts : %"PRIu64"\n", s->getStarts()); ++ printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", s->getConflicts(), s->getConflicts()/cpu_time); ++ printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", s->getDecisions(), (float)s->getRndDecisions()*100 / (float)s->getDecisions(), s->getDecisions()/cpu_time); ++ printf("propagations : %-12"PRIu64" (%.0f /sec)\n", s->getPropagations(), s->getPropagations()/cpu_time); ++ printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", s->getTotLiterals(), (s->getMaxLiterals() - s->getTotLiterals())*100 / (double)s->getMaxLiterals()); + if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); + printf("CPU time : %g s\n", cpu_time); + } +--- ./src/sat/Makefile.orig 2011-11-27 19:55:18.000000000 -0700 ++++ ./src/sat/Makefile 2012-08-07 16:22:05.826811547 -0600 +@@ -13,7 +13,7 @@ export COPTIMIZE=$(CFLAGS_M32) $(CFLAGS_ + core: $(LIB) + + # $(LIB) depends on */lib_release.a and will be rebuilt only if they have been updated +-$(LIB): core/lib_release.a core_prop/lib_release.a simp/lib_release.a utils/lib_release.a cryptominisat2/libminisat.a $(OBJS) ++$(LIB): core/lib_release.a core_prop/lib_release.a simp/lib_release.a utils/lib_release.a $(OBJS) + $(RM) $@ + $(call arcat,$@,$(filter %.a,$^)) + $(AR) qcs $@ $(filter %.o,$^) +@@ -26,8 +26,6 @@ simp/lib_release.a: FORCE + $(MAKE) -C simp libr + utils/lib_release.a: FORCE + $(MAKE) -C utils libr +-cryptominisat2/libminisat.a: FORCE +- $(MAKE) -C cryptominisat2 lib all + FORCE: + + .PHONY: clean +@@ -37,6 +35,5 @@ clean: + $(MAKE) -C core_prop clean + $(MAKE) -C simp clean + $(MAKE) -C utils clean +- $(MAKE) -C cryptominisat2 clean + +-CryptoMinisat.o: CFLAGS += -Icryptominisat2/mtl -Imtl -I$(TOP)/src ++CryptoMinisat.o: CFLAGS += -I/usr/include/cmsat/mtl -Imtl -I$(TOP)/src +--- ./src/sat/CryptoMinisat.h.orig 2012-01-09 21:59:09.000000000 -0700 ++++ ./src/sat/CryptoMinisat.h 2012-08-07 16:22:05.826811547 -0600 +@@ -6,16 +6,13 @@ + + #include "SATSolver.h" + +-namespace MINISAT +-{ +- class Solver; +-} +- + namespace BEEV + { ++ class CryptoMinisatSolver; ++ + class CryptoMinisat : public SATSolver + { +- MINISAT::Solver* s; ++ CryptoMinisatSolver* s; + + public: + CryptoMinisat(); +--- ./src/STPManager/STP.h.orig 2012-03-15 06:38:21.000000000 -0600 ++++ ./src/STPManager/STP.h 2012-08-07 16:22:05.827811530 -0600 +@@ -19,7 +19,7 @@ + #include "../parser/LetMgr.h" + #include "../absrefine_counterexample/AbsRefine_CounterExample.h" + #include "../simplifier/PropagateEqualities.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/STPManager/NodeIterator.h.orig 2012-01-23 05:43:59.000000000 -0700 ++++ ./src/STPManager/NodeIterator.h 2012-08-07 16:22:05.827811530 -0600 +@@ -2,7 +2,7 @@ + #define NODEITERATOR_H_ + + #include +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/STPManager/UserDefinedFlags.h.orig 2012-04-06 18:20:57.000000000 -0600 ++++ ./src/STPManager/UserDefinedFlags.h 2012-08-07 16:22:05.827811530 -0600 +@@ -14,7 +14,7 @@ + #include + #include + #include +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/STPManager/STPManager.h.orig 2012-01-25 22:04:55.000000000 -0700 ++++ ./src/STPManager/STPManager.h 2012-08-07 16:22:05.828811513 -0600 +@@ -14,7 +14,7 @@ + #include "../AST/AST.h" + #include "../AST/NodeFactory/HashingNodeFactory.h" + #include "../sat/SATSolver.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/STPManager/DifficultyScore.h.orig 2012-01-23 05:43:59.000000000 -0700 ++++ ./src/STPManager/DifficultyScore.h 2012-08-07 16:22:05.828811513 -0600 +@@ -6,7 +6,7 @@ + #include "../AST/ASTKind.h" + #include + #include "../STPManager/NodeIterator.h" +-#include "../boost/noncopyable.hpp" ++#include + + // estimate how difficult that input is to solve based on some simple rules. + +--- ./src/simplifier/SubstitutionMap.h.orig 2012-03-19 21:59:03.000000000 -0600 ++++ ./src/simplifier/SubstitutionMap.h 2012-08-07 16:22:05.829811496 -0600 +@@ -5,7 +5,7 @@ + #include "../STPManager/STPManager.h" + #include "../AST/NodeFactory/SimplifyingNodeFactory.h" + #include "VariablesInExpression.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/simplifier/simplifier.h.orig 2012-03-19 21:59:03.000000000 -0600 ++++ ./src/simplifier/simplifier.h 2012-08-07 16:22:05.829811496 -0600 +@@ -14,7 +14,7 @@ + #include "../STPManager/STPManager.h" + #include "../AST/NodeFactory/SimplifyingNodeFactory.h" + #include "SubstitutionMap.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/simplifier/UseITEContext.h.orig 2012-03-19 21:59:03.000000000 -0600 ++++ ./src/simplifier/UseITEContext.h 2012-08-07 16:22:05.829811496 -0600 +@@ -13,7 +13,7 @@ + + #include "../AST/AST.h" + #include "../STPManager/STPManager.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/simplifier/AIGSimplifyPropositionalCore.h.orig 2012-03-19 21:59:03.000000000 -0600 ++++ ./src/simplifier/AIGSimplifyPropositionalCore.h 2012-08-07 16:22:05.830811479 -0600 +@@ -18,7 +18,7 @@ + #include "../extlib-abc/dar.h" + #include "../to-sat/AIG/BBNodeManagerAIG.h" + #include "../to-sat/BitBlaster.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/simplifier/FindPureLiterals.h.orig 2012-01-23 05:43:59.000000000 -0700 ++++ ./src/simplifier/FindPureLiterals.h 2012-08-07 16:22:05.830811479 -0600 +@@ -21,7 +21,7 @@ + #include "../AST/AST.h" + #include "../STPManager/STPManager.h" + #include "../simplifier/simplifier.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/simplifier/Symbols.h.orig 2012-01-23 05:43:59.000000000 -0700 ++++ ./src/simplifier/Symbols.h 2012-08-07 16:22:05.831811462 -0600 +@@ -1,7 +1,7 @@ + #ifndef SYMBOLS_H + #define SYMBOLS_H + +-#include "../boost/noncopyable.hpp" ++#include + + // Each node is either: empty, an ASTNode, or a vector of more than one child nodes. + +--- ./src/simplifier/AlwaysTrue.h.orig 2012-01-23 05:43:59.000000000 -0700 ++++ ./src/simplifier/AlwaysTrue.h 2012-08-07 16:22:05.831811462 -0600 +@@ -7,7 +7,7 @@ + #include "../AST/AST.h" + #include "../STPManager/STPManager.h" + #include "../simplifier/simplifier.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/simplifier/RemoveUnconstrained.h.orig 2012-03-19 21:59:03.000000000 -0600 ++++ ./src/simplifier/RemoveUnconstrained.h 2012-08-07 16:22:05.832811445 -0600 +@@ -11,7 +11,7 @@ + #include "constantBitP/Dependencies.h" + #include "simplifier.h" + #include "MutableASTNode.h" +-#include "../boost/noncopyable.hpp" ++#include + + + namespace BEEV +--- ./src/simplifier/bvsolver.h.orig 2012-03-19 21:59:03.000000000 -0600 ++++ ./src/simplifier/bvsolver.h 2012-08-07 16:22:05.832811445 -0600 +@@ -13,7 +13,7 @@ + #include "simplifier.h" + #include "Symbols.h" + #include "VariablesInExpression.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/simplifier/VariablesInExpression.h.orig 2012-01-23 05:43:59.000000000 -0700 ++++ ./src/simplifier/VariablesInExpression.h 2012-08-07 16:22:05.833811428 -0600 +@@ -8,7 +8,7 @@ + + #include "../AST/AST.h" + #include "Symbols.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/simplifier/PropagateEqualities.h.orig 2012-01-23 05:43:59.000000000 -0700 ++++ ./src/simplifier/PropagateEqualities.h 2012-08-07 16:22:05.833811428 -0600 +@@ -4,7 +4,7 @@ + #include "../AST/AST.h" + #include "../STPManager/STPManager.h" + #include "../simplifier/simplifier.h" +-#include "../boost/noncopyable.hpp" ++#include + + //This finds conjuncts which are one of: (= SYMBOL BVCONST), (= BVCONST (READ SYMBOL BVCONST)), + // (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL) +--- ./src/simplifier/EstablishIntervals.h.orig 2012-03-19 21:59:03.000000000 -0600 ++++ ./src/simplifier/EstablishIntervals.h 2012-08-07 16:22:05.834811411 -0600 +@@ -8,7 +8,7 @@ + #include "../STPManager/STPManager.h" + #include "simplifier.h" + #include "../AST/NodeFactory/SimplifyingNodeFactory.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/AST/NodeFactory/NodeFactory.h.orig 2012-03-19 21:59:03.000000000 -0600 ++++ ./src/AST/NodeFactory/NodeFactory.h 2012-08-07 16:22:05.834811411 -0600 +@@ -4,7 +4,7 @@ + + #include + #include "../ASTKind.h" +-#include "../../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/AST/ArrayTransformer.h.orig 2012-05-11 20:18:08.000000000 -0600 ++++ ./src/AST/ArrayTransformer.h 2012-08-07 16:22:05.834811411 -0600 +@@ -13,7 +13,7 @@ + #include "AST.h" + #include "../STPManager/STPManager.h" + #include "../AST/NodeFactory/SimplifyingNodeFactory.h" +-#include "../boost/noncopyable.hpp" ++#include + + namespace BEEV + { +--- ./src/AST/RunTimes.h.orig 2012-01-23 05:43:59.000000000 -0700 ++++ ./src/AST/RunTimes.h 2012-08-07 16:22:05.835811395 -0600 +@@ -15,7 +15,7 @@ + #include + #include "../sat/utils/System.h" + #include +-#include "../boost/noncopyable.hpp" ++#include + + class RunTimes : boost::noncopyable + { diff --git a/stp-warning.patch b/stp-warning.patch index 3133ca8..2a98623 100644 --- a/stp-warning.patch +++ b/stp-warning.patch @@ -1,833 +1,787 @@ ---- ./src/simplifier/UseITEContext.h.orig 2011-04-07 07:38:52.000000000 -0600 -+++ ./src/simplifier/UseITEContext.h 2012-01-10 16:05:21.201610452 -0700 -@@ -27,7 +27,7 @@ namespace BEEV - if (n.GetKind() == NOT && n[0].GetKind() == OR) - { - ASTVec flat = FlattenKind(OR, n[0].GetChildren()); -- for (int i = 0; i < flat.size(); i++) -+ for (size_t i = 0; i < flat.size(); i++) - context.insert(nf->CreateNode(NOT, flat[i])); - } - else if (n.GetKind() == AND) -@@ -85,7 +85,7 @@ namespace BEEV - } - else - { -- for (int i = 0; i < n.GetChildren().size(); i++) -+ for (size_t i = 0; i < n.GetChildren().size(); i++) - new_children.push_back(visit(n[i], visited, visited_empty, context)); - } +--- ./src/c_interface/c_interface.cpp.orig 2012-04-18 06:38:48.000000000 -0600 ++++ ./src/c_interface/c_interface.cpp 2012-08-07 16:26:11.734851974 -0600 +@@ -557,7 +557,6 @@ void vc_printCounterExample(VC vc) { ---- ./src/simplifier/AlwaysTrue.h.orig 2011-05-01 06:48:53.000000000 -0600 -+++ ./src/simplifier/AlwaysTrue.h 2012-01-10 16:05:21.202610431 -0700 -@@ -88,7 +88,7 @@ public: - else - new_state = state; + Expr vc_getCounterExample(VC vc, Expr e) { + nodestar a = (nodestar)e; +- bmstar b = (bmstar)(((stpstar)vc)->bm); + ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); -- for (int i=0; i < n.Degree(); i++) -+ for (size_t i=0; i < n.Degree(); i++) - { - newChildren.push_back(visit(n[i],new_state,fromTo)); - } ---- ./src/simplifier/MutableASTNode.h.orig 2011-03-29 07:18:23.000000000 -0600 -+++ ./src/simplifier/MutableASTNode.h 2012-01-10 16:05:21.210610269 -0700 -@@ -46,12 +46,12 @@ public: - vector tempChildren; - tempChildren.reserve(n.Degree()); + bool t = false; +@@ -570,7 +569,6 @@ Expr vc_getCounterExample(VC vc, Expr e) -- for (int i = 0; i < n.Degree(); i++) -+ for (size_t i = 0; i < n.Degree(); i++) - tempChildren.push_back(build(n[i], visited)); + void vc_getCounterExampleArray(VC vc, Expr e, Expr **indices, Expr **values, int *size) { + nodestar a = (nodestar)e; +- bmstar b = (bmstar)(((stpstar)vc)->bm); + ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); - MutableASTNode * mut = createNode(n); + bool t = false; +@@ -590,7 +588,6 @@ void vc_getCounterExampleArray(VC vc, Ex + } -- for (int i = 0; i < n.Degree(); i++) -+ for (size_t i = 0; i < n.Degree(); i++) - tempChildren[i]->parents.insert(mut); + int vc_counterexample_size(VC vc) { +- bmstar b = (bmstar)(((stpstar)vc)->bm); + ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); - mut->children.insert(mut->children.end(),tempChildren.begin(),tempChildren.end()); -@@ -86,7 +86,7 @@ private: - assert(found); - } + return ce->CounterExampleSize(); +@@ -982,7 +979,7 @@ Expr vc_bvConstExprFromInt(VC vc, + bmstar b = (bmstar)(((stpstar)vc)->bm); -- for (int i = 0; i < children.size(); i++) -+ for (size_t i = 0; i < children.size(); i++) - { - // call check on all the children. - children[i]->checkInvariant(); -@@ -116,7 +116,7 @@ private: - return n; + unsigned long long int v = (unsigned long long int)value; +- unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> 64-n_bits; ++ unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> (64-n_bits); + //printf("%ull", max_n_bits); + if(v > max_n_bits) { + printf("CInterface: vc_bvConstExprFromInt: "\ +@@ -1546,16 +1543,11 @@ Expr vc_bvWriteToMemoryArray(VC vc, + return vc_writeExpr(vc, array, byteIndex, element); + else { + int count = 1; +- int hi = newBitsPerElem - 1; +- int low = newBitsPerElem - 8; + int low_elem = 0; + int hi_elem = low_elem + 7; + Expr c = vc_bvExtract(vc, element, hi_elem, low_elem); + Expr newarray = vc_writeExpr(vc, array, byteIndex, c); + while(--numOfBytes > 0) { +- hi = low-1; +- low = low-8; +- + low_elem = low_elem + 8; + hi_elem = low_elem + 7; + +@@ -1730,7 +1722,6 @@ int vc_isBool(Expr e) { + } - ASTVec newChildren; -- for (int i = 0; i < children.size(); i++) -+ for (size_t i = 0; i < children.size(); i++) - newChildren.push_back(children[i]->toASTNode(nf)); - - // Don't use the hashing node factory here. Imagine CreateNode simplified down, -@@ -189,7 +189,7 @@ private: - removeChildren(vars); // ignore the result - children.clear(); - children.insert(children.begin(), newN->children.begin(), newN->children.end()); -- for (int i = 0; i < children.size(); i++) -+ for (size_t i = 0; i < children.size(); i++) - children[i]->parents.insert(this); - - propagateUpDirty(); -@@ -249,7 +249,7 @@ private: - - ASTNode& node = all[i]->n; - bool found[node.GetValueWidth()]; -- for (int j=0; j bm); + // for(std::vector::iterator it=created_exprs.begin(), + // itend=created_exprs.end();it!=itend;it++) { + // BEEV::ASTNode * aaa = *it; +--- ./src/to-sat/BitBlaster.cpp.orig 2012-04-06 18:20:57.000000000 -0600 ++++ ./src/to-sat/BitBlaster.cpp 2012-08-07 16:26:11.736851970 -0600 +@@ -64,7 +64,7 @@ namespace BEEV + size_t operator()(const vector& n) const { -- for (int i = 0; i < all.size(); i++) -+ for (size_t i = 0; i < all.size(); i++) - delete all[i]; - all.clear(); + int hash =0; +- for (int i=0; i < std::min(n.size(),(size_t)6); i++) ++ for (size_t i=0; i < std::min(n.size(),(size_t)6); i++) + hash += n[i].GetNodeNum(); + return hash; } ---- ./src/simplifier/EstablishIntervals.h.orig 2011-08-08 23:15:54.000000000 -0600 -+++ ./src/simplifier/EstablishIntervals.h 2012-01-10 16:05:21.210610269 -0700 -@@ -117,7 +117,7 @@ namespace BEEV - ASTVec new_children; - new_children.reserve(result.GetChildren().size()); +@@ -79,7 +79,7 @@ namespace BEEV + if (n0.size() != n1.size()) + return false; -- for (int i =0; i < result.Degree();i++) -+ for (size_t i =0; i < result.Degree();i++) - new_children.push_back(replace(result[i],fromTo,cache)); +- for (int i=0; i < n0.size(); i++) ++ for (size_t i=0; i < n0.size(); i++) + { + if (!(n0[i] == n1[i])) + return false; +@@ -428,7 +428,7 @@ namespace BEEV + bool + BitBlaster::isConstant(const BBNodeVec& v) + { +- for (int i = 0; i < v.size(); i++) ++ for (size_t i = 0; i < v.size(); i++) + { + if (v[i] != nf->getTrue() && v[i] != nf->getFalse()) + return false; +@@ -451,7 +451,7 @@ namespace BEEV - if (new_children == result.GetChildren()) -@@ -496,7 +496,7 @@ namespace BEEV - result = freshUnsignedInterval(n.GetValueWidth()); + CBV bv = CONSTANTBV::BitVector_Create(v.size(), true); - // Copy in the minimum and maximum. -- for (int i=0; i < n[0].GetValueWidth();i++) -+ for (unsigned int i=0; i < n[0].GetValueWidth();i++) - { - if (CONSTANTBV::BitVector_bit_test(children[0]->maxV,i)) - CONSTANTBV::BitVector_Bit_On(result->maxV,i); -@@ -509,7 +509,7 @@ namespace BEEV - CONSTANTBV::BitVector_Bit_Off(result->minV,i); - } +- for (int i = 0; i < v.size(); i++) ++ for (size_t i = 0; i < v.size(); i++) + if (v[i] == nf->getTrue()) + CONSTANTBV::BitVector_Bit_On(bv, i); -- for (int i=n[0].GetValueWidth(); i < n.GetValueWidth();i++) -+ for (unsigned int i=n[0].GetValueWidth(); i < n.GetValueWidth();i++) - CONSTANTBV::BitVector_Bit_Off(result->maxV,i); - } - } else if (knownC1) -@@ -517,13 +517,13 @@ namespace BEEV - // Ignores what's already there for now.. - - IntervalType * circ_result = freshUnsignedInterval(n.GetValueWidth()); -- for (int i=0; i < n[0].GetValueWidth()-1;i++) -+ for (unsigned int i=0; i < n[0].GetValueWidth()-1;i++) +@@ -787,14 +787,14 @@ namespace BEEV { - CONSTANTBV::BitVector_Bit_On(circ_result->maxV,i); - CONSTANTBV::BitVector_Bit_Off(circ_result->minV,i); + // Add all the children up using an addition network. + vector results; +- for (int i = 0; i < term.Degree(); i++) ++ for (size_t i = 0; i < term.Degree(); i++) + results.push_back(BBTerm(term[i], support)); + +- const int bitWidth = term[0].GetValueWidth(); ++ const unsigned int bitWidth = term[0].GetValueWidth(); + std::vector > products(bitWidth+1); +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { +- for (int j = 0; j < results.size(); j++) ++ for (size_t j = 0; j < results.size(); j++) + products[i].push_back(results[j][i]); + } + +@@ -1283,7 +1283,7 @@ namespace BEEV + const BBNode& BBTrue = nf->getTrue(); + const BBNode& BBFalse = nf->getFalse(); + +- for (int i = 0; i < v.size(); i++) ++ for (size_t i = 0; i < v.size(); i++) + { + if (v[i] == BBTrue) + result[i] = ONE_MT; +@@ -1295,7 +1295,7 @@ namespace BEEV + + // find runs of ones. + int lastOne = -1; +- for (int i = 0; i < v.size(); i++) ++ for (size_t i = 0; i < v.size(); i++) + { + assert(result[i] != MINUS_ONE_MT); + +@@ -1305,7 +1305,7 @@ namespace BEEV + if (result[i] != ONE_MT && lastOne != -1 && (i - lastOne >= 3)) + { + result[lastOne] = MINUS_ONE_MT; +- for (int j = lastOne + 1; j < i; j++) ++ for (size_t j = lastOne + 1; j < i; j++) + result[j] = ZERO_MT; + // Should this be lastOne = i? + lastOne = i; +@@ -1319,7 +1319,7 @@ namespace BEEV + if (lastOne != -1 && (v.size() - lastOne > 1)) + { + result[lastOne] = MINUS_ONE_MT; +- for (int j = lastOne + 1; j < v.size(); j++) ++ for (size_t j = lastOne + 1; j < v.size(); j++) + result[j] = ZERO_MT; + } + } +@@ -1361,7 +1361,7 @@ namespace BEEV + BitBlaster::buildAdditionNetworkResult(vector >& products, set& support, + const ASTNode& n) + { +- const int bitWidth = n.GetValueWidth(); ++ const unsigned int bitWidth = n.GetValueWidth(); + + // If we have details of the partial products which can be true, + int ignore = -1; +@@ -1370,7 +1370,7 @@ namespace BEEV + ms = NULL; + + BBNodeVec results; +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + + buildAdditionNetworkResult(products[i], products[i+1], support, (i + 1 == bitWidth), (ms != NULL && (ms->sumH[i] == 0))); +@@ -1380,7 +1380,7 @@ namespace BEEV + } + + assert(products[bitWidth].size() ==0); // products[bitwidth] is defined but should never be used. +- assert(results.size() == ((unsigned)bitWidth)); ++ assert(results.size() == bitWidth); + return results; + } + +@@ -1482,7 +1482,7 @@ namespace BEEV + BitBlaster::multWithBounds(const ASTNode&n, vector >& products, + BBNodeSet& toConjoinToTop) + { +- const int bitWidth = n.GetValueWidth(); ++ const unsigned int bitWidth = n.GetValueWidth(); + + int ignored=0; + assert(upper_multiplication_bound); +@@ -1491,7 +1491,7 @@ namespace BEEV + + + // If all of the partial products in the column must be zero, then replace +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + if (conjoin_to_top && ms.columnH[i] == 0) + { +@@ -1513,7 +1513,7 @@ namespace BEEV + } + + vector prior; +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + if (debug_bounds) + { +@@ -1533,7 +1533,7 @@ namespace BEEV + if (debug_bitblaster) + cerr << endl << endl; + +- assert(result.size() == ((unsigned)bitWidth)); ++ assert(result.size() == bitWidth); + return result; + } + +@@ -1557,7 +1557,7 @@ namespace BEEV + } + + BBNodeVec notY; +- for (int i = 0; i < y.size(); i++) ++ for (size_t i = 0; i < y.size(); i++) + { + notY.push_back(nf->CreateNode(NOT, y[i])); + } +@@ -1610,7 +1610,7 @@ namespace BEEV + t_products[i].push_back(BBFalse); + + sort(t_products[i].begin(), t_products[i].end()); +- for (int j = 0; j < t_products[i].size(); j++) ++ for (size_t j = 0; j < t_products[i].size(); j++) + products[i].push_back(t_products[i][j]); + } + } +@@ -1668,13 +1668,13 @@ namespace BEEV + assert(ms->x.getWidth() == ms->y.getWidth()); + assert(ms->r.getWidth() == ms->y.getWidth()); + assert(ms->r.getWidth() == (int)ms->bitWidth); +- } + +- for (int i = 0; i < n.GetValueWidth(); i++) +- if (ms->sumH[i] == 0) +- highestZero = i; ++ for (unsigned int i = 0; i < n.GetValueWidth(); i++) ++ if (ms->sumH[i] == 0) ++ highestZero = i; + +- return ms; ++ return ms; ++ } + } + + return NULL; +@@ -1686,7 +1686,7 @@ namespace BEEV + BitBlaster::mult_normal(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, + const ASTNode&n) + { +- const int bitWidth = n.GetValueWidth(); ++ const unsigned int bitWidth = n.GetValueWidth(); + + // If we have details of the partial products which can be true, + int highestZero = -1; +@@ -1698,7 +1698,7 @@ namespace BEEV + + BBNodeVec prod = BBNodeVec(BBAndBit(y, *x.begin())); // start prod with first partial product. + +- for (int i = 1; i < bitWidth; i++) // start loop at next bit. ++ for (unsigned int i = 1; i < bitWidth; i++) // start loop at next bit. + { + const BBNode& xit = x[i]; + +@@ -1715,7 +1715,7 @@ namespace BEEV + BBNodeVec pprod = BBAndBit(ycopy, xit); + + // Iterate through from the current location upwards, setting anything to zero that can be.. +- if (ms != NULL && highestZero >= i) ++ if (ms != NULL && highestZero >= (int)i) + { + for (int column = i; column <= highestZero; column++) + { +@@ -1740,7 +1740,7 @@ namespace BEEV + { + + // Add the carry from the prior column. i.e. each second sorted formula. +- for (int k = 1; k < priorSorted.size(); k += 2) ++ for (size_t k = 1; k < priorSorted.size(); k += 2) + { + current.push_back(priorSorted[k]); + } +@@ -1820,7 +1820,7 @@ namespace BEEV + FixedBits* b = cb->fixedMap->map->find(n)->second; + for (int i = 0; i < b->getWidth(); i++) + { +- if (b->isFixed(i)) ++ if (b->isFixed(i)) { + if (b->getValue(i)) + { + assert(v[i]== BBTrue); +@@ -1837,6 +1837,7 @@ namespace BEEV + + assert(v[i]== BBFalse); + } ++ } + } + } + } +@@ -1850,7 +1851,7 @@ namespace BEEV + BitBlaster::setColumnsToZero(vector >& products, set& support, + const ASTNode&n) + { +- const int bitWidth = n.GetValueWidth(); ++ const unsigned int bitWidth = n.GetValueWidth(); + + // If we have details of the partial products which can be true, + int highestZero = -1; +@@ -1861,7 +1862,7 @@ namespace BEEV + if (ms == NULL) + return; + +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + if (ms->sumH[i] == 0) + { +@@ -2000,18 +2001,18 @@ namespace BEEV + vector b; + + // half way rounded up. +- const int halfWay = (((in.size()%2)==0? 0:1) + (in.size()/2) ); +- for (int i =0; i < halfWay;i++) ++ const size_t halfWay = (((in.size()%2)==0? 0:1) + (in.size()/2) ); ++ for (size_t i =0; i < halfWay;i++) + a.push_back(in[i]); + +- for (int i =halfWay; i < in.size();i++) ++ for (size_t i =halfWay; i < in.size();i++) + b.push_back(in[i]); + + assert(a.size() >= b.size()); + assert(a.size() + b.size() == in.size()); + vector result= mergeSorted(batcher(a), batcher(b)); + +- for (int k = 0; k < result.size(); k++) ++ for (size_t k = 0; k < result.size(); k++) + assert(!result[k].IsNull()); + + assert(result.size() == in.size()); +@@ -2043,7 +2044,7 @@ namespace BEEV + assert(sorted.size() == toSort.size()); + + vector sortedCarryIn; +- for (int k = 1; k < priorSorted.size(); k += 2) ++ for (size_t k = 1; k < priorSorted.size(); k += 2) + { + sortedCarryIn.push_back(priorSorted[k]); + } +@@ -2081,11 +2082,11 @@ namespace BEEV + BBNodeVec + BitBlaster::v6(vector >& products, set& support, const ASTNode&n) + { +- const int bitWidth = n.GetValueWidth(); ++ const unsigned int bitWidth = n.GetValueWidth(); + + vector prior; + +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + vector output; + sortingNetworkAdd(support, products[i], output ,prior); +@@ -2101,7 +2102,7 @@ namespace BEEV + BBNodeVec + BitBlaster::v13(vector >& products, set& support, const ASTNode&n) + { +- const int bitWidth = n.GetValueWidth(); ++ const unsigned int bitWidth = n.GetValueWidth(); + + int ignore = -1; + simplifier::constantBitP::MultiplicationStats* ms = getMS(n, ignore); +@@ -2117,7 +2118,7 @@ namespace BEEV + { + done = true; + +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + if (products[i].size() > 2) + done = false; +@@ -2155,12 +2156,12 @@ namespace BEEV + + } + BBPlus2(a, b, BBFalse); +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + products[i].push_back(a[i]); + } + + BBNodeVec results; +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + assert(products[i].size() ==1); + results.push_back(products[i].back()); +@@ -2178,22 +2179,22 @@ namespace BEEV + BBNodeVec + BitBlaster::v9(vector >& products, set& support,const ASTNode&n) + { +- const int bitWidth = n.GetValueWidth(); ++ const unsigned int bitWidth = n.GetValueWidth(); + + vector< vector< BBNode> > toAdd(bitWidth); + +- for (int column = 0; column < bitWidth; column++) ++ for (unsigned int column = 0; column < bitWidth; column++) + { + vector sorted; // The current column (sorted) gets put into here. + vector prior; // Prior is always empty in this.. + +- const int size= products[column].size(); ++ const size_t size= products[column].size(); + sortingNetworkAdd(support, products[column], sorted ,prior); + + assert(products[column].size() == 1); + assert(sorted.size() == size); + +- for (int k = 2; k <= sorted.size(); k++) ++ for (size_t k = 2; k <= sorted.size(); k++) + { + BBNode part; + if (k==sorted.size()) +@@ -2208,8 +2209,8 @@ namespace BEEV + continue; // shortcut. + } + +- int position =k; +- int increment =1; ++ size_t position =k; ++ unsigned int increment =1; + while (position != 0) + { + if (column+increment >= bitWidth) +@@ -2223,12 +2224,12 @@ namespace BEEV + } + } + +- for (int carry_column =column+1; carry_column < bitWidth; carry_column++) ++ for (unsigned int carry_column =column+1; carry_column < bitWidth; carry_column++) + { + if (toAdd[carry_column].size() ==0) + continue ; + BBNode disjunct = BBFalse; +- for (int l = 0; l < toAdd[carry_column].size();l++) ++ for (size_t l = 0; l < toAdd[carry_column].size();l++) + { + disjunct = nf->CreateNode(OR,disjunct,toAdd[carry_column][l]); + } +@@ -2238,7 +2239,7 @@ namespace BEEV + toAdd[carry_column].clear(); + } + } +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + assert(toAdd[i].size() == 0); + } +@@ -2252,7 +2253,7 @@ namespace BEEV + BBNodeVec + BitBlaster::v7(vector >& products, set& support, const ASTNode&n) + { +- const int bitWidth = n.GetValueWidth(); ++ const unsigned int bitWidth = n.GetValueWidth(); + + // If we have details of the partial products which can be true, + int ignore = -1; +@@ -2264,13 +2265,13 @@ namespace BEEV + std::vector > later(bitWidth+1); + std::vector > next(bitWidth+1); + +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + next[i+1].clear(); + buildAdditionNetworkResult(products[i], next[i + 1], support, bitWidth == i+1, (ms!=NULL && (ms->sumH[i]==0))); + + // Calculate the carries of carries. +- for (int j = i + 1; j < bitWidth; j++) ++ for (unsigned int j = i + 1; j < bitWidth; j++) + { + if (next[j].size() == 0) + break; +@@ -2280,7 +2281,7 @@ namespace BEEV + } + + // Put the carries of the carries away until later. +- for (int j = i + 1; j < bitWidth; j++) ++ for (unsigned int j = i + 1; j < bitWidth; j++) + { + if (next[j].size() == 0) + break; +@@ -2291,7 +2292,7 @@ namespace BEEV } -- for (int i=n[0].GetValueWidth()-1; i < n.GetValueWidth();i++) -+ for (unsigned int i=n[0].GetValueWidth()-1; i < n.GetValueWidth();i++) - { - CONSTANTBV::BitVector_Bit_Off(circ_result->maxV,i); - CONSTANTBV::BitVector_Bit_On(circ_result->minV,i); -@@ -598,7 +598,7 @@ namespace BEEV - CONSTANTBV::BitVector_increment(result->maxV); - bool bad= false; -- for (int i =0; i < children.size(); i++) -+ for (size_t i =0; i < children.size(); i++) - { - if (children[i] == NULL) - { -@@ -611,10 +611,10 @@ namespace BEEV - e = CONSTANTBV::BitVector_Multiply(max, result->maxV, children[i]->maxV); - assert (0 == e); - -- if (CONSTANTBV::Set_Max(max) >= width) -+ if (CONSTANTBV::Set_Max(max) >= (long)width) - bad = true; - -- for (int j = width; j < 2 * width; j++) -+ for (unsigned int j = width; j < 2 * width; j++) - { - if (CONSTANTBV::BitVector_bit_test(min, j)) - bad = true; -@@ -687,7 +687,7 @@ namespace BEEV - - bool carry = false; - -- for (int i =0; i < children.size(); i++) -+ for (size_t i =0; i < children.size(); i++) - { - if (children[i] == NULL) - { -@@ -716,7 +716,7 @@ namespace BEEV - if (knownC1) - { - // Copy in the minimum and maximum. -- for (int i=0; i < n[1].GetValueWidth();i++) -+ for (unsigned int i=0; i < n[1].GetValueWidth();i++) - { - if (CONSTANTBV::BitVector_bit_test(children[1]->maxV,i)) - CONSTANTBV::BitVector_Bit_On(result->maxV,i); -@@ -733,7 +733,7 @@ namespace BEEV - if (knownC0) - { - // Copy in the minimum and maximum. -- for (int i=n[1].GetValueWidth(); i < n.GetValueWidth();i++) -+ for (unsigned int i=n[1].GetValueWidth(); i < n.GetValueWidth();i++) - { - if (CONSTANTBV::BitVector_bit_test(children[0]->maxV,i- n[1].GetValueWidth())) - CONSTANTBV::BitVector_Bit_On(result->maxV,i); -@@ -754,7 +754,7 @@ namespace BEEV - - bool nonNull = true; - // If all the children are known, output 'em. -- for (int i=0; i < n.Degree();i++) -+ for (size_t i=0; i < n.Degree();i++) - { - if (children[i]== NULL) - nonNull=false; -@@ -763,7 +763,7 @@ namespace BEEV - if (false && nonNull && n.GetKind() != SYMBOL && n.GetKind() != AND) - { - cerr << n; -- for (int i=0; i < n.Degree();i++) -+ for (size_t i=0; i < n.Degree();i++) - children[i]->print(); - } - } -@@ -796,10 +796,10 @@ namespace BEEV - - ~EstablishIntervals() - { -- for (int i =0; i < toDeleteLater.size();i++) -+ for (size_t i =0; i < toDeleteLater.size();i++) - delete toDeleteLater[i]; - -- for (int i =0; i < likeAutoPtr.size();i++) -+ for (size_t i =0; i < likeAutoPtr.size();i++) - CONSTANTBV::BitVector_Destroy(likeAutoPtr[i]); - - likeAutoPtr.clear(); ---- ./src/simplifier/constantBitP/ConstantBitP_Shifting.cpp.orig 2010-11-27 20:45:32.000000000 -0700 -+++ ./src/simplifier/constantBitP/ConstantBitP_Shifting.cpp 2012-01-10 16:05:21.211610249 -0700 -@@ -204,8 +204,6 @@ Result bvArithmeticRightShiftBothWays(ve - assert(children[0]->getWidth() == children[1]->getWidth()); - const unsigned MSBIndex = bitWidth-1; - -- Result result = NO_CHANGE; -- - FixedBits& op = *children[0]; - FixedBits& shift = *children[1]; - -@@ -393,7 +391,6 @@ Result bvArithmeticRightShiftBothWays(ve - { - shift.setFixed(i, true); - shift.setValue(i, setOfPossibleShifts.getValue(i)); -- result = CHANGED; - } - else if (shift.isFixed(i) && shift.getValue(i) - != setOfPossibleShifts.getValue(i)) -@@ -550,7 +547,6 @@ Result bvArithmeticRightShiftBothWays(ve - { - output.setFixed(column, true); - output.setValue(column, allFixedTo); -- result = CHANGED; - } - } - } -@@ -563,8 +559,6 @@ Result bvLeftShiftBothWays(vector 0); - -- Result result = NO_CHANGE; -- - FixedBits& op = *children[0]; - FixedBits& shift = *children[1]; - -@@ -761,7 +755,6 @@ Result bvLeftShiftBothWays(vectorpush(n[i]); - } - -@@ -462,7 +462,7 @@ namespace simplifier - - assert(FixedBits::equals(newBits, current)); - -- for (int i = 0; i < n.Degree(); i++) -+ for (size_t i = 0; i < n.Degree(); i++) - { - if (!FixedBits::equals(*getUpdatedFixedBits(n[i]), - childrenFixedBits[i])) ---- ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp.orig 2010-11-27 20:45:32.000000000 -0700 -+++ ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp 2012-01-10 16:05:21.212610229 -0700 -@@ -110,8 +110,6 @@ void destroy(CBV a, CBV b, CBV c, CBV d) - - Result bvSignedLessThanBothWays(FixedBits& c0, FixedBits& c1, FixedBits& output) - { -- Result r = NO_CHANGE; -- - assert(c0.getWidth() == c1.getWidth()); - - CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); -@@ -135,7 +133,6 @@ Result bvSignedLessThanBothWays(FixedBit - { - output.setFixed(0, true); - output.setValue(0, true); -- r = CHANGED; - } - } - -@@ -153,7 +150,6 @@ Result bvSignedLessThanBothWays(FixedBit - { - output.setFixed(0, true); - output.setValue(0, false); -- r = CHANGED; - } - } - -@@ -183,7 +179,6 @@ Result bvSignedLessThanBothWays(FixedBit - c0.setFixed(msb, true); - c0.setValue(msb, true); - setSignedMinMax(c0, c0_min, c0_max); -- r = CHANGED; - } - else - { -@@ -199,7 +194,6 @@ Result bvSignedLessThanBothWays(FixedBit - c1.setFixed(msb, true); - c1.setValue(msb, false); - setSignedMinMax(c1, c1_min, c1_max); -- r = CHANGED; - } - else - { -@@ -222,7 +216,6 @@ Result bvSignedLessThanBothWays(FixedBit - c0.setFixed(i, true); - c0.setValue(i, false); - setSignedMinMax(c0, c0_min, c0_max); -- r = CHANGED; - } - else - { -@@ -242,7 +235,6 @@ Result bvSignedLessThanBothWays(FixedBit - c1.setFixed(i, true); - c1.setValue(i, true); - setSignedMinMax(c1, c1_min, c1_max); -- r = CHANGED; - } - else - { -@@ -259,8 +251,6 @@ Result bvSignedLessThanBothWays(FixedBit - - Result bvSignedLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output) - { -- Result r = NO_CHANGE; -- - assert(c0.getWidth() == c1.getWidth()); - - CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); -@@ -283,7 +273,6 @@ Result bvSignedLessThanEqualsBothWays(Fi - { - output.setFixed(0, true); - output.setValue(0, true); -- r = CHANGED; - } - } - -@@ -299,7 +288,6 @@ Result bvSignedLessThanEqualsBothWays(Fi - { - output.setFixed(0, true); - output.setValue(0, false); -- r = CHANGED; - } - } - -@@ -329,7 +317,6 @@ Result bvSignedLessThanEqualsBothWays(Fi - c0.setFixed(msb, true); - c0.setValue(msb, true); - setSignedMinMax(c0, c0_min, c0_max); -- r = CHANGED; - } - else - { -@@ -345,7 +332,6 @@ Result bvSignedLessThanEqualsBothWays(Fi - c1.setFixed(msb, true); - c1.setValue(msb, false); - setSignedMinMax(c1, c1_min, c1_max); -- r = CHANGED; - } - else - { -@@ -412,8 +398,6 @@ Result bvSignedLessThanEqualsBothWays(Fi - // UNSIGNED!! - Result bvLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output) - { -- Result r = NO_CHANGE; -- - assert(c0.getWidth() == c1.getWidth()); - - CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); -@@ -467,8 +451,6 @@ Result bvLessThanBothWays(FixedBits& c0, - return bvGreaterThanEqualsBothWays(c0, c1, t); - } - -- bool changed = false; -- - if (output.isFixed(0) && output.getValue(0)) - { - // Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side -@@ -484,7 +466,6 @@ Result bvLessThanBothWays(FixedBits& c0, - c0.setFixed(i, true); - c0.setValue(i, false); - setUnsignedMinMax(c0, c0_min, c0_max); -- changed = true; - } - else - { -@@ -504,7 +485,6 @@ Result bvLessThanBothWays(FixedBits& c0, - c1.setFixed(i, true); - c1.setValue(i, true); - setUnsignedMinMax(c1, c1_min, c1_max); -- changed = true; - } - else - { -@@ -521,8 +501,6 @@ Result bvLessThanBothWays(FixedBits& c0, - - Result bvLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output) - { -- Result r = NO_CHANGE; -- - assert(c0.getWidth() == c1.getWidth()); - - CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); ---- ./src/simplifier/constantBitP/multiplication/ImplicationGraph.h.orig 2012-01-01 19:35:12.000000000 -0700 -+++ ./src/simplifier/constantBitP/multiplication/ImplicationGraph.h 2012-01-10 16:12:04.745158953 -0700 -@@ -106,13 +106,13 @@ class ImplicationGraph - if (debug_multiply) - { - cout << "left"; -- for (int i = 0; i < left.size(); i++) -+ for (size_t i = 0; i < left.size(); i++) - { - - cout << "[" << i << ":" << left[i].size() << "] "; - } - cout << "right"; -- for (int i = 0; i < right.size(); i++) -+ for (size_t i = 0; i < right.size(); i++) - { - - cout << "[" << i << ":" << right[i].size() << "] "; -@@ -512,8 +512,6 @@ public: - if (!ok) - return CONFLICT; - -- Result r; -- - bool changed = writeIn(left_assigned, left); - changed = writeIn(right_assigned, right) | changed; - -@@ -578,7 +576,7 @@ public: - } - - bool allAlreadyMin = true; -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - if (min[i] != 0) - allAlreadyMin = false; - ---- ./src/simplifier/constantBitP/ConstantBitP_Division.cpp.orig 2012-01-01 19:28:47.000000000 -0700 -+++ ./src/simplifier/constantBitP/ConstantBitP_Division.cpp 2012-01-10 16:10:56.223982228 -0700 -@@ -172,14 +172,14 @@ Result bvUnsignedQuotientAndRemainder(ve - if (whatIs == QUOTIENT_IS_OUTPUT) { - setUnsignedMinMax(output, minQuotient, maxQuotient); - -- for (int i = 0; i < width; i++) -+ for (unsigned int i = 0; i < width; i++) - CONSTANTBV::BitVector_Bit_On(maxRemainder, i); - } - else - { - setUnsignedMinMax(output, minRemainder, maxRemainder); - -- for (int i =0; i < width;i++) -+ for (unsigned int i =0; i < width;i++) - CONSTANTBV::BitVector_Bit_On(maxQuotient,i); - } - ---- ./src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp.orig 2010-11-27 20:45:32.000000000 -0700 -+++ ./src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp 2012-01-10 16:05:21.213610209 -0700 -@@ -33,7 +33,6 @@ Result bvSubtractBothWays(vector& children, FixedBits& output) - { -- Result result = NO_CHANGE; -- - const int bitWidth = output.getWidth(); - const int numberOfChildren = children.size(); - -@@ -361,7 +356,6 @@ Result bvAddBothWays(vector& - { - output.setFixed(column, true); - output.setValue(column, newResult); -- result = CHANGED; - changed = true; - } - else if (output.isFixed(column) && (output.getValue(column) != newResult)) ---- ./src/simplifier/FindPureLiterals.h.orig 2011-12-19 17:30:14.000000000 -0700 -+++ ./src/simplifier/FindPureLiterals.h 2012-01-10 16:05:21.214610188 -0700 -@@ -109,7 +109,7 @@ public: - { - case AND: - case OR: -- for (int i =0; i < n.Degree(); i ++) -+ for (size_t i =0; i < n.Degree(); i ++) - build(n[i],polarity); - break; - -@@ -120,7 +120,7 @@ public: - - default: - polarity = bothPolarity; // both -- for (int i =0; i < n.Degree(); i ++) -+ for (size_t i =0; i < n.Degree(); i ++) - build(n[i],polarity); - break; - } ---- ./src/simplifier/VariablesInExpression.cpp.orig 2011-02-01 05:41:57.000000000 -0700 -+++ ./src/simplifier/VariablesInExpression.cpp 2012-01-10 16:05:21.214610188 -0700 -@@ -42,7 +42,7 @@ Symbols* VariablesInExpression::getSymbo - } - - vector children; -- for (int i = 0; i < n.Degree(); i++) { -+ for (size_t i = 0; i < n.Degree(); i++) { - Symbols* v = getSymbol(n[i]); - if (!v->empty()) - children.push_back(v); -@@ -111,7 +111,7 @@ ASTNodeSet * VariablesInExpression::Seto - vector av; - VarSeenInTerm(symbol,visited,*symbols,av); - -- for (int i =0; i < av.size();i++) -+ for (size_t i =0; i < av.size();i++) - { - const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second; - symbols->insert(sym.begin(), sym.end()); -@@ -155,7 +155,7 @@ bool VariablesInExpression::VarSeenInTer - sort(av.begin(), av.end()); - - //cout << "===" << endl; -- for (int i = 0; i < av.size(); i++) { -+ for (size_t i = 0; i < av.size(); i++) { - if (i!=0 && av[i] == av[i-1]) - continue; - ---- ./src/simplifier/SubstitutionMap.cpp.orig 2011-12-28 20:17:45.000000000 -0700 -+++ ./src/simplifier/SubstitutionMap.cpp 2012-01-10 16:05:21.215610168 -0700 -@@ -199,7 +199,7 @@ void SubstitutionMap::buildDepends(const - vars.VarSeenInTerm(vars.getSymbol(n1), rhs_visited, rhs, av); - - sort(av.begin(), av.end()); -- for (int i =0; i < av.size();i++) -+ for (size_t i =0; i < av.size();i++) - { - if (i!=0 && av[i] == av[i-1]) - continue; // Treat it like a set of Symbol* in effect. ---- ./src/simplifier/simplifier.cpp.orig 2012-01-05 06:04:33.000000000 -0700 -+++ ./src/simplifier/simplifier.cpp 2012-01-10 16:10:08.282375196 -0700 -@@ -241,7 +241,7 @@ namespace BEEV - assert(false); - } - -- for (int i = 0; i < n.Degree(); i++) -+ for (size_t i = 0; i < n.Degree(); i++) +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) { - checkIfInSimplifyMap(n[i], visited); + // Copy all the laters into products + while(later[i].size() > 0) +@@ -2302,7 +2303,7 @@ namespace BEEV } -@@ -516,6 +516,7 @@ namespace BEEV - return getConstantBit(n[0], i); - assert(false); -+ return -1; + BBNodeVec results; +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + + buildAdditionNetworkResult((products[i]), (products[i + 1]), support, bitWidth == i+1, false); +@@ -2312,7 +2313,7 @@ namespace BEEV + products[i].pop_back(); + } + +- assert(results.size() == ((unsigned)bitWidth)); ++ assert(results.size() == bitWidth); + return results; } - ASTNode -@@ -1284,7 +1285,7 @@ namespace BEEV - else - { - ASTVec newC; -- for (int i = 0; i < a.GetChildren().size(); i++) -+ for (size_t i = 0; i < a.GetChildren().size(); i++) - { - newC.push_back(SimplifyFormula(a[i], false, VarConstMap)); - } -@@ -1646,9 +1647,9 @@ namespace BEEV - assert(BVMULT == k || SBVDIV == k || BVPLUS ==k); - const int inputValueWidth = output.GetValueWidth(); - -- int lengthA = output.GetChildren()[0][0].GetValueWidth(); -- int lengthB = output.GetChildren()[1][0].GetValueWidth(); -- int maxLength; -+ unsigned int lengthA = output.GetChildren()[0][0].GetValueWidth(); -+ unsigned int lengthB = output.GetChildren()[1][0].GetValueWidth(); -+ unsigned int maxLength; - if (BVMULT == output.GetKind()) - maxLength = lengthA + lengthB; - else if (BVPLUS == output.GetKind() || SBVDIV == output.GetKind()) -@@ -1676,7 +1677,7 @@ namespace BEEV +@@ -2321,7 +2322,7 @@ namespace BEEV + BBNodeVec + BitBlaster::v8(vector >& products, set& support, const ASTNode&n) { - const ASTNode a = children[0]; - const ASTNode b = children[1]; -- const int width = children[0].GetValueWidth(); -+ const unsigned int width = children[0].GetValueWidth(); - ASTNode output; +- const int bitWidth = n.GetValueWidth(); ++ const unsigned int bitWidth = n.GetValueWidth(); - assert(b.isConstant()); -@@ -1707,7 +1708,7 @@ namespace BEEV - { - const ASTNode a = children[0]; - const ASTNode b = children[1]; -- const int width = children[0].GetValueWidth(); -+ const unsigned int width = children[0].GetValueWidth(); - ASTNode output; + // If we have details of the partial products which can be true, + int ignore = -1; +@@ -2334,14 +2335,14 @@ namespace BEEV + std::vector > later(bitWidth+1); // +1 then ignore the topmost. + std::vector > next(bitWidth+1); - assert(b.isConstant()); -@@ -1888,7 +1889,7 @@ namespace BEEV - //I haven't measured if this is worth the expense. - { - bool notSimplified = false; -- for (int i = 0; i < inputterm.Degree(); i++) -+ for (size_t i = 0; i < inputterm.Degree(); i++) - if (inputterm[i].GetType() != ARRAY_TYPE) - if (!hasBeenSimplified(inputterm[i])) - { -@@ -2229,7 +2230,6 @@ namespace BEEV - case BVEXTRACT: +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) { - const unsigned innerLow = a0[2].GetUnsignedConst(); -- const unsigned innerHigh = a0[1].GetUnsignedConst(); + // Put all the products into next. + next[i+1].clear(); + buildAdditionNetworkResult((products[i]), (next[i + 1]), support, i+1 ==bitWidth, (ms!=NULL && (ms->sumH[i]==0))); - output = nf->CreateTerm(BVEXTRACT, inputValueWidth, a0[0], _bm->CreateBVConst(32, i_val + innerLow), - _bm->CreateBVConst(32, j_val + innerLow)); -@@ -2629,7 +2629,7 @@ namespace BEEV - assert(BVTypeCheck(output)); - - // If the leading bits are zero. Replace it by a concat with zero. -- int i; -+ unsigned int i; - if (output.GetKind() == BVAND && output.Degree() == 2 && ((i = numberOfLeadingZeroes(output[0])) > 0)) - { - // i contains the number of leading zeroes. -@@ -2651,13 +2651,13 @@ namespace BEEV - } - if (output.GetKind() == BVAND) - { -- int trailingZeroes = 0; -- for (int i = 0; i < output.Degree(); i++) -+ unsigned int trailingZeroes = 0; -+ for (size_t i = 0; i < output.Degree(); i++) - { - const ASTNode& n = output[i]; - if (n.GetKind() != BVCONST) - continue; -- int j; -+ unsigned int j; - for (j = 0; j < n.GetValueWidth(); j++) - if (CONSTANTBV::BitVector_bit_test(n.GetBVConst(), j)) - break; -@@ -2674,7 +2674,7 @@ namespace BEEV - //cerr << "old" << output; - ASTNode zeroes = _bm->CreateZeroConst(trailingZeroes); - ASTVec newChildren; -- for (int i = 0; i < output.Degree(); i++) -+ for (size_t i = 0; i < output.Degree(); i++) - newChildren.push_back( - nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - trailingZeroes, output[i], - _bm->CreateBVConst(32, output.GetValueWidth() - 1), ---- ./src/simplifier/consteval.cpp.orig 2011-12-28 19:00:01.000000000 -0700 -+++ ./src/simplifier/consteval.cpp 2012-01-10 16:05:21.217610127 -0700 -@@ -43,7 +43,7 @@ namespace BEEV - - ASTVec children; - children.reserve(number_of_children); -- for (int i =0; i < number_of_children; i++) -+ for (unsigned int i =0; i < number_of_children; i++) - { - if (input_children[i].isConstant()) - children.push_back(input_children[i]); ---- ./src/simplifier/SubstitutionMap.h.orig 2011-12-28 20:17:45.000000000 -0700 -+++ ./src/simplifier/SubstitutionMap.h 2012-01-10 16:05:21.218610106 -0700 -@@ -40,7 +40,7 @@ class SubstitutionMap { - void loops_helper(const set& varsToCheck, set& visited); - bool loops(const ASTNode& n0, const ASTNode& n1); - -- int substitutionsLastApplied; -+ size_t substitutionsLastApplied; - public: - - bool hasUnappliedSubstitutions() ---- ./src/simplifier/RemoveUnconstrained.cpp.orig 2011-12-28 19:00:01.000000000 -0700 -+++ ./src/simplifier/RemoveUnconstrained.cpp 2012-01-10 16:05:21.218610106 -0700 -@@ -60,7 +60,7 @@ namespace BEEV - - bool allChildrenAreUnconstrained(vector children) - { -- for (int i =0; i < children.size(); i++) -+ for (size_t i =0; i < children.size(); i++) - if (!children[i]->isUnconstrained()) - return false; - -@@ -105,7 +105,7 @@ namespace BEEV - // Going to be rebuilt later anyway, so discard. - vector variables; - -- for (int i =0; i n; - assert(var.GetKind() == SYMBOL); -@@ -156,7 +156,7 @@ namespace BEEV - } - - ASTNode concat = concatVec[0]; -- for (int i=1; i < concatVec.size();i++) -+ for (size_t i=1; i < concatVec.size();i++) - { - assert(!concat.IsNull()); - concat = bm.CreateTerm(BVCONCAT, concat.GetValueWidth() + concatVec[i].GetValueWidth(),concatVec[i], concat); -@@ -189,7 +189,7 @@ namespace BEEV - - topMutable->getAllUnconstrainedVariables(variable_array); - -- for (int i =0; i < variable_array.size() ; i++) -+ for (size_t i =0; i < variable_array.size() ; i++) - { - // Don't make this is a reference. If the vector gets resized, it will point to - // memory that no longer contains the object. -@@ -213,7 +213,7 @@ namespace BEEV - //nb. The children might be dirty. i.e. not have substitutions written through them yet. - ASTVec children; - children.reserve(mutable_children.size()); -- for (int j = 0; j n); - - const size_t numberOfChildren = children.size(); -@@ -247,7 +247,7 @@ namespace BEEV - { - int found = 0; - -- for (int i = 0; i < numberOfChildren; i++) -+ for (size_t i = 0; i < numberOfChildren; i++) - { - if (children[i] == var) - found++; -@@ -434,7 +434,7 @@ namespace BEEV - { - ASTNodeSet already; - ASTNode v =replaceParentWithFresh(muteParent, variable_array); -- for (int i =0; i < numberOfChildren;i++) -+ for (size_t i =0; i < numberOfChildren;i++) + // Calculate the carries of carries. +- for (int j = i + 1; j < bitWidth; j++) ++ for (unsigned int j = i + 1; j < bitWidth; j++) { - /* to avoid problems with: - 734:(AND -@@ -469,7 +469,7 @@ namespace BEEV - ASTNode v =replaceParentWithFresh(muteParent, variable_array); + if (next[j].size() == 0) + break; +@@ -2351,7 +2352,7 @@ namespace BEEV + } - ASTVec others; -- for (int i = 0; i < numberOfChildren; i++) -+ for (size_t i = 0; i < numberOfChildren; i++) - { - if (children[i] !=var) - others.push_back(mutable_children[i]->toASTNode(nf)); -@@ -622,7 +622,7 @@ namespace BEEV - case BVPLUS: - { - ASTVec other; -- for (int i = 0; i < children.size(); i++) -+ for (size_t i = 0; i < children.size(); i++) - if (children[i] != var) - other.push_back(mutable_children[i]->toASTNode(nf)); + // Put the carries of the carries away until later. +- for (int j = i + 1; j < bitWidth; j++) ++ for (unsigned int j = i + 1; j < bitWidth; j++) + { + if (next[j].size() == 0) + break; +@@ -2362,7 +2363,7 @@ namespace BEEV + } -@@ -644,7 +644,6 @@ namespace BEEV - { - ASTNode v =replaceParentWithFresh(muteParent, variable_array); -- const unsigned resultWidth = width; - const unsigned operandWidth = var.GetValueWidth(); - assert(children[0] == var); // It can't be anywhere else. +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + // Copy all the laters into products + while(later[i].size() > 0) +@@ -2373,14 +2374,14 @@ namespace BEEV + } ---- ./src/absrefine_counterexample/CounterExample.cpp.orig 2011-11-10 06:01:41.000000000 -0700 -+++ ./src/absrefine_counterexample/CounterExample.cpp 2012-01-10 16:05:21.219610086 -0700 -@@ -46,7 +46,7 @@ namespace BEEV - assert(symbol.GetKind() == SYMBOL); - vector bitVector_array(symbolWidth,false); + BBNodeVec results; +- for (int i = 0; i < bitWidth; i++) ++ for (unsigned int i = 0; i < bitWidth; i++) + { + buildAdditionNetworkResult(products[i], products[i + 1], support, i+1 ==bitWidth, false); + results.push_back(products[i].back()); + products[i].pop_back(); + } -- for (int index = 0; index < v.size(); index++) -+ for (size_t index = 0; index < v.size(); index++) - { - const unsigned sat_variable_index = v[index]; +- assert(results.size() == ((unsigned)bitWidth)); ++ assert(results.size() == bitWidth); + return results; + } -@@ -863,7 +863,7 @@ namespace BEEV - ASTNode symbol = it->first; - vector v = it->second; +@@ -2392,7 +2393,7 @@ namespace BEEV + { + vector result(in); -- for (int i =0 ; i < v.size();i++) -+ for (size_t i =0 ; i < v.size();i++) +- for (int i = 2; i < in.size(); i =i+ 2) ++ for (size_t i = 2; i < in.size(); i =i+ 2) { - if (v[i] == ~((unsigned)0)) // nb. special value. - continue; ---- ./src/absrefine_counterexample/AbstractionRefinement.cpp.orig 2012-01-05 06:04:33.000000000 -0700 -+++ ./src/absrefine_counterexample/AbstractionRefinement.cpp 2012-01-10 16:05:21.220610066 -0700 + BBNode a = in[i-1]; + BBNode b = in[i]; +@@ -2429,7 +2430,7 @@ namespace BEEV + { + vector evenL; + vector oddL; +- for (int i =0; i < in1.size();i++) ++ for (size_t i =0; i < in1.size();i++) + { + if (i%2 ==0) + evenL.push_back(in1[i]); +@@ -2439,7 +2440,7 @@ namespace BEEV + + vector evenR; // Take the even of each. + vector oddR; // Take the odd of each +- for (int i =0; i < in2.size();i++) ++ for (size_t i =0; i < in2.size();i++) + { + if (i%2 ==0) + evenR.push_back(in2[i]); +@@ -2450,7 +2451,7 @@ namespace BEEV + vector even = evenL.size()< evenR.size() ? mergeSorted(evenR,evenL) : mergeSorted(evenL,evenR); + vector odd = oddL.size() < oddR.size() ? mergeSorted(oddR,oddL) : mergeSorted(oddL,oddR); + +- for (int i =0; i < std::max(even.size(),odd.size());i++) ++ for (size_t i =0; i < std::max(even.size(),odd.size());i++) + { + if (even.size() > i) + result.push_back(even[i]); +@@ -2495,7 +2496,7 @@ namespace BEEV + + // check if y is already zero. + bool isZero = true; +- for (int i = 0; i < rwidth; i++) ++ for (unsigned int i = 0; i < rwidth; i++) + if (y[i] != nf->getFalse()) + { + isZero = false; +--- ./src/to-sat/AIG/BBNodeManagerAIG.h.orig 2012-01-29 20:28:39.000000000 -0700 ++++ ./src/to-sat/AIG/BBNodeManagerAIG.h 2012-08-07 16:26:11.736851970 -0600 +@@ -148,7 +148,7 @@ public: + Aig_Obj_t * pNode; + assert (children.size() != 0); + +- for (int i =0; i < children.size();i++) ++ for (size_t i =0; i < children.size();i++) + assert(!children[i].IsNull()); + + switch (kind) +--- ./src/to-sat/AIG/BBNodeAIG.h.orig 2012-02-02 20:41:30.000000000 -0700 ++++ ./src/to-sat/AIG/BBNodeAIG.h 2012-08-07 16:26:11.737851968 -0600 +@@ -11,6 +11,7 @@ + #define BBNODEAIG_H_ + + #include "../../extlib-abc/aig.h" ++#include + #include + + namespace BEEV +--- ./src/to-sat/AIG/ToSATAIG.cpp.orig 2012-04-03 00:43:00.000000000 -0600 ++++ ./src/to-sat/AIG/ToSATAIG.cpp 2012-08-07 16:26:11.737851968 -0600 +@@ -136,7 +136,7 @@ namespace BEEV + if (it != nodeToSATVar.end()) + { + const vector& v = it->second; +- for (int i = 0; i < v.size(); i++) ++ for (size_t i = 0; i < v.size(); i++) + satSolver.setFrozen(v[i]); + } + +@@ -144,7 +144,7 @@ namespace BEEV + if (it2 != nodeToSATVar.end()) + { + const vector& v = it2->second; +- for (int i = 0; i < v.size(); i++) ++ for (size_t i = 0; i < v.size(); i++) + satSolver.setFrozen(v[i]); + } + } +@@ -195,7 +195,7 @@ namespace BEEV + vector v_a; + assert(ar.index_symbol.GetKind() == SYMBOL); + // It was ommitted from the initial problem, so assign it freshly. +- for (int i = 0; i < ar.index_symbol.GetValueWidth(); i++) ++ for (unsigned int i = 0; i < ar.index_symbol.GetValueWidth(); i++) + { + SATSolver::Var v = satSolver.newVar(); + // We probably don't want the variable eliminated. +@@ -204,7 +204,7 @@ namespace BEEV + } + nodeToSATVar.insert(make_pair(ar.index_symbol, v_a)); + +- for (int i = 0; i < v_a.size(); i++) ++ for (size_t i = 0; i < v_a.size(); i++) + { + SATSolver::Var var = v_a[i]; + index.push(SATSolver::mkLit(var, false)); +@@ -220,7 +220,7 @@ namespace BEEV + if (it != nodeToSATVar.end()) + { + vector& v = it->second; +- for (int i = 0; i < v.size(); i++) ++ for (size_t i = 0; i < v.size(); i++) + { + SATSolver::Var var = v[i]; + value.push(SATSolver::mkLit(var, false)); +@@ -229,7 +229,7 @@ namespace BEEV + else if (ar.symbol.isConstant()) + { + CBV c = ar.symbol.GetBVConst(); +- for (int i = 0; i < ar.symbol.GetValueWidth(); i++) ++ for (unsigned int i = 0; i < ar.symbol.GetValueWidth(); i++) + if (CONSTANTBV::BitVector_bit_test(c, i)) + value_constants.push((Minisat::lbool) satSolver.true_literal()); + else +@@ -243,7 +243,7 @@ namespace BEEV + + assert(ar.symbol.GetKind() == SYMBOL); + // It was ommitted from the initial problem, so assign it freshly. +- for (int i = 0; i < ar.symbol.GetValueWidth(); i++) ++ for (unsigned int i = 0; i < ar.symbol.GetValueWidth(); i++) + { + SATSolver::Var v = satSolver.newVar(); + // We probably don't want the variable eliminated. +@@ -252,7 +252,7 @@ namespace BEEV + } + nodeToSATVar.insert(make_pair(ar.symbol, v_a)); + +- for (int i = 0; i < v_a.size(); i++) ++ for (size_t i = 0; i < v_a.size(); i++) + { + SATSolver::Var var = v_a[i]; + value.push(SATSolver::mkLit(var, false)); +--- ./src/to-sat/ASTNode/ToSAT.cpp.orig 2011-12-28 19:00:01.000000000 -0700 ++++ ./src/to-sat/ASTNode/ToSAT.cpp 2012-08-07 16:26:11.738851967 -0600 +@@ -52,7 +52,7 @@ namespace BEEV + + // Copies the symbol into the map that is used to build the counter example. + // For boolean we create a vector of size 1. +- if (n.GetKind() == BVGETBIT && n[0].GetKind() == SYMBOL || (n.GetKind() == SYMBOL && !isTseitinVariable(n))) ++ if ((n.GetKind() == BVGETBIT && n[0].GetKind() == SYMBOL) || (n.GetKind() == SYMBOL && !isTseitinVariable(n))) + { + const ASTNode& symbol = n.GetKind() == BVGETBIT ? n[0] : n; + const unsigned index = n.GetKind() == BVGETBIT ? n[1].GetUnsignedConst() : 0; +@@ -98,7 +98,7 @@ namespace BEEV + CountersAndStats("SAT Solver", bm); + bm->GetRunTimes()->start(RunTimes::SendingToSAT); + +- int input_clauselist_size = cll.size(); ++ // int input_clauselist_size = cll.size(); + if (cll.size() == 0) + { + FatalError("toSATandSolve: Nothing to Solve", ASTUndefined); +@@ -115,7 +115,7 @@ namespace BEEV + + //iterate through the list (conjunction) of ASTclauses cll + ClauseContainer::const_iterator i = cc.begin(), iend = cc.end(); +- for (int count=0, flag=0; i != iend; i++) ++ for (/* int count=0, flag=0 */; i != iend; i++) + { + satSolverClause.clear(); + vector::const_iterator j = (*i)->begin(); +@@ -312,7 +312,7 @@ namespace BEEV + ClauseBuckets::iterator itend = cb->end(); + + bool sat = false; +- for(int count=1;it!=itend;it++, count++) ++ for(size_t count=1;it!=itend;it++, count++) + { + ClauseList *cl = (*it).second; + sat = toSATandSolve(SatSolver,*cl, count==cb->size(),cm); +--- ./src/to-sat/ASTNode/ToCNF.cpp.orig 2011-12-28 19:00:01.000000000 -0700 ++++ ./src/to-sat/ASTNode/ToCNF.cpp 2012-08-07 16:26:11.739851966 -0600 +@@ -250,12 +250,14 @@ namespace BEEV + return psi; + } //End of SINGLETON() + ++#ifdef CRYPTOMINISAT__2 + static ASTNode GetNodeFrom_SINGLETON(ClauseList *cl) + { + ClausePtr c = (*(*cl).asList())[0]; + const ASTNode * a = (*c)[0]; + return *a; + } ++#endif + + //######################################## + //######################################## +--- ./src/absrefine_counterexample/AbstractionRefinement.cpp.orig 2012-04-25 07:40:33.000000000 -0600 ++++ ./src/absrefine_counterexample/AbstractionRefinement.cpp 2012-08-07 16:26:11.740851965 -0600 @@ -35,7 +35,7 @@ namespace BEEV { assert(a.GetKind() == SYMBOL); @@ -906,781 +860,65 @@ { const ASTNode& index_j = listOfIndices[j]; ---- ./src/to-sat/ASTNode/ToSAT.cpp.orig 2011-12-28 19:00:01.000000000 -0700 -+++ ./src/to-sat/ASTNode/ToSAT.cpp 2012-01-10 16:05:21.220610066 -0700 -@@ -52,7 +52,7 @@ namespace BEEV +@@ -556,13 +555,13 @@ namespace BEEV - // Copies the symbol into the map that is used to build the counter example. - // For boolean we create a vector of size 1. -- if (n.GetKind() == BVGETBIT && n[0].GetKind() == SYMBOL || (n.GetKind() == SYMBOL && !isTseitinVariable(n))) -+ if ((n.GetKind() == BVGETBIT && n[0].GetKind() == SYMBOL) || (n.GetKind() == SYMBOL && !isTseitinVariable(n))) + //loop over the list of indices for the array and create LA, + //and add to inputAlreadyInSAT +- for (int i = 0; i < listOfIndices.size(); i++) ++ for (size_t i = 0; i < listOfIndices.size(); i++) + { + const ASTNode& index_i = listOfIndices[i]; + const Kind iKind = index_i.GetKind(); + + // Create all distinct pairs of indexes. +- for (int j = i + 1; j < listOfIndices.size(); j++) ++ for (size_t j = i + 1; j < listOfIndices.size(); j++) { - const ASTNode& symbol = n.GetKind() == BVGETBIT ? n[0] : n; - const unsigned index = n.GetKind() == BVGETBIT ? n[1].GetUnsignedConst() : 0; -@@ -98,7 +98,7 @@ namespace BEEV - CountersAndStats("SAT Solver", bm); - bm->GetRunTimes()->start(RunTimes::SendingToSAT); + const ASTNode& index_j = listOfIndices[j]; -- int input_clauselist_size = cll.size(); -+ // int input_clauselist_size = cll.size(); - if (cll.size() == 0) - { - FatalError("toSATandSolve: Nothing to Solve", ASTUndefined); -@@ -115,7 +115,7 @@ namespace BEEV +--- ./src/absrefine_counterexample/CounterExample.cpp.orig 2012-06-15 08:40:15.000000000 -0600 ++++ ./src/absrefine_counterexample/CounterExample.cpp 2012-08-07 16:26:11.740851965 -0600 +@@ -46,7 +46,7 @@ namespace BEEV + assert(symbol.GetKind() == SYMBOL); + vector bitVector_array(symbolWidth,false); - //iterate through the list (conjunction) of ASTclauses cll - ClauseContainer::const_iterator i = cc.begin(), iend = cc.end(); -- for (int count=0, flag=0; i != iend; i++) -+ for ( ; i != iend; i++) - { - satSolverClause.clear(); - vector::const_iterator j = (*i)->begin(); -@@ -312,7 +312,7 @@ namespace BEEV - ClauseBuckets::iterator itend = cb->end(); - - bool sat = false; -- for(int count=1;it!=itend;it++, count++) -+ for(size_t count=1;it!=itend;it++, count++) - { - ClauseList *cl = (*it).second; - sat = toSATandSolve(SatSolver,*cl, count==cb->size(),cm); ---- ./src/to-sat/ASTNode/ToCNF.cpp.orig 2011-12-28 19:00:01.000000000 -0700 -+++ ./src/to-sat/ASTNode/ToCNF.cpp 2012-01-10 16:05:21.221610046 -0700 -@@ -250,12 +250,14 @@ namespace BEEV - return psi; - } //End of SINGLETON() - -+#ifdef CRYPTOMINISAT__2 - static ASTNode GetNodeFrom_SINGLETON(ClauseList *cl) - { - ClausePtr c = (*(*cl).asList())[0]; - const ASTNode * a = (*c)[0]; - return *a; - } -+#endif - - //######################################## - //######################################## ---- ./src/to-sat/BitBlaster.cpp.orig 2012-01-09 20:03:23.000000000 -0700 -+++ ./src/to-sat/BitBlaster.cpp 2012-01-10 16:06:28.158957729 -0700 -@@ -311,7 +311,7 @@ namespace BEEV - bool - BitBlaster::isConstant(const BBNodeVec& v) - { -- for (int i = 0; i < v.size(); i++) -+ for (size_t i = 0; i < v.size(); i++) - { - if (v[i] != nf->getTrue() && v[i] != nf->getFalse()) - return false; -@@ -334,7 +334,7 @@ namespace BEEV - - CBV bv = CONSTANTBV::BitVector_Create(v.size(), true); - -- for (int i = 0; i < v.size(); i++) -+ for (size_t i = 0; i < v.size(); i++) - if (v[i] == nf->getTrue()) - CONSTANTBV::BitVector_Bit_On(bv, i); - -@@ -670,14 +670,14 @@ namespace BEEV +- for (int index = 0; index < v.size(); index++) ++ for (size_t index = 0; index < v.size(); index++) { - // Add all the children up using an addition network. - vector results; -- for (int i = 0; i < term.Degree(); i++) -+ for (size_t i = 0; i < term.Degree(); i++) - results.push_back(BBTerm(term[i], support)); + const unsigned sat_variable_index = v[index]; -- const int bitWidth = term[0].GetValueWidth(); -+ const unsigned int bitWidth = term[0].GetValueWidth(); - std::vector > products(bitWidth); -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { -- for (int j = 0; j < results.size(); j++) -+ for (size_t j = 0; j < results.size(); j++) - products[i].push_back(results[j][i]); - } +@@ -863,7 +863,7 @@ namespace BEEV + ASTNode symbol = it->first; + vector v = it->second; -@@ -1157,7 +1157,7 @@ namespace BEEV - const BBNode& BBTrue = nf->getTrue(); - const BBNode& BBFalse = nf->getFalse(); - -- for (int i = 0; i < v.size(); i++) -+ for (size_t i = 0; i < v.size(); i++) +- for (int i =0 ; i < v.size();i++) ++ for (size_t i =0 ; i < v.size();i++) { - if (v[i] == BBTrue) - result[i] = ONE_MT; -@@ -1169,7 +1169,7 @@ namespace BEEV + if (v[i] == ~((unsigned)0)) // nb. special value. + continue; +--- ./src/sat/CryptoMinisat.cpp.orig 2012-08-07 16:26:07.496857705 -0600 ++++ ./src/sat/CryptoMinisat.cpp 2012-08-07 16:26:11.741851964 -0600 +@@ -44,7 +44,7 @@ namespace BEEV + for (int i =0; i= 3)) - { - result[lastOne] = MINUS_ONE_MT; -- for (int j = lastOne + 1; j < i; j++) -+ for (size_t j = lastOne + 1; j < i; j++) - result[j] = ZERO_MT; - // Should this be lastOne = i? - lastOne = i; -@@ -1193,7 +1193,7 @@ namespace BEEV - if (lastOne != -1 && (v.size() - lastOne > 1)) - { - result[lastOne] = MINUS_ONE_MT; -- for (int j = lastOne + 1; j < v.size(); j++) -+ for (size_t j = lastOne + 1; j < v.size(); j++) - result[j] = ZERO_MT; - } - } -@@ -1235,7 +1235,7 @@ namespace BEEV - BitBlaster::buildAdditionNetworkResult(list* products, set& support, - const ASTNode& n) - { -- const int bitWidth = n.GetValueWidth(); -+ const unsigned int bitWidth = n.GetValueWidth(); - - // If we have details of the partial products which can be true, - int ignore = -1; -@@ -1244,7 +1244,7 @@ namespace BEEV - ms = NULL; - - BBNodeVec results; -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - - buildAdditionNetworkResult(products[i], products[i+1], support, (i + 1 == bitWidth), (ms != NULL && (ms->sumH[i] == 0))); -@@ -1254,7 +1254,7 @@ namespace BEEV - } - - assert(products[bitWidth].size() ==0); // products[bitwidth] is defined but should never be used. -- assert(results.size() == ((unsigned)bitWidth)); -+ assert(results.size() == bitWidth); - return results; - } - -@@ -1356,7 +1356,7 @@ namespace BEEV - BitBlaster::multWithBounds(const ASTNode&n, list* products, - BBNodeSet& toConjoinToTop) - { -- const int bitWidth = n.GetValueWidth(); -+ const unsigned int bitWidth = n.GetValueWidth(); - - int ignored=0; - assert(multiplication_upper_bound); -@@ -1365,7 +1365,7 @@ namespace BEEV - - - // If all of the partial products in the column must be zero, then replace -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - if (conjoin_to_top && ms.columnH[i] == 0) - { -@@ -1387,7 +1387,7 @@ namespace BEEV - } - - vector prior; -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - if (debug_bounds) - { -@@ -1407,7 +1407,7 @@ namespace BEEV - if (debug_bitblaster) - cerr << endl << endl; - -- assert(result.size() == ((unsigned)bitWidth)); -+ assert(result.size() == bitWidth); - return result; - } - -@@ -1431,7 +1431,7 @@ namespace BEEV - } - - BBNodeVec notY; -- for (int i = 0; i < y.size(); i++) -+ for (size_t i = 0; i < y.size(); i++) - { - notY.push_back(nf->CreateNode(NOT, y[i])); - } -@@ -1484,7 +1484,7 @@ namespace BEEV - t_products[i].push_back(BBFalse); - - sort(t_products[i].begin(), t_products[i].end()); -- for (int j = 0; j < t_products[i].size(); j++) -+ for (size_t j = 0; j < t_products[i].size(); j++) - products[i].push_back(t_products[i][j]); - } - } -@@ -1542,13 +1542,13 @@ namespace BEEV - assert(ms->x.getWidth() == ms->y.getWidth()); - assert(ms->r.getWidth() == ms->y.getWidth()); - assert(ms->r.getWidth() == (int)ms->bitWidth); -- } - -- for (int i = 0; i < n.GetValueWidth(); i++) -- if (ms->sumH[i] == 0) -- highestZero = i; -+ for (unsigned int i = 0; i < n.GetValueWidth(); i++) -+ if (ms->sumH[i] == 0) -+ highestZero = (int)i; - -- return ms; -+ return ms; -+ } - } - - return NULL; -@@ -1560,7 +1560,7 @@ namespace BEEV - BitBlaster::mult_normal(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, - const ASTNode&n) - { -- const int bitWidth = n.GetValueWidth(); -+ const unsigned int bitWidth = n.GetValueWidth(); - - // If we have details of the partial products which can be true, - int highestZero = -1; -@@ -1572,7 +1572,7 @@ namespace BEEV - - BBNodeVec prod = BBNodeVec(BBAndBit(y, *x.begin())); // start prod with first partial product. - -- for (int i = 1; i < bitWidth; i++) // start loop at next bit. -+ for (unsigned int i = 1; i < bitWidth; i++) // start loop at next bit. - { - const BBNode& xit = x[i]; - -@@ -1589,7 +1589,7 @@ namespace BEEV - BBNodeVec pprod = BBAndBit(ycopy, xit); - - // Iterate through from the current location upwards, setting anything to zero that can be.. -- if (ms != NULL && highestZero >= i) -+ if (ms != NULL && highestZero >= (int)i) - { - for (int column = i; column <= highestZero; column++) - { -@@ -1614,7 +1614,7 @@ namespace BEEV - { - - // Add the carry from the prior column. i.e. each second sorted formula. -- for (int k = 1; k < priorSorted.size(); k += 2) -+ for (size_t k = 1; k < priorSorted.size(); k += 2) - { - current.push_back(priorSorted[k]); - } -@@ -1694,7 +1694,7 @@ namespace BEEV - FixedBits* b = cb->fixedMap->map->find(n)->second; - for (int i = 0; i < b->getWidth(); i++) - { -- if (b->isFixed(i)) -+ if (b->isFixed(i)) { - if (b->getValue(i)) - { - assert(v[i]== BBTrue); -@@ -1711,6 +1711,7 @@ namespace BEEV - - assert(v[i]== BBFalse); - } -+ } - } - } - } -@@ -1734,7 +1735,7 @@ namespace BEEV - y = _x; - } - -- const int bitWidth = n.GetValueWidth(); -+ const unsigned int bitWidth = n.GetValueWidth(); - assert(x.size() == bitWidth); - assert(y.size() == bitWidth); - -@@ -1762,7 +1763,7 @@ namespace BEEV - mult_Booth(_x, _y, support, n[0], n[1], products.data(), n); - vector prior; - -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - vector output; - mult_BubbleSorterWithBounds(support, products[i], output, prior); -@@ -1824,18 +1825,18 @@ namespace BEEV - vector b; - - // half way rounded up. -- const int halfWay = (((in.size()%2)==0? 0:1) + (in.size()/2) ); -- for (int i =0; i < halfWay;i++) -+ const size_t halfWay = (((in.size()%2)==0? 0:1) + (in.size()/2) ); -+ for (size_t i =0; i < halfWay;i++) - a.push_back(in[i]); - -- for (int i =halfWay; i < in.size();i++) -+ for (size_t i =halfWay; i < in.size();i++) - b.push_back(in[i]); - - assert(a.size() >= b.size()); - assert(a.size() + b.size() == in.size()); - vector result= mergeSorted(batcher(a), batcher(b)); - -- for (int k = 0; k < result.size(); k++) -+ for (size_t k = 0; k < result.size(); k++) - assert(!result[k].IsNull()); - - assert(result.size() == in.size()); -@@ -1867,7 +1868,7 @@ namespace BEEV - assert(sorted.size() == toSort.size()); - - vector sortedCarryIn; -- for (int k = 1; k < priorSorted.size(); k += 2) -+ for (size_t k = 1; k < priorSorted.size(); k += 2) - { - sortedCarryIn.push_back(priorSorted[k]); - } -@@ -1905,11 +1906,11 @@ namespace BEEV - BBNodeVec - BitBlaster::v6(list* products, set& support, const ASTNode&n) - { -- const int bitWidth = n.GetValueWidth(); -+ const unsigned int bitWidth = n.GetValueWidth(); - - vector prior; - -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - vector output; - sortingNetworkAdd(support, products[i], output ,prior); -@@ -1928,22 +1929,21 @@ namespace BEEV - BBNodeVec - BitBlaster::v9(list* products, set& support,const ASTNode&n) - { -- const int bitWidth = n.GetValueWidth(); -+ const unsigned int bitWidth = n.GetValueWidth(); - - vector< vector< BBNode> > toAdd(bitWidth); - -- for (int column = 0; column < bitWidth; column++) -+ for (unsigned int column = 0; column < bitWidth; column++) - { - vector sorted; // The current column (sorted) gets put into here. - vector prior; // Prior is always empty in this.. - -- const int size= products[column].size(); - sortingNetworkAdd(support, products[column], sorted ,prior); - - assert(products[column].size() == 1); - assert(sorted.size() == size); - -- for (int k = 2; k <= sorted.size(); k++) -+ for (size_t k = 2; k <= sorted.size(); k++) - { - BBNode part; - if (k==sorted.size()) -@@ -1958,7 +1958,7 @@ namespace BEEV - continue; // shortcut. - } - -- int position =k; -+ size_t position =k; - int increment =1; - while (position != 0) - { -@@ -1973,12 +1973,12 @@ namespace BEEV - } - } - -- for (int carry_column =column+1; carry_column < bitWidth; carry_column++) -+ for (unsigned int carry_column =column+1; carry_column < bitWidth; carry_column++) - { - if (toAdd[carry_column].size() ==0) - continue ; - BBNode disjunct = BBFalse; -- for (int l = 0; l < toAdd[carry_column].size();l++) -+ for (size_t l = 0; l < toAdd[carry_column].size();l++) - { - disjunct = nf->CreateNode(OR,disjunct,toAdd[carry_column][l]); - } -@@ -1988,7 +1988,7 @@ namespace BEEV - toAdd[carry_column].clear(); - } - } -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - assert(toAdd[i].size() == 0); - } -@@ -2002,7 +2002,7 @@ namespace BEEV - BBNodeVec - BitBlaster::v7(list* products, set& support, const ASTNode&n) - { -- const int bitWidth = n.GetValueWidth(); -+ const unsigned int bitWidth = n.GetValueWidth(); - - // If we have details of the partial products which can be true, - int ignore = -1; -@@ -2014,13 +2014,13 @@ namespace BEEV - std::vector > later(bitWidth+1); - std::vector > next(bitWidth+1); - -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - next[i+1].clear(); - buildAdditionNetworkResult(products[i], next[i + 1], support, bitWidth == i+1, (ms!=NULL && (ms->sumH[i]==0))); - - // Calculate the carries of carries. -- for (int j = i + 1; j < bitWidth; j++) -+ for (unsigned int j = i + 1; j < bitWidth; j++) - { - if (next[j].size() == 0) - break; -@@ -2030,7 +2030,7 @@ namespace BEEV - } - - // Put the carries of the carries away until later. -- for (int j = i + 1; j < bitWidth; j++) -+ for (unsigned int j = i + 1; j < bitWidth; j++) - { - if (next[j].size() == 0) - break; -@@ -2041,7 +2041,7 @@ namespace BEEV - } - - -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - // Copy all the laters into products - while(later[i].size() > 0) -@@ -2052,7 +2052,7 @@ namespace BEEV - } - - BBNodeVec results; -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - - buildAdditionNetworkResult((products[i]), (products[i + 1]), support, bitWidth == i+1, false); -@@ -2062,7 +2062,7 @@ namespace BEEV - products[i].pop_back(); - } - -- assert(results.size() == ((unsigned)bitWidth)); -+ assert(results.size() == bitWidth); - return results; +- s->addClause(v); ++ return s->addClause(v); } -@@ -2071,7 +2071,7 @@ namespace BEEV - BBNodeVec - BitBlaster::v8(list* products, set& support, const ASTNode&n) - { -- const int bitWidth = n.GetValueWidth(); -+ const unsigned int bitWidth = n.GetValueWidth(); - - // If we have details of the partial products which can be true, - int ignore = -1; -@@ -2084,14 +2084,14 @@ namespace BEEV - std::vector > later(bitWidth+1); // +1 then ignore the topmost. - std::vector > next(bitWidth+1); - -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - // Put all the products into next. - next[i+1].clear(); - buildAdditionNetworkResult((products[i]), (next[i + 1]), support, i+1 ==bitWidth, (ms!=NULL && (ms->sumH[i]==0))); - - // Calculate the carries of carries. -- for (int j = i + 1; j < bitWidth; j++) -+ for (unsigned int j = i + 1; j < bitWidth; j++) - { - if (next[j].size() == 0) - break; -@@ -2101,7 +2101,7 @@ namespace BEEV - } - - // Put the carries of the carries away until later. -- for (int j = i + 1; j < bitWidth; j++) -+ for (unsigned int j = i + 1; j < bitWidth; j++) - { - if (next[j].size() == 0) - break; -@@ -2112,7 +2112,7 @@ namespace BEEV - } - - -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - // Copy all the laters into products - while(later[i].size() > 0) -@@ -2123,14 +2123,14 @@ namespace BEEV - } - - BBNodeVec results; -- for (int i = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - buildAdditionNetworkResult(products[i], products[i + 1], support, i+1 ==bitWidth, false); - results.push_back(products[i].back()); - products[i].pop_back(); - } - -- assert(results.size() == ((unsigned)bitWidth)); -+ assert(results.size() == bitWidth); - return results; + bool +@@ -71,7 +71,7 @@ namespace BEEV + return s->newVar(); } -@@ -2142,7 +2142,7 @@ namespace BEEV - { - vector result(in); - -- for (int i = 2; i < in.size(); i =i+ 2) -+ for (size_t i = 2; i < in.size(); i =i+ 2) - { - BBNode a = in[i-1]; - BBNode b = in[i]; -@@ -2179,7 +2179,7 @@ namespace BEEV - { - vector evenL; - vector oddL; -- for (int i =0; i < in1.size();i++) -+ for (size_t i =0; i < in1.size();i++) - { - if (i%2 ==0) - evenL.push_back(in1[i]); -@@ -2189,7 +2189,7 @@ namespace BEEV - - vector evenR; // Take the even of each. - vector oddR; // Take the odd of each -- for (int i =0; i < in2.size();i++) -+ for (size_t i =0; i < in2.size();i++) - { - if (i%2 ==0) - evenR.push_back(in2[i]); -@@ -2200,7 +2200,7 @@ namespace BEEV - vector even = evenL.size()< evenR.size() ? mergeSorted(evenR,evenL) : mergeSorted(evenL,evenR); - vector odd = oddL.size() < oddR.size() ? mergeSorted(oddR,oddL) : mergeSorted(oddL,oddR); - -- for (int i =0; i < std::max(even.size(),odd.size());i++) -+ for (size_t i =0; i < std::max(even.size(),odd.size());i++) - { - if (even.size() > i) - result.push_back(even[i]); -@@ -2245,7 +2245,7 @@ namespace BEEV - - // check if y is already zero. - bool isZero = true; -- for (int i = 0; i < rwidth; i++) -+ for (unsigned int i = 0; i < rwidth; i++) - if (y[i] != nf->getFalse()) - { - isZero = false; ---- ./src/to-sat/AIG/BBNodeManagerAIG.h.orig 2011-02-01 22:39:54.000000000 -0700 -+++ ./src/to-sat/AIG/BBNodeManagerAIG.h 2012-01-10 16:05:21.224609986 -0700 -@@ -142,7 +142,7 @@ public: - Aig_Obj_t * pNode; - assert (children.size() != 0); - -- for (int i =0; i < children.size();i++) -+ for (size_t i =0; i < children.size();i++) - assert(!children[i].IsNull()); - - switch (kind) ---- ./src/to-sat/AIG/ToSATAIG.cpp.orig 2011-12-31 07:51:52.000000000 -0700 -+++ ./src/to-sat/AIG/ToSATAIG.cpp 2012-01-10 16:05:21.225609966 -0700 -@@ -126,7 +126,7 @@ namespace BEEV - if (it != nodeToSATVar.end()) - { - const vector& v = it->second; -- for (int i = 0; i < v.size(); i++) -+ for (size_t i = 0; i < v.size(); i++) - satSolver.setFrozen(v[i]); - } - -@@ -134,7 +134,7 @@ namespace BEEV - if (it2 != nodeToSATVar.end()) - { - const vector& v = it2->second; -- for (int i = 0; i < v.size(); i++) -+ for (size_t i = 0; i < v.size(); i++) - satSolver.setFrozen(v[i]); - } - } -@@ -185,7 +185,7 @@ namespace BEEV - vector v_a; - assert(ar.index_symbol.GetKind() == SYMBOL); - // It was ommitted from the initial problem, so assign it freshly. -- for (int i = 0; i < ar.index_symbol.GetValueWidth(); i++) -+ for (unsigned int i = 0; i < ar.index_symbol.GetValueWidth(); i++) - { - SATSolver::Var v = satSolver.newVar(); - // We probably don't want the variable eliminated. -@@ -194,7 +194,7 @@ namespace BEEV - } - nodeToSATVar.insert(make_pair(ar.index_symbol, v_a)); - -- for (int i = 0; i < v_a.size(); i++) -+ for (size_t i = 0; i < v_a.size(); i++) - { - SATSolver::Var var = v_a[i]; - index.push(SATSolver::mkLit(var, false)); -@@ -210,7 +210,7 @@ namespace BEEV - if (it != nodeToSATVar.end()) - { - vector& v = it->second; -- for (int i = 0; i < v.size(); i++) -+ for (size_t i = 0; i < v.size(); i++) - { - SATSolver::Var var = v[i]; - value.push(SATSolver::mkLit(var, false)); -@@ -219,7 +219,7 @@ namespace BEEV - else if (ar.symbol.isConstant()) - { - CBV c = ar.symbol.GetBVConst(); -- for (int i = 0; i < ar.symbol.GetValueWidth(); i++) -+ for (unsigned int i = 0; i < ar.symbol.GetValueWidth(); i++) - if (CONSTANTBV::BitVector_bit_test(c, i)) - value_constants.push((Minisat::lbool) satSolver.true_literal()); - else -@@ -233,7 +233,7 @@ namespace BEEV - - assert(ar.symbol.GetKind() == SYMBOL); - // It was ommitted from the initial problem, so assign it freshly. -- for (int i = 0; i < ar.symbol.GetValueWidth(); i++) -+ for (unsigned int i = 0; i < ar.symbol.GetValueWidth(); i++) - { - SATSolver::Var v = satSolver.newVar(); - // We probably don't want the variable eliminated. -@@ -242,7 +242,7 @@ namespace BEEV - } - nodeToSATVar.insert(make_pair(ar.symbol, v_a)); - -- for (int i = 0; i < v_a.size(); i++) -+ for (size_t i = 0; i < v_a.size(); i++) - { - SATSolver::Var var = v_a[i]; - value.push(SATSolver::mkLit(var, false)); ---- ./src/c_interface/c_interface.cpp.orig 2011-12-21 22:12:52.000000000 -0700 -+++ ./src/c_interface/c_interface.cpp 2012-01-10 16:05:21.225609966 -0700 -@@ -516,7 +516,6 @@ void vc_printCounterExample(VC vc) { - - Expr vc_getCounterExample(VC vc, Expr e) { - nodestar a = (nodestar)e; -- bmstar b = (bmstar)(((stpstar)vc)->bm); - ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); - - bool t = false; -@@ -529,7 +528,6 @@ Expr vc_getCounterExample(VC vc, Expr e) - - void vc_getCounterExampleArray(VC vc, Expr e, Expr **indices, Expr **values, int *size) { - nodestar a = (nodestar)e; -- bmstar b = (bmstar)(((stpstar)vc)->bm); - ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); - - bool t = false; -@@ -549,7 +547,6 @@ void vc_getCounterExampleArray(VC vc, Ex - } - - int vc_counterexample_size(VC vc) { -- bmstar b = (bmstar)(((stpstar)vc)->bm); - ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); - - return ce->CounterExampleSize(); -@@ -941,7 +938,7 @@ Expr vc_bvConstExprFromInt(VC vc, - bmstar b = (bmstar)(((stpstar)vc)->bm); - - unsigned long long int v = (unsigned long long int)value; -- unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> 64-n_bits; -+ unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> (64-n_bits); - //printf("%ull", max_n_bits); - if(v > max_n_bits) { - printf("CInterface: vc_bvConstExprFromInt: "\ -@@ -1484,16 +1481,11 @@ Expr vc_bvWriteToMemoryArray(VC vc, - return vc_writeExpr(vc, array, byteIndex, element); - else { - int count = 1; -- int hi = newBitsPerElem - 1; -- int low = newBitsPerElem - 8; - int low_elem = 0; - int hi_elem = low_elem + 7; - Expr c = vc_bvExtract(vc, element, hi_elem, low_elem); - Expr newarray = vc_writeExpr(vc, array, byteIndex, c); - while(--numOfBytes > 0) { -- hi = low-1; -- low = low-8; -- - low_elem = low_elem + 8; - hi_elem = low_elem + 7; - -@@ -1668,7 +1660,6 @@ int vc_isBool(Expr e) { - } - - void vc_Destroy(VC vc) { -- bmstar b = (bmstar)(((stpstar)vc)->bm); - // for(std::vector::iterator it=created_exprs.begin(), - // itend=created_exprs.end();it!=itend;it++) { - // BEEV::ASTNode * aaa = *it; ---- ./src/printer/SMTLIB2Printer.cpp.orig 2010-07-10 08:49:13.000000000 -0600 -+++ ./src/printer/SMTLIB2Printer.cpp 2012-01-10 16:05:21.226609946 -0700 -@@ -210,7 +210,7 @@ void printVarDeclsToStream(ASTNodeSet& s - { - string close = ""; - -- for (int i =0; i < c.size()-1; i++) -+ for (size_t i =0; i < c.size()-1; i++) - { - os << "(" << functionToSMTLIBName(kind,false); - os << " "; ---- ./src/printer/SMTLIB1Printer.cpp.orig 2010-06-24 23:19:52.000000000 -0600 -+++ ./src/printer/SMTLIB1Printer.cpp 2012-01-10 16:05:21.226609946 -0700 -@@ -214,7 +214,7 @@ void printSMTLIB1VarDeclsToStream(ASTNod - { - string close = ""; - -- for (int i =0; i < c.size()-1; i++) -+ for (size_t i =0; i < c.size()-1; i++) - { - os << "(" << functionToSMTLIBName(kind,true); - os << " "; ---- ./src/printer/SMTLIBPrinter.h.orig 2010-05-23 20:03:46.000000000 -0600 -+++ ./src/printer/SMTLIBPrinter.h 2012-01-10 16:05:21.227609925 -0700 -@@ -24,7 +24,5 @@ namespace printer - ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB_Print1)(ostream&, const ASTNode , int , bool ), bool smtlib1); - - bool containsAnyArrayOps(const ASTNode& n); -- -- static string tolower(const char * name); - }; - #endif ---- ./src/sat/SimplifyingMinisat.h.orig 2012-01-09 21:59:09.000000000 -0700 -+++ ./src/sat/SimplifyingMinisat.h 2012-01-10 16:05:21.227609925 -0700 -@@ -34,7 +34,7 @@ namespace BEEV - bool - simplify(); // Removes already satisfied clauses. - -- int setVerbosity(int v); -+ void setVerbosity(int v); - - virtual uint8_t modelValue(Var x) const; - ---- ./src/sat/SATSolver.h.orig 2012-01-09 21:59:09.000000000 -0700 -+++ ./src/sat/SATSolver.h 2012-01-10 16:05:21.227609925 -0700 -@@ -61,7 +61,7 @@ namespace BEEV - exit(1); - } - -- virtual int setVerbosity(int v) =0; -+ virtual void setVerbosity(int v) =0; - - virtual lbool true_literal() =0; - virtual lbool false_literal() =0; ---- ./src/sat/MinisatCore_prop.h.orig 2012-01-09 21:59:09.000000000 -0700 -+++ ./src/sat/MinisatCore_prop.h 2012-01-10 16:05:21.227609925 -0700 -@@ -43,7 +43,7 @@ namespace BEEV +- int CryptoMinisat::setVerbosity(int v) ++ void CryptoMinisat::setVerbosity(int v) + { + s->conf.verbosity = v; + } +--- ./src/sat/MinisatCore_prop.h.orig 2012-03-11 22:07:37.000000000 -0600 ++++ ./src/sat/MinisatCore_prop.h 2012-08-07 16:26:11.741851964 -0600 +@@ -40,7 +40,7 @@ namespace BEEV virtual Var newVar(); @@ -1689,8 +927,8 @@ int nVars(); ---- ./src/sat/SimplifyingMinisat.cpp.orig 2012-01-09 21:59:09.000000000 -0700 -+++ ./src/sat/SimplifyingMinisat.cpp 2012-01-10 16:05:21.228609904 -0700 +--- ./src/sat/SimplifyingMinisat.cpp.orig 2012-01-23 21:26:37.000000000 -0700 ++++ ./src/sat/SimplifyingMinisat.cpp 2012-08-07 16:26:11.741851964 -0600 @@ -17,7 +17,7 @@ namespace BEEV bool SimplifyingMinisat::addClause(const vec_literals& ps) // Add a clause to the solver. @@ -1709,60 +947,81 @@ { s->verbosity = v; } ---- ./src/sat/cryptominisat2/Logger.cpp.orig 2010-06-04 12:11:26.000000000 -0600 -+++ ./src/sat/cryptominisat2/Logger.cpp 2012-01-10 16:05:21.228609904 -0700 -@@ -372,8 +372,9 @@ void Logger::end(const finish_type finis - fprintf(proof,"}\n"); - history.push_back(uniqueid); - -- proof = (FILE*)fclose(proof); -- assert(proof == NULL); -+ int err = fclose(proof); -+ assert(err == 0); -+ proof = NULL; - } - - if (statistics_on) { ---- ./src/sat/cryptominisat2/FailedVarSearcher.cpp.orig 2010-07-02 08:35:28.000000000 -0600 -+++ ./src/sat/cryptominisat2/FailedVarSearcher.cpp 2012-01-10 16:05:21.229609884 -0700 -@@ -261,7 +261,6 @@ const bool FailedVarSearcher::search(uin - }*/ - - end: -- bool removedOldLearnts = false; - binClauseAdded = solver.binaryClauses.size() - origBinClauses; - //Print results - if (solver.verbosity >= 1) printResults(myTime); -@@ -272,7 +271,6 @@ end: - double time = cpuTime(); - if ((int)origHeapSize - (int)solver.order_heap.size() > (int)origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) { - completelyDetachAndReattach(); -- removedOldLearnts = true; - } else { - solver.clauseCleaner->removeAndCleanAll(); +--- ./src/sat/utils/Options.h.orig 2010-11-27 19:45:43.000000000 -0700 ++++ ./src/sat/utils/Options.h 2012-08-07 16:26:11.742851962 -0600 +@@ -60,7 +60,7 @@ class Option + struct OptionLt { + bool operator()(const Option* x, const Option* y) { + int test1 = strcmp(x->category, y->category); +- return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0; ++ return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0); } ---- ./src/sat/CryptoMinisat.cpp.orig 2010-08-20 06:07:42.000000000 -0600 -+++ ./src/sat/CryptoMinisat.cpp 2012-01-10 16:05:21.230609864 -0700 -@@ -34,7 +34,7 @@ namespace BEEV - for (int i =0; iaddClause(v); -+ return s->addClause(v); - } + }; +--- ./src/sat/MinisatCore.cpp.orig 2012-03-11 18:12:51.000000000 -0600 ++++ ./src/sat/MinisatCore.cpp 2012-08-07 16:27:00.075801722 -0600 +@@ -22,7 +22,7 @@ namespace BEEV bool -@@ -61,7 +61,7 @@ namespace BEEV - return s->newVar(); + MinisatCore::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver. + { +- s->addClause(ps); ++ return s->addClause(ps); } -- int CryptoMinisat::setVerbosity(int v) -+ void CryptoMinisat::setVerbosity(int v) + template +@@ -58,7 +58,7 @@ namespace BEEV + } + + template +- int MinisatCore::setVerbosity(int v) ++ void MinisatCore::setVerbosity(int v) { s->verbosity = v; } ---- ./src/sat/core_prop/Solver_prop.cc.orig 2011-11-27 19:55:18.000000000 -0700 -+++ ./src/sat/core_prop/Solver_prop.cc 2012-01-10 16:05:21.230609864 -0700 +@@ -97,7 +97,7 @@ namespace BEEV + template + bool MinisatCore::simplify() + { +- s->simplify(); ++ return s->simplify(); + } + + +--- ./src/sat/MinisatCore.h.orig 2012-04-19 19:01:00.000000000 -0600 ++++ ./src/sat/MinisatCore.h 2012-08-07 16:26:11.743851961 -0600 +@@ -47,7 +47,7 @@ namespace BEEV + + virtual Var newVar(); + +- int setVerbosity(int v); ++ void setVerbosity(int v); + + int nVars(); + +--- ./src/sat/SimplifyingMinisat.h.orig 2012-01-23 21:26:37.000000000 -0700 ++++ ./src/sat/SimplifyingMinisat.h 2012-08-07 16:26:11.743851961 -0600 +@@ -34,7 +34,7 @@ namespace BEEV + bool + simplify(); // Removes already satisfied clauses. + +- int setVerbosity(int v); ++ void setVerbosity(int v); + + virtual uint8_t modelValue(Var x) const; + +--- ./src/sat/SATSolver.h.orig 2012-03-11 18:12:51.000000000 -0600 ++++ ./src/sat/SATSolver.h 2012-08-07 16:26:11.743851961 -0600 +@@ -61,7 +61,7 @@ namespace BEEV + exit(1); + } + +- virtual int setVerbosity(int v) =0; ++ virtual void setVerbosity(int v) =0; + + virtual lbool true_literal() =0; + virtual lbool false_literal() =0; +--- ./src/sat/core_prop/Solver_prop.cc.orig 2012-05-25 07:36:17.000000000 -0600 ++++ ./src/sat/core_prop/Solver_prop.cc 2012-08-07 16:26:11.744851960 -0600 @@ -171,11 +171,11 @@ Solver_prop::addArray(int array_id, cons if (!ok) return false; @@ -1777,7 +1036,7 @@ "Unfortunately your problem has array indexes of size %d bits. " "STP does arbitrary precision indices with the '--oldstyle-refinement' or the '-r' flags.\n", INDEX_BIT_WIDTH, std::max(i.size(), ki.size())); -@@ -1167,7 +1167,6 @@ void Solver_prop::analyze(CRef confl, ve +@@ -1136,7 +1136,6 @@ void Solver_prop::analyze(CRef confl, ve if (debug_print) printf("%d %d\n", toInt(p), toInt(var(p))); @@ -1785,8 +1044,8 @@ assert(ca[confl][0] ==p); assert(value(p) != l_Undef); ---- ./src/sat/core_prop/Solver_prop.h.orig 2011-11-27 19:55:18.000000000 -0700 -+++ ./src/sat/core_prop/Solver_prop.h 2012-01-10 16:05:21.231609844 -0700 +--- ./src/sat/core_prop/Solver_prop.h.orig 2012-01-23 21:26:37.000000000 -0700 ++++ ./src/sat/core_prop/Solver_prop.h 2012-08-07 16:26:11.745851958 -0600 @@ -36,8 +36,10 @@ namespace Minisat { typedef unsigned int uint128_t __attribute__((mode(TI))); static inline uint32_t hash(uint128_t x){ return (uint32_t)x; } @@ -1807,39 +1066,40 @@ printf("Known Value: %c\n", isValueConstant() ? 't' : 'f'); printf("Array ID:%d\n", array_id); printf("------------\n"); ---- ./src/sat/utils/Options.h.orig 2010-11-27 19:45:43.000000000 -0700 -+++ ./src/sat/utils/Options.h 2012-01-10 16:05:21.231609844 -0700 -@@ -60,7 +60,7 @@ class Option - struct OptionLt { - bool operator()(const Option* x, const Option* y) { - int test1 = strcmp(x->category, y->category); -- return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0; -+ return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0); +--- ./src/sat/cryptominisat2/FailedVarSearcher.cpp.orig 2010-07-02 08:35:28.000000000 -0600 ++++ ./src/sat/cryptominisat2/FailedVarSearcher.cpp 2012-08-07 16:26:11.746851956 -0600 +@@ -261,7 +261,6 @@ const bool FailedVarSearcher::search(uin + }*/ + + end: +- bool removedOldLearnts = false; + binClauseAdded = solver.binaryClauses.size() - origBinClauses; + //Print results + if (solver.verbosity >= 1) printResults(myTime); +@@ -272,7 +271,6 @@ end: + double time = cpuTime(); + if ((int)origHeapSize - (int)solver.order_heap.size() > (int)origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) { + completelyDetachAndReattach(); +- removedOldLearnts = true; + } else { + solver.clauseCleaner->removeAndCleanAll(); } - }; +--- ./src/sat/cryptominisat2/Logger.cpp.orig 2010-06-04 12:11:26.000000000 -0600 ++++ ./src/sat/cryptominisat2/Logger.cpp 2012-08-07 16:26:11.747851955 -0600 +@@ -372,8 +372,9 @@ void Logger::end(const finish_type finis + fprintf(proof,"}\n"); + history.push_back(uniqueid); ---- ./src/sat/MinisatCore.cpp.orig 2012-01-09 21:59:09.000000000 -0700 -+++ ./src/sat/MinisatCore.cpp 2012-01-10 16:05:21.231609844 -0700 -@@ -22,7 +22,7 @@ namespace BEEV - bool - MinisatCore::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver. - { -- s->addClause(ps); -+ return s->addClause(ps); - } +- proof = (FILE*)fclose(proof); +- assert(proof == NULL); ++ int err = fclose(proof); ++ assert(err == 0); ++ proof = NULL; + } - template -@@ -58,7 +58,7 @@ namespace BEEV - } - - template -- int MinisatCore::setVerbosity(int v) -+ void MinisatCore::setVerbosity(int v) - { - s->verbosity = v; - } ---- ./src/sat/MinisatCore_prop.cpp.orig 2012-01-09 21:59:09.000000000 -0700 -+++ ./src/sat/MinisatCore_prop.cpp 2012-01-10 16:05:21.232609824 -0700 + if (statistics_on) { +--- ./src/sat/MinisatCore_prop.cpp.orig 2012-01-23 21:26:37.000000000 -0700 ++++ ./src/sat/MinisatCore_prop.cpp 2012-08-07 16:26:11.747851955 -0600 @@ -30,7 +30,7 @@ namespace BEEV bool MinisatCore_prop::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver. @@ -1858,9 +1118,9 @@ { s->verbosity = v; } ---- ./src/sat/CryptoMinisat.h.orig 2012-01-09 21:59:09.000000000 -0700 -+++ ./src/sat/CryptoMinisat.h 2012-01-10 16:05:21.232609824 -0700 -@@ -36,7 +36,7 @@ namespace BEEV +--- ./src/sat/CryptoMinisat.h.orig 2012-08-07 16:26:07.497857703 -0600 ++++ ./src/sat/CryptoMinisat.h 2012-08-07 16:26:11.747851955 -0600 +@@ -33,7 +33,7 @@ namespace BEEV virtual Var newVar(); @@ -1869,107 +1129,135 @@ int nVars(); ---- ./src/sat/MinisatCore.h.orig 2012-01-09 21:59:09.000000000 -0700 -+++ ./src/sat/MinisatCore.h 2012-01-10 16:05:21.232609824 -0700 -@@ -40,7 +40,7 @@ namespace BEEV +--- ./src/printer/SMTLIBPrinter.h.orig 2010-05-23 20:03:46.000000000 -0600 ++++ ./src/printer/SMTLIBPrinter.h 2012-08-07 16:26:11.748851954 -0600 +@@ -24,7 +24,5 @@ namespace printer + ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB_Print1)(ostream&, const ASTNode , int , bool ), bool smtlib1); - virtual Var newVar(); + bool containsAnyArrayOps(const ASTNode& n); +- +- static string tolower(const char * name); + }; + #endif +--- ./src/printer/SMTLIB2Printer.cpp.orig 2012-04-04 19:13:21.000000000 -0600 ++++ ./src/printer/SMTLIB2Printer.cpp 2012-08-07 16:26:11.748851954 -0600 +@@ -213,7 +213,7 @@ void printVarDeclsToStream(ASTNodeSet& s + { + string close = ""; -- int setVerbosity(int v); -+ void setVerbosity(int v); +- for (int i =0; i < c.size()-1; i++) ++ for (size_t i =0; i < c.size()-1; i++) + { + os << "(" << functionToSMTLIBName(kind,false); + os << " "; +--- ./src/printer/SMTLIB1Printer.cpp.orig 2010-06-24 23:19:52.000000000 -0600 ++++ ./src/printer/SMTLIB1Printer.cpp 2012-08-07 16:26:11.749851953 -0600 +@@ -214,7 +214,7 @@ void printSMTLIB1VarDeclsToStream(ASTNod + { + string close = ""; - int nVars(); +- for (int i =0; i < c.size()-1; i++) ++ for (size_t i =0; i < c.size()-1; i++) + { + os << "(" << functionToSMTLIBName(kind,true); + os << " "; +--- ./src/cpp_interface/cpp_interface.h.orig 2012-06-15 08:28:01.000000000 -0600 ++++ ./src/cpp_interface/cpp_interface.h 2012-08-07 16:26:11.750851951 -0600 +@@ -197,7 +197,7 @@ namespace BEEV + { + bool removed=false; ---- ./src/extlib-abc/kit.h.orig 2011-02-09 18:31:59.000000000 -0700 -+++ ./src/extlib-abc/kit.h 2012-01-10 16:05:21.232609824 -0700 -@@ -53,11 +53,15 @@ struct Kit_Sop_t_ - unsigned * pCubes; // the storage for cubes - }; - --typedef struct Kit_Edge_t_ Kit_Edge_t; --struct Kit_Edge_t_ -+typedef union Kit_Edge_t_ Kit_Edge_t; -+union Kit_Edge_t_ +- for (int i=0; i < symbols.back().size(); i++) ++ for (size_t i=0; i < symbols.back().size(); i++) + if (symbols.back()[i] == s) + { + symbols.back().erase(symbols.back().begin() + i); +@@ -218,7 +218,7 @@ namespace BEEV + f.name = name; + + ASTNodeMap fromTo; +- for (int i=0; i < params.size();i++) ++ for (size_t i=0; i < params.size();i++) + { + ASTNode p = bm.CreateFreshVariable(params[i].GetIndexWidth(), params[i].GetValueWidth(), "STP_INTERNAL_FUNCTION_NAME"); + fromTo.insert(make_pair(params[i], p)); +@@ -239,7 +239,7 @@ namespace BEEV + f = functions[string(name)]; + + ASTNodeMap fromTo; +- for (int i=0; i < f.params.size();i++) ++ for (size_t i=0; i < f.params.size();i++) + { + if (f.params[i].GetValueWidth() != params[i].GetValueWidth()) + FatalError("Actual parameters differ from formal"); +@@ -371,7 +371,7 @@ namespace BEEV + + cache.erase(cache.end() - 1); + ASTVec & current = symbols.back(); +- for (int i = 0; i < current.size(); i++) ++ for (size_t i = 0; i < current.size(); i++) + letMgr._parser_symbol_table.erase(current[i]); + symbols.erase(symbols.end() - 1); + checkInvariant(); +@@ -402,7 +402,7 @@ namespace BEEV + void + printStatus() + { +- for (int i = 0; i < cache.size(); i++) ++ for (size_t i = 0; i < cache.size(); i++) + { + cache[i].print(); + } +--- ./src/extlib-abc/aig/aig/aigShow.c.orig 2010-03-06 06:48:41.000000000 -0700 ++++ ./src/extlib-abc/aig/aig/aigShow.c 2012-08-07 16:38:04.988829249 -0600 +@@ -329,7 +329,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, + void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) { -- unsigned fCompl : 1; // the complemented bit -- unsigned Node : 30; // the decomposition node pointed by the edge -+ struct { -+ unsigned fCompl : 1; // the complemented bit -+ unsigned Node : 30; // the decomposition node pointed by the edge -+ } edgeBits; + extern void Abc_ShowFile( char * FileNameDot ); +- static Counter = 0; ++ static int Counter = 0; + char FileNameDot[200]; + FILE * pFile; + // create the file name +--- ./src/extlib-abc/aig/aig/aigObj.c.orig 2010-03-06 06:48:41.000000000 -0700 ++++ ./src/extlib-abc/aig/aig/aigObj.c 2012-08-07 16:26:11.750851951 -0600 +@@ -299,8 +299,10 @@ void Aig_NodeFixBufferFanins( Aig_Man_t + pResult = Aig_Oper( p, pFanReal0, pFanReal1, Aig_ObjType(pObj) ); + // else if ( Aig_ObjIsLatch(pObj) ) + // pResult = Aig_Latch( p, pFanReal0, Aig_ObjInit(pObj) ); +- else ++ else { + assert( 0 ); ++ pResult = NULL; ++ } + // replace the node with buffer by the node without buffer + Aig_ObjReplace( p, pObj, pResult, fNodesOnly, fUpdateLevel ); + } +--- ./src/extlib-abc/aig/aig/aigTable.c.orig 2010-03-06 06:48:41.000000000 -0700 ++++ ./src/extlib-abc/aig/aig/aigTable.c 2012-08-07 16:26:11.750851951 -0600 +@@ -74,8 +74,8 @@ void Aig_TableResize( Aig_Man_t * p ) + { + Aig_Obj_t * pEntry, * pNext; + Aig_Obj_t ** pTableOld, ** ppPlace; +- int nTableSizeOld, Counter, i, clk; +-clk = clock(); ++ int nTableSizeOld, Counter, i; + -+ unsigned int edgeInt; - }; + // save the old table + pTableOld = p->pTable; + nTableSizeOld = p->nTableSize; +--- ./src/extlib-abc/aig/cnf/cnfWrite.c.orig 2011-01-07 21:23:57.000000000 -0700 ++++ ./src/extlib-abc/aig/cnf/cnfWrite.c 2012-08-07 16:26:11.751851950 -0600 +@@ -352,7 +352,6 @@ Cnf_Dat_t * Cnf_DeriveSimple_Additional( + int Number = old->nVars+1; - typedef struct Kit_Node_t_ Kit_Node_t; -@@ -203,18 +207,18 @@ static inline void Kit_SopShrink - static inline void Kit_SopPushCube( Kit_Sop_t * cSop, unsigned uCube ) { cSop->pCubes[cSop->nCubes++] = uCube; } - static inline void Kit_SopWriteCube( Kit_Sop_t * cSop, unsigned uCube, int i ) { cSop->pCubes[i] = uCube; } - --static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { fCompl, Node }; return eEdge; } --static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.Node << 1) | eEdge.fCompl; } -+static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { { fCompl, Node } }; return eEdge; } -+static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.edgeBits.Node << 1) | eEdge.edgeBits.fCompl; } - static inline Kit_Edge_t Kit_IntToEdge( unsigned Edge ) { return Kit_EdgeCreate( Edge >> 1, Edge & 1 ); } --static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return *(unsigned *)&eEdge; } --static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { return *(Kit_Edge_t *)&Edge; } -+static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return eEdge.edgeInt; } -+static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { Kit_Edge_t eEdge; eEdge.edgeInt = Edge; return eEdge; } - - static inline int Kit_GraphIsConst( Kit_Graph_t * pGraph ) { return pGraph->fConst; } --static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.fCompl; } --static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.fCompl; } --static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.fCompl; } --static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; } --static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.fCompl ^= 1; } -+static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.edgeBits.fCompl; } -+static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.edgeBits.fCompl; } -+static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.edgeBits.fCompl; } -+static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.edgeBits.Node < (unsigned)pGraph->nLeaves; } -+static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.edgeBits.fCompl ^= 1; } - static inline void Kit_GraphSetRoot( Kit_Graph_t * pGraph, Kit_Edge_t eRoot ) { pGraph->eRoot = eRoot; } - static inline int Kit_GraphLeaveNum( Kit_Graph_t * pGraph ) { return pGraph->nLeaves; } - static inline int Kit_GraphNodeNum( Kit_Graph_t * pGraph ) { return pGraph->nSize - pGraph->nLeaves; } -@@ -222,14 +226,12 @@ static inline Kit_Node_t * Kit_GraphNode - static inline Kit_Node_t * Kit_GraphNodeLast( Kit_Graph_t * pGraph ) { return pGraph->pNodes + pGraph->nSize - 1; } - static inline int Kit_GraphNodeInt( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return pNode - pGraph->pNodes; } - static inline int Kit_GraphNodeIsVar( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; } --static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.Node ); } -+static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.edgeBits.Node ); } - static inline int Kit_GraphVarInt( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); } --static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node); } --static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node); } --static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level; } -+static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node); } -+static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node); } -+static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.edgeBits.Node)->Level; } - --static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); } --static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); } - static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); } - static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } - static inline unsigned Kit_BitMask( int nBits ) { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits); } -@@ -486,6 +488,18 @@ static inline void Kit_TruthIthVar( unsi - /// FUNCTION DECLARATIONS /// - //////////////////////////////////////////////////////////////////////// - -+extern Kit_Graph_t * Kit_GraphCreateConst0( void ); -+extern Kit_Graph_t * Kit_GraphCreateConst1( void ); -+extern void Kit_GraphFree( Kit_Graph_t * ); -+extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t *, int, int, Vec_Int_t * ); -+extern void Kit_TruthCofactor0( unsigned *, int, int ); -+extern void Kit_TruthCofactor1( unsigned *, int, int ); -+extern int Kit_TruthIsop( unsigned *, int, Vec_Int_t *, int ); -+extern void Kit_TruthShrink( unsigned *, unsigned *, int, int, unsigned, int ); -+extern void Kit_TruthStretch( unsigned *, unsigned *, int, int, unsigned, int ); -+extern Kit_Graph_t * Kit_TruthToGraph( unsigned *, int, Vec_Int_t * ); -+extern int Kit_TruthVarInSupport( unsigned *, int, int ); -+ - #if 0 - - /*=== kitBdd.c ==========================================================*/ + // assign variables to the PIs +- int newPI = 0; + Aig_ManForEachPi( p, pObj, i ) + if (pCnf->pVarNums[pObj->Id] == -1) // new! + pCnf->pVarNums[pObj->Id] = Number++; --- ./src/extlib-abc/aig/kit/kitSop.c.orig 2010-03-06 06:48:41.000000000 -0700 -+++ ./src/extlib-abc/aig/kit/kitSop.c 2012-01-10 16:05:21.233609804 -0700 ++++ ./src/extlib-abc/aig/kit/kitSop.c 2012-08-07 16:26:11.751851950 -0600 @@ -174,7 +174,7 @@ void Kit_SopDivideByCube( Kit_Sop_t * cS ***********************************************************************/ void Kit_SopDivideInternal( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory ) @@ -1980,7 +1268,7 @@ assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) ); // consider special case --- ./src/extlib-abc/aig/kit/kitAig.c.orig 2010-03-06 06:48:41.000000000 -0700 -+++ ./src/extlib-abc/aig/kit/kitAig.c 2012-01-10 16:05:21.233609804 -0700 ++++ ./src/extlib-abc/aig/kit/kitAig.c 2012-08-07 16:26:11.751851950 -0600 @@ -54,8 +54,8 @@ Aig_Obj_t * Kit_GraphToAigInternal( Aig_ // build the AIG nodes corresponding to the AND gates of the graph Kit_GraphForEachNode( pGraph, pNode, i ) @@ -1993,7 +1281,7 @@ } // complement the result if necessary --- ./src/extlib-abc/aig/kit/kitGraph.c.orig 2010-03-06 06:48:41.000000000 -0700 -+++ ./src/extlib-abc/aig/kit/kitGraph.c 2012-01-10 16:05:21.234609784 -0700 ++++ ./src/extlib-abc/aig/kit/kitGraph.c 2012-08-07 16:38:39.828797982 -0600 @@ -69,7 +69,7 @@ Kit_Graph_t * Kit_GraphCreateConst0() pGraph = ALLOC( Kit_Graph_t, 1 ); memset( pGraph, 0, sizeof(Kit_Graph_t) ); @@ -2118,72 +1406,8 @@ uTruth = uTruth0 & uTruth1; pNode->pFunc = (void *)(long)uTruth; } ---- ./src/extlib-abc/aig/aig/aigTable.c.orig 2010-03-06 06:48:41.000000000 -0700 -+++ ./src/extlib-abc/aig/aig/aigTable.c 2012-01-10 16:05:21.234609784 -0700 -@@ -74,8 +74,8 @@ void Aig_TableResize( Aig_Man_t * p ) - { - Aig_Obj_t * pEntry, * pNext; - Aig_Obj_t ** pTableOld, ** ppPlace; -- int nTableSizeOld, Counter, i, clk; --clk = clock(); -+ int nTableSizeOld, Counter, i; -+ - // save the old table - pTableOld = p->pTable; - nTableSizeOld = p->nTableSize; ---- ./src/extlib-abc/aig/aig/aigShow.c.orig 2010-03-06 06:48:41.000000000 -0700 -+++ ./src/extlib-abc/aig/aig/aigShow.c 2012-01-10 16:05:21.234609784 -0700 -@@ -329,7 +329,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, - void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) - { - extern void Abc_ShowFile( char * FileNameDot ); -- static Counter = 0; -+ static int Counter = 0; - char FileNameDot[200]; - FILE * pFile; - // create the file name ---- ./src/extlib-abc/aig/aig/aigObj.c.orig 2010-03-06 06:48:41.000000000 -0700 -+++ ./src/extlib-abc/aig/aig/aigObj.c 2012-01-10 16:05:21.234609784 -0700 -@@ -299,8 +299,10 @@ void Aig_NodeFixBufferFanins( Aig_Man_t - pResult = Aig_Oper( p, pFanReal0, pFanReal1, Aig_ObjType(pObj) ); - // else if ( Aig_ObjIsLatch(pObj) ) - // pResult = Aig_Latch( p, pFanReal0, Aig_ObjInit(pObj) ); -- else -+ else { - assert( 0 ); -+ pResult = NULL; -+ } - // replace the node with buffer by the node without buffer - Aig_ObjReplace( p, pObj, pResult, fNodesOnly, fUpdateLevel ); - } ---- ./src/extlib-abc/aig/cnf/cnfWrite.c.orig 2011-01-07 21:23:57.000000000 -0700 -+++ ./src/extlib-abc/aig/cnf/cnfWrite.c 2012-01-10 16:05:21.235609764 -0700 -@@ -352,7 +352,6 @@ Cnf_Dat_t * Cnf_DeriveSimple_Additional( - int Number = old->nVars+1; - - // assign variables to the PIs -- int newPI = 0; - Aig_ManForEachPi( p, pObj, i ) - if (pCnf->pVarNums[pObj->Id] == -1) // new! - pCnf->pVarNums[pObj->Id] = Number++; ---- ./src/extlib-abc/aig/dar/darPrec.c.orig 2010-03-06 06:48:41.000000000 -0700 -+++ ./src/extlib-abc/aig/dar/darPrec.c 2012-01-10 16:05:21.235609764 -0700 -@@ -258,11 +258,9 @@ unsigned Dar_TruthPolarize( unsigned uTr - 0xFF00FF00, // 1111 1111 0000 0000 1111 1111 0000 0000 - 0xFFFF0000 // 1111 1111 1111 1111 0000 0000 0000 0000 - }; -- unsigned uTruthRes, uCof0, uCof1; -- int nMints, Shift, v; -+ unsigned uCof0, uCof1; -+ int Shift, v; - assert( nVars < 6 ); -- nMints = (1 << nVars); -- uTruthRes = uTruth; - for ( v = 0; v < nVars; v++ ) - if ( Polarity & (1 << v) ) - { --- ./src/extlib-abc/aig/dar/darRefact.c.orig 2010-03-06 06:48:41.000000000 -0700 -+++ ./src/extlib-abc/aig/dar/darRefact.c 2012-01-10 16:05:21.236609744 -0700 ++++ ./src/extlib-abc/aig/dar/darRefact.c 2012-08-07 16:26:11.752851949 -0600 @@ -213,7 +213,7 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig { Kit_Node_t * pNode, * pNode0, * pNode1; @@ -2234,30 +1458,733 @@ pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 ); /* printf( "Checking " ); ---- ./src/AST/ASTmisc.cpp.orig 2012-01-09 22:53:22.000000000 -0700 -+++ ./src/AST/ASTmisc.cpp 2012-01-10 16:05:21.236609744 -0700 -@@ -150,7 +150,7 @@ namespace BEEV +--- ./src/extlib-abc/aig/dar/darPrec.c.orig 2010-03-06 06:48:41.000000000 -0700 ++++ ./src/extlib-abc/aig/dar/darPrec.c 2012-08-07 16:26:11.752851949 -0600 +@@ -258,11 +258,9 @@ unsigned Dar_TruthPolarize( unsigned uTr + 0xFF00FF00, // 1111 1111 0000 0000 1111 1111 0000 0000 + 0xFFFF0000 // 1111 1111 1111 1111 0000 0000 0000 0000 + }; +- unsigned uTruthRes, uCof0, uCof1; +- int nMints, Shift, v; ++ unsigned uCof0, uCof1; ++ int Shift, v; + assert( nVars < 6 ); +- nMints = (1 << nVars); +- uTruthRes = uTruth; + for ( v = 0; v < nVars; v++ ) + if ( Polarity & (1 << v) ) + { +--- ./src/extlib-abc/kit.h.orig 2011-02-09 18:31:59.000000000 -0700 ++++ ./src/extlib-abc/kit.h 2012-08-07 16:26:11.753851948 -0600 +@@ -53,11 +53,14 @@ struct Kit_Sop_t_ + unsigned * pCubes; // the storage for cubes + }; + +-typedef struct Kit_Edge_t_ Kit_Edge_t; +-struct Kit_Edge_t_ ++typedef union Kit_Edge_t_ Kit_Edge_t; ++union Kit_Edge_t_ + { +- unsigned fCompl : 1; // the complemented bit +- unsigned Node : 30; // the decomposition node pointed by the edge ++ struct { ++ unsigned fCompl : 1; // the complemented bit ++ unsigned Node : 30; // the decomposition node pointed by the edge ++ } edgeBits; ++ unsigned int edgeInt; + }; + + typedef struct Kit_Node_t_ Kit_Node_t; +@@ -203,18 +206,18 @@ static inline void Kit_SopShrink + static inline void Kit_SopPushCube( Kit_Sop_t * cSop, unsigned uCube ) { cSop->pCubes[cSop->nCubes++] = uCube; } + static inline void Kit_SopWriteCube( Kit_Sop_t * cSop, unsigned uCube, int i ) { cSop->pCubes[i] = uCube; } + +-static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { fCompl, Node }; return eEdge; } +-static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.Node << 1) | eEdge.fCompl; } ++static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { { fCompl, Node } }; return eEdge; } ++static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.edgeBits.Node << 1) | eEdge.edgeBits.fCompl; } + static inline Kit_Edge_t Kit_IntToEdge( unsigned Edge ) { return Kit_EdgeCreate( Edge >> 1, Edge & 1 ); } +-static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return *(unsigned *)&eEdge; } +-static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { return *(Kit_Edge_t *)&Edge; } ++static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return eEdge.edgeInt; } ++static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { Kit_Edge_t eEdge; eEdge.edgeInt = Edge; return eEdge; } + + static inline int Kit_GraphIsConst( Kit_Graph_t * pGraph ) { return pGraph->fConst; } +-static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.fCompl; } +-static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.fCompl; } +-static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.fCompl; } +-static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; } +-static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.fCompl ^= 1; } ++static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.edgeBits.fCompl; } ++static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.edgeBits.fCompl; } ++static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.edgeBits.fCompl; } ++static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.edgeBits.Node < (unsigned)pGraph->nLeaves; } ++static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.edgeBits.fCompl ^= 1; } + static inline void Kit_GraphSetRoot( Kit_Graph_t * pGraph, Kit_Edge_t eRoot ) { pGraph->eRoot = eRoot; } + static inline int Kit_GraphLeaveNum( Kit_Graph_t * pGraph ) { return pGraph->nLeaves; } + static inline int Kit_GraphNodeNum( Kit_Graph_t * pGraph ) { return pGraph->nSize - pGraph->nLeaves; } +@@ -222,14 +225,12 @@ static inline Kit_Node_t * Kit_GraphNode + static inline Kit_Node_t * Kit_GraphNodeLast( Kit_Graph_t * pGraph ) { return pGraph->pNodes + pGraph->nSize - 1; } + static inline int Kit_GraphNodeInt( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return pNode - pGraph->pNodes; } + static inline int Kit_GraphNodeIsVar( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; } +-static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.Node ); } ++static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.edgeBits.Node ); } + static inline int Kit_GraphVarInt( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); } +-static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node); } +-static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node); } +-static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level; } ++static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node); } ++static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node); } ++static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.edgeBits.Node)->Level; } + +-static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); } +-static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); } + static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); } + static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } + static inline unsigned Kit_BitMask( int nBits ) { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits); } +@@ -486,6 +487,18 @@ static inline void Kit_TruthIthVar( unsi + /// FUNCTION DECLARATIONS /// + //////////////////////////////////////////////////////////////////////// + ++extern Kit_Graph_t * Kit_GraphCreateConst0( void ); ++extern Kit_Graph_t * Kit_GraphCreateConst1( void ); ++extern void Kit_GraphFree( Kit_Graph_t * ); ++extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t *, int, int, Vec_Int_t * ); ++extern void Kit_TruthCofactor0( unsigned *, int, int ); ++extern void Kit_TruthCofactor1( unsigned *, int, int ); ++extern int Kit_TruthIsop( unsigned *, int, Vec_Int_t *, int ); ++extern void Kit_TruthShrink( unsigned *, unsigned *, int, int, unsigned, int ); ++extern void Kit_TruthStretch( unsigned *, unsigned *, int, int, unsigned, int ); ++extern Kit_Graph_t * Kit_TruthToGraph( unsigned *, int, Vec_Int_t * ); ++extern int Kit_TruthVarInSupport( unsigned *, int, int ); ++ + #if 0 + + /*=== kitBdd.c ==========================================================*/ +--- ./src/STPManager/STP.cpp.orig 2012-06-15 08:40:15.000000000 -0600 ++++ ./src/STPManager/STP.cpp 2012-08-07 16:26:11.753851948 -0600 +@@ -65,8 +65,8 @@ namespace BEEV { + newS = new MinisatCore(bm->soft_timeout_expired); + else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS) + newS = new MinisatCore_prop(bm->soft_timeout_expired); +- +- ++ else ++ newS = NULL; - visited.insert(n.GetNodeNum()); + SATSolver& NewSolver = *newS; + +@@ -566,7 +566,7 @@ namespace BEEV { + + ToSATAIG toSATAIG(bm, cb, arrayTransformer); + +- ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ; ++ ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : &toSATAIG; + + if (bm->soft_timeout_expired) + return SOLVER_TIMEOUT; +--- ./src/simplifier/constantBitP/ConstantBitP_Division.cpp.orig 2012-04-15 00:52:35.000000000 -0600 ++++ ./src/simplifier/constantBitP/ConstantBitP_Division.cpp 2012-08-07 16:26:11.754851947 -0600 +@@ -157,14 +157,14 @@ Result bvUnsignedQuotientAndRemainder(ve + if (whatIs == QUOTIENT_IS_OUTPUT) { + setUnsignedMinMax(output, minQuotient, maxQuotient); + +- for (int i = 0; i < width; i++) ++ for (unsigned int i = 0; i < width; i++) + CONSTANTBV::BitVector_Bit_On(maxRemainder, i); + } + else + { + setUnsignedMinMax(output, minRemainder, maxRemainder); + +- for (int i =0; i < width;i++) ++ for (unsigned int i =0; i < width;i++) + CONSTANTBV::BitVector_Bit_On(maxQuotient,i); + } + +--- ./src/simplifier/constantBitP/ConstantBitPropagation.cpp.orig 2012-04-03 06:32:10.000000000 -0600 ++++ ./src/simplifier/constantBitP/ConstantBitPropagation.cpp 2012-08-07 16:26:11.754851947 -0600 +@@ -430,7 +430,7 @@ namespace simplifier + void + ConstantBitPropagation::scheduleDown(const ASTNode& n) + { +- for (int i = 0; i < n.Degree(); i++) ++ for (size_t i = 0; i < n.Degree(); i++) + workList->push(n[i]); + } + +@@ -465,7 +465,7 @@ namespace simplifier + + assert(FixedBits::equals(newBits, current)); + +- for (int i = 0; i < n.Degree(); i++) ++ for (size_t i = 0; i < n.Degree(); i++) + { + if (!FixedBits::equals(*getUpdatedFixedBits(n[i]), + childrenFixedBits[i])) +--- ./src/simplifier/constantBitP/FixedBits.cpp.orig 2012-02-17 06:48:39.000000000 -0700 ++++ ./src/simplifier/constantBitP/FixedBits.cpp 2012-08-07 16:34:38.053114918 -0600 +@@ -382,7 +382,7 @@ namespace simplifier + void + FixedBits::fromUnsigned(unsigned val) + { +- for (unsigned i = 0; i < width; i++) ++ for (unsigned i = 0; i < (unsigned) width; i++) + { + if (i < (unsigned) width && i < sizeof(unsigned) * 8) + { +--- ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp.orig 2012-04-22 05:52:33.000000000 -0600 ++++ ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp 2012-08-07 16:37:05.172884335 -0600 +@@ -128,6 +128,7 @@ fast_exit(FixedBits& c0, FixedBits& c1) + } + return false; + } ++ return false; + } + + +--- ./src/simplifier/SubstitutionMap.h.orig 2012-08-07 16:26:07.499857701 -0600 ++++ ./src/simplifier/SubstitutionMap.h 2012-08-07 16:26:11.755851945 -0600 +@@ -40,7 +40,7 @@ namespace BEEV + bool + loops(const ASTNode& n0, const ASTNode& n1); + +- int substitutionsLastApplied; ++ size_t substitutionsLastApplied; + public: + + bool +--- ./src/simplifier/VariablesInExpression.cpp.orig 2011-02-01 05:41:57.000000000 -0700 ++++ ./src/simplifier/VariablesInExpression.cpp 2012-08-07 16:26:11.755851945 -0600 +@@ -42,7 +42,7 @@ Symbols* VariablesInExpression::getSymbo + } + + vector children; +- for (int i = 0; i < n.Degree(); i++) { ++ for (size_t i = 0; i < n.Degree(); i++) { + Symbols* v = getSymbol(n[i]); + if (!v->empty()) + children.push_back(v); +@@ -111,7 +111,7 @@ ASTNodeSet * VariablesInExpression::Seto + vector av; + VarSeenInTerm(symbol,visited,*symbols,av); + +- for (int i =0; i < av.size();i++) ++ for (size_t i =0; i < av.size();i++) + { + const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second; + symbols->insert(sym.begin(), sym.end()); +@@ -155,7 +155,7 @@ bool VariablesInExpression::VarSeenInTer + sort(av.begin(), av.end()); + + //cout << "===" << endl; +- for (int i = 0; i < av.size(); i++) { ++ for (size_t i = 0; i < av.size(); i++) { + if (i!=0 && av[i] == av[i-1]) + continue; + +--- ./src/simplifier/UseITEContext.h.orig 2012-08-07 16:26:07.500857699 -0600 ++++ ./src/simplifier/UseITEContext.h 2012-08-07 16:26:11.756851943 -0600 +@@ -28,7 +28,7 @@ namespace BEEV + if (n.GetKind() == NOT && n[0].GetKind() == OR) + { + ASTVec flat = FlattenKind(OR, n[0].GetChildren()); +- for (int i = 0; i < flat.size(); i++) ++ for (size_t i = 0; i < flat.size(); i++) + context.insert(nf->CreateNode(NOT, flat[i])); + } + else if (n.GetKind() == AND) +@@ -86,7 +86,7 @@ namespace BEEV + } + else + { +- for (int i = 0; i < n.GetChildren().size(); i++) ++ for (size_t i = 0; i < n.GetChildren().size(); i++) + new_children.push_back(visit(n[i], visited, visited_empty, context)); + } + +--- ./src/simplifier/FindPureLiterals.h.orig 2012-08-07 16:26:07.500857699 -0600 ++++ ./src/simplifier/FindPureLiterals.h 2012-08-07 16:26:11.756851943 -0600 +@@ -110,7 +110,7 @@ public: + { + case AND: + case OR: +- for (int i =0; i < n.Degree(); i ++) ++ for (size_t i =0; i < n.Degree(); i ++) + build(n[i],polarity); + break; + +@@ -121,7 +121,7 @@ public: + + default: + polarity = bothPolarity; // both +- for (int i =0; i < n.Degree(); i ++) ++ for (size_t i =0; i < n.Degree(); i ++) + build(n[i],polarity); + break; + } +--- ./src/simplifier/simplifier.cpp.orig 2012-04-29 04:49:41.000000000 -0600 ++++ ./src/simplifier/simplifier.cpp 2012-08-07 16:26:11.757851942 -0600 +@@ -248,7 +248,7 @@ namespace BEEV + assert(false); + } - for (int i = 0; i < n.Degree(); i++) + for (size_t i = 0; i < n.Degree(); i++) - numberOfReadsLessThan(n[i], visited, soFar,limit); + { + checkIfInSimplifyMap(n[i], visited); + } +@@ -523,6 +523,7 @@ namespace BEEV + return getConstantBit(n[0], i); + + assert(false); ++ return -1; } ---- ./src/AST/ArrayTransformer.cpp.orig 2011-12-28 19:00:01.000000000 -0700 -+++ ./src/AST/ArrayTransformer.cpp 2012-01-10 16:05:21.236609744 -0700 -@@ -61,7 +61,6 @@ namespace BEEV - iset_end = arrayToIndexToRead.end(); - iset != iset_end; iset++) - { -- const ASTNode& ArrName = iset->first; - map& mapper = iset->second; + ASTNode +@@ -1302,7 +1303,7 @@ namespace BEEV + else + { + ASTVec newC; +- for (int i = 0; i < a.GetChildren().size(); i++) ++ for (size_t i = 0; i < a.GetChildren().size(); i++) + { + newC.push_back(SimplifyFormula(a[i], false, VarConstMap)); + } +@@ -1664,9 +1665,9 @@ namespace BEEV + assert(BVMULT == k || SBVDIV == k || BVPLUS ==k); + const int inputValueWidth = output.GetValueWidth(); - for (map::iterator it =mapper.begin() ; it != mapper.end();it++) ---- ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp.orig 2012-01-09 20:39:36.000000000 -0700 -+++ ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp 2012-01-10 16:05:21.237609723 -0700 -@@ -384,7 +384,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(c +- int lengthA = output.GetChildren()[0][0].GetValueWidth(); +- int lengthB = output.GetChildren()[1][0].GetValueWidth(); +- int maxLength; ++ unsigned int lengthA = output.GetChildren()[0][0].GetValueWidth(); ++ unsigned int lengthB = output.GetChildren()[1][0].GetValueWidth(); ++ unsigned int maxLength; + if (BVMULT == output.GetKind()) + maxLength = lengthA + lengthB; + else if (BVPLUS == output.GetKind() || SBVDIV == output.GetKind()) +@@ -1694,7 +1695,7 @@ namespace BEEV + { + const ASTNode a = children[0]; + const ASTNode b = children[1]; +- const int width = children[0].GetValueWidth(); ++ const unsigned int width = children[0].GetValueWidth(); + ASTNode output; + + assert(b.isConstant()); +@@ -1725,7 +1726,7 @@ namespace BEEV + { + const ASTNode a = children[0]; + const ASTNode b = children[1]; +- const int width = children[0].GetValueWidth(); ++ const unsigned int width = children[0].GetValueWidth(); + ASTNode output; + + assert(b.isConstant()); +@@ -1906,7 +1907,7 @@ namespace BEEV + //I haven't measured if this is worth the expense. + { + bool notSimplified = false; +- for (int i = 0; i < inputterm.Degree(); i++) ++ for (size_t i = 0; i < inputterm.Degree(); i++) + if (inputterm[i].GetType() != ARRAY_TYPE) + if (!hasBeenSimplified(inputterm[i])) + { +@@ -2247,7 +2248,6 @@ namespace BEEV + case BVEXTRACT: + { + const unsigned innerLow = a0[2].GetUnsignedConst(); +- const unsigned innerHigh = a0[1].GetUnsignedConst(); + + output = nf->CreateTerm(BVEXTRACT, inputValueWidth, a0[0], _bm->CreateBVConst(32, i_val + innerLow), + _bm->CreateBVConst(32, j_val + innerLow)); +@@ -2647,7 +2647,7 @@ namespace BEEV + assert(BVTypeCheck(output)); + + // If the leading bits are zero. Replace it by a concat with zero. +- int i; ++ unsigned int i; + if (output.GetKind() == BVAND && output.Degree() == 2 && ((i = numberOfLeadingZeroes(output[0])) > 0)) + { + // i contains the number of leading zeroes. +@@ -2669,13 +2669,13 @@ namespace BEEV + } + if (output.GetKind() == BVAND) + { +- int trailingZeroes = 0; +- for (int i = 0; i < output.Degree(); i++) ++ unsigned int trailingZeroes = 0; ++ for (size_t i = 0; i < output.Degree(); i++) + { + const ASTNode& n = output[i]; + if (n.GetKind() != BVCONST) + continue; +- int j; ++ unsigned int j; + for (j = 0; j < n.GetValueWidth(); j++) + if (CONSTANTBV::BitVector_bit_test(n.GetBVConst(), j)) + break; +@@ -2692,7 +2692,7 @@ namespace BEEV + //cerr << "old" << output; + ASTNode zeroes = _bm->CreateZeroConst(trailingZeroes); + ASTVec newChildren; +- for (int i = 0; i < output.Degree(); i++) ++ for (size_t i = 0; i < output.Degree(); i++) + newChildren.push_back( + nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - trailingZeroes, output[i], + _bm->CreateBVConst(32, output.GetValueWidth() - 1), +--- ./src/simplifier/RemoveUnconstrained.cpp.orig 2012-03-19 21:59:03.000000000 -0600 ++++ ./src/simplifier/RemoveUnconstrained.cpp 2012-08-07 16:28:13.624742813 -0600 +@@ -55,7 +55,7 @@ namespace BEEV + + bool allChildrenAreUnconstrained(vector children) + { +- for (int i =0; i < children.size(); i++) ++ for (size_t i =0; i < children.size(); i++) + if (!children[i]->isUnconstrained()) + return false; + +@@ -100,7 +100,7 @@ namespace BEEV + // Going to be rebuilt later anyway, so discard. + vector variables; + +- for (int i =0; i n; + assert(var.GetKind() == SYMBOL); +@@ -151,7 +151,7 @@ namespace BEEV + } + + ASTNode concat = concatVec[0]; +- for (int i=1; i < concatVec.size();i++) ++ for (size_t i=1; i < concatVec.size();i++) + { + assert(!concat.IsNull()); + concat = bm.CreateTerm(BVCONCAT, concat.GetValueWidth() + concatVec[i].GetValueWidth(),concatVec[i], concat); +@@ -184,7 +184,7 @@ namespace BEEV + + topMutable->getAllUnconstrainedVariables(variable_array); + +- for (int i =0; i < variable_array.size() ; i++) ++ for (size_t i =0; i < variable_array.size() ; i++) + { + // Don't make this is a reference. If the vector gets resized, it will point to + // memory that no longer contains the object. +@@ -208,7 +208,7 @@ namespace BEEV + //nb. The children might be dirty. i.e. not have substitutions written through them yet. + ASTVec children; + children.reserve(mutable_children.size()); +- for (int j = 0; j n); + + const size_t numberOfChildren = children.size(); +@@ -217,7 +217,7 @@ namespace BEEV + unsigned indexWidth = muteNode.getParent().n.GetIndexWidth(); + + ASTNode other; +- MutableASTNode* muteOther; ++ MutableASTNode* muteOther = NULL; + + if(numberOfChildren == 2) + { +@@ -242,7 +242,7 @@ namespace BEEV + { + int found = 0; + +- for (int i = 0; i < numberOfChildren; i++) ++ for (size_t i = 0; i < numberOfChildren; i++) + { + if (children[i] == var) + found++; +@@ -429,7 +429,7 @@ namespace BEEV + { + ASTNodeSet already; + ASTNode v =replaceParentWithFresh(muteParent, variable_array); +- for (int i =0; i < numberOfChildren;i++) ++ for (size_t i =0; i < numberOfChildren;i++) + { + /* to avoid problems with: + 734:(AND +@@ -464,7 +464,7 @@ namespace BEEV + ASTNode v =replaceParentWithFresh(muteParent, variable_array); + + ASTVec others; +- for (int i = 0; i < numberOfChildren; i++) ++ for (size_t i = 0; i < numberOfChildren; i++) + { + if (children[i] !=var) + others.push_back(mutable_children[i]->toASTNode(nf)); +@@ -617,7 +617,7 @@ namespace BEEV + case BVPLUS: + { + ASTVec other; +- for (int i = 0; i < children.size(); i++) ++ for (size_t i = 0; i < children.size(); i++) + if (children[i] != var) + other.push_back(mutable_children[i]->toASTNode(nf)); + +@@ -639,7 +639,6 @@ namespace BEEV + { + ASTNode v =replaceParentWithFresh(muteParent, variable_array); + +- const unsigned resultWidth = width; + const unsigned operandWidth = var.GetValueWidth(); + assert(children[0] == var); // It can't be anywhere else. + +--- ./src/simplifier/AlwaysTrue.h.orig 2012-08-07 16:26:07.501857698 -0600 ++++ ./src/simplifier/AlwaysTrue.h 2012-08-07 16:26:11.759851939 -0600 +@@ -85,7 +85,7 @@ public: + else + new_state = state; + +- for (int i=0; i < n.Degree(); i++) ++ for (size_t i=0; i < n.Degree(); i++) + { + newChildren.push_back(visit(n[i],new_state,fromTo)); + } +--- ./src/simplifier/PropagateEqualities.cpp.orig 2012-01-28 19:12:31.000000000 -0700 ++++ ./src/simplifier/PropagateEqualities.cpp 2012-08-07 16:30:09.932731593 -0600 +@@ -31,10 +31,10 @@ namespace BEEV + + bool result = false; + if (k == XOR) +- for (int i = 0; i < lhs.Degree(); i++) ++ for (unsigned int i = 0; i < lhs.Degree(); i++) + { + ASTVec others; +- for (int j = 0; j < lhs.Degree(); j++) ++ for (unsigned int j = 0; j < lhs.Degree(); j++) + if (j != i) + others.push_back(lhs[j]); + +@@ -77,10 +77,10 @@ namespace BEEV + return searchTerm(lhs[0], nf->CreateTerm(BVNEG, width, rhs)); + + if (lhs.GetKind() == BVXOR || lhs.GetKind() == BVPLUS) +- for (int i = 0; i < lhs.Degree(); i++) ++ for (unsigned int i = 0; i < lhs.Degree(); i++) + { + ASTVec others; +- for (int j = 0; j < lhs.Degree(); j++) ++ for (unsigned int j = 0; j < lhs.Degree(); j++) + if (j != i) + others.push_back(lhs[j]); + +--- ./src/simplifier/consteval.cpp.orig 2011-12-28 19:00:01.000000000 -0700 ++++ ./src/simplifier/consteval.cpp 2012-08-07 16:26:11.759851939 -0600 +@@ -43,7 +43,7 @@ namespace BEEV + + ASTVec children; + children.reserve(number_of_children); +- for (int i =0; i < number_of_children; i++) ++ for (unsigned int i =0; i < number_of_children; i++) + { + if (input_children[i].isConstant()) + children.push_back(input_children[i]); +--- ./src/simplifier/MutableASTNode.h.orig 2011-03-29 07:18:23.000000000 -0600 ++++ ./src/simplifier/MutableASTNode.h 2012-08-07 16:26:11.760851937 -0600 +@@ -46,12 +46,12 @@ public: + vector tempChildren; + tempChildren.reserve(n.Degree()); + +- for (int i = 0; i < n.Degree(); i++) ++ for (size_t i = 0; i < n.Degree(); i++) + tempChildren.push_back(build(n[i], visited)); + + MutableASTNode * mut = createNode(n); + +- for (int i = 0; i < n.Degree(); i++) ++ for (size_t i = 0; i < n.Degree(); i++) + tempChildren[i]->parents.insert(mut); + + mut->children.insert(mut->children.end(),tempChildren.begin(),tempChildren.end()); +@@ -86,7 +86,7 @@ private: + assert(found); + } + +- for (int i = 0; i < children.size(); i++) ++ for (size_t i = 0; i < children.size(); i++) + { + // call check on all the children. + children[i]->checkInvariant(); +@@ -116,7 +116,7 @@ private: + return n; + + ASTVec newChildren; +- for (int i = 0; i < children.size(); i++) ++ for (size_t i = 0; i < children.size(); i++) + newChildren.push_back(children[i]->toASTNode(nf)); + + // Don't use the hashing node factory here. Imagine CreateNode simplified down, +@@ -189,7 +189,7 @@ private: + removeChildren(vars); // ignore the result + children.clear(); + children.insert(children.begin(), newN->children.begin(), newN->children.end()); +- for (int i = 0; i < children.size(); i++) ++ for (size_t i = 0; i < children.size(); i++) + children[i]->parents.insert(this); + + propagateUpDirty(); +@@ -249,7 +249,7 @@ private: + + ASTNode& node = all[i]->n; + bool found[node.GetValueWidth()]; +- for (int j=0; j maxV,i)) + CONSTANTBV::BitVector_Bit_On(result->maxV,i); +@@ -510,7 +510,7 @@ namespace BEEV + CONSTANTBV::BitVector_Bit_Off(result->minV,i); + } + +- for (int i=n[0].GetValueWidth(); i < n.GetValueWidth();i++) ++ for (unsigned int i=n[0].GetValueWidth(); i < n.GetValueWidth();i++) + CONSTANTBV::BitVector_Bit_Off(result->maxV,i); + } + } else if (knownC1) +@@ -518,13 +518,13 @@ namespace BEEV + // Ignores what's already there for now.. + + IntervalType * circ_result = freshUnsignedInterval(n.GetValueWidth()); +- for (int i=0; i < n[0].GetValueWidth()-1;i++) ++ for (unsigned int i=0; i < n[0].GetValueWidth()-1;i++) + { + CONSTANTBV::BitVector_Bit_On(circ_result->maxV,i); + CONSTANTBV::BitVector_Bit_Off(circ_result->minV,i); + } + +- for (int i=n[0].GetValueWidth()-1; i < n.GetValueWidth();i++) ++ for (unsigned int i=n[0].GetValueWidth()-1; i < n.GetValueWidth();i++) + { + CONSTANTBV::BitVector_Bit_Off(circ_result->maxV,i); + CONSTANTBV::BitVector_Bit_On(circ_result->minV,i); +@@ -599,7 +599,7 @@ namespace BEEV + CONSTANTBV::BitVector_increment(result->maxV); + + bool bad= false; +- for (int i =0; i < children.size(); i++) ++ for (size_t i =0; i < children.size(); i++) + { + if (children[i] == NULL) + { +@@ -612,10 +612,10 @@ namespace BEEV + e = CONSTANTBV::BitVector_Multiply(max, result->maxV, children[i]->maxV); + assert (0 == e); + +- if (CONSTANTBV::Set_Max(max) >= width) ++ if (CONSTANTBV::Set_Max(max) >= (long)width) + bad = true; + +- for (int j = width; j < 2 * width; j++) ++ for (unsigned int j = width; j < 2 * width; j++) + { + if (CONSTANTBV::BitVector_bit_test(min, j)) + bad = true; +@@ -688,7 +688,7 @@ namespace BEEV + + bool carry = false; + +- for (int i =0; i < children.size(); i++) ++ for (size_t i =0; i < children.size(); i++) + { + if (children[i] == NULL) + { +@@ -717,7 +717,7 @@ namespace BEEV + if (knownC1) + { + // Copy in the minimum and maximum. +- for (int i=0; i < n[1].GetValueWidth();i++) ++ for (unsigned int i=0; i < n[1].GetValueWidth();i++) + { + if (CONSTANTBV::BitVector_bit_test(children[1]->maxV,i)) + CONSTANTBV::BitVector_Bit_On(result->maxV,i); +@@ -734,7 +734,7 @@ namespace BEEV + if (knownC0) + { + // Copy in the minimum and maximum. +- for (int i=n[1].GetValueWidth(); i < n.GetValueWidth();i++) ++ for (unsigned int i=n[1].GetValueWidth(); i < n.GetValueWidth();i++) + { + if (CONSTANTBV::BitVector_bit_test(children[0]->maxV,i- n[1].GetValueWidth())) + CONSTANTBV::BitVector_Bit_On(result->maxV,i); +@@ -755,7 +755,7 @@ namespace BEEV + + bool nonNull = true; + // If all the children are known, output 'em. +- for (int i=0; i < n.Degree();i++) ++ for (size_t i=0; i < n.Degree();i++) + { + if (children[i]== NULL) + nonNull=false; +@@ -764,7 +764,7 @@ namespace BEEV + if (false && nonNull && n.GetKind() != SYMBOL && n.GetKind() != AND) + { + cerr << n; +- for (int i=0; i < n.Degree();i++) ++ for (size_t i=0; i < n.Degree();i++) + children[i]->print(); + } + } +@@ -797,10 +797,10 @@ namespace BEEV + + ~EstablishIntervals() + { +- for (int i =0; i < toDeleteLater.size();i++) ++ for (size_t i =0; i < toDeleteLater.size();i++) + delete toDeleteLater[i]; + +- for (int i =0; i < likeAutoPtr.size();i++) ++ for (size_t i =0; i < likeAutoPtr.size();i++) + CONSTANTBV::BitVector_Destroy(likeAutoPtr[i]); + + likeAutoPtr.clear(); +--- ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp.orig 2012-05-26 00:24:52.000000000 -0600 ++++ ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp 2012-08-07 16:26:11.762851935 -0600 +@@ -386,7 +386,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(c const ASTNode& in2 = swap ? children[0] : children[1]; const Kind k1 = in1.GetKind(); const Kind k2 = in2.GetKind(); @@ -2266,16 +2193,7 @@ if (in1 == in2) //terms are syntactically the same -@@ -401,7 +401,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(c - if ((k1 == BVUMINUS && k2 == BEEV::BVCONST) || (k1 == BVNEG && k2 == BEEV::BVCONST)) - return NodeFactory::CreateNode(EQ, in1[0], NodeFactory::CreateTerm(k1, width, in2)); - -- if (k2 == BVUMINUS && k1 == BEEV::BVCONST || (k2 == BVNEG && k1 == BEEV::BVCONST)) -+ if ((k2 == BVUMINUS && k1 == BEEV::BVCONST) || (k2 == BVNEG && k1 == BEEV::BVCONST)) - return NodeFactory::CreateNode(EQ, in2[0], NodeFactory::CreateTerm(k2, width, in1)); - - if ((k1 == BVNEG && in1[0] == in2) || (k2 == BVNEG && in2[0] == in1)) -@@ -460,8 +460,8 @@ SimplifyingNodeFactory::CreateSimpleEQ(c +@@ -462,8 +462,8 @@ SimplifyingNodeFactory::CreateSimpleEQ(c { int match1 = -1, match2 = -1; @@ -2286,7 +2204,7 @@ { if (c1[i] == c2[j]) { -@@ -519,7 +519,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(c +@@ -521,7 +521,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(c bool foundZero = false, foundOne = false; const unsigned original_width = in2[0].GetValueWidth(); const unsigned new_width = in2.GetValueWidth(); @@ -2295,7 +2213,7 @@ if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(), i)) foundOne = true; else -@@ -1103,7 +1103,7 @@ SimplifyingNodeFactory::CreateTerm(Kind +@@ -1107,7 +1107,7 @@ SimplifyingNodeFactory::CreateTerm(Kind bool oneFound = false; bool zeroFound = false; @@ -2304,7 +2222,7 @@ { if (children[i].GetKind() == BEEV::BVCONST) { -@@ -1122,7 +1122,7 @@ SimplifyingNodeFactory::CreateTerm(Kind +@@ -1126,7 +1126,7 @@ SimplifyingNodeFactory::CreateTerm(Kind else if (oneFound) { ASTVec new_children; @@ -2313,7 +2231,7 @@ { if (children[i].GetKind() != BEEV::BVCONST || !CONSTANTBV::BitVector_is_full(children[i].GetBVConst())) new_children.push_back(children[i]); -@@ -1162,13 +1162,14 @@ SimplifyingNodeFactory::CreateTerm(Kind +@@ -1166,13 +1166,14 @@ SimplifyingNodeFactory::CreateTerm(Kind int end = -1; BEEV::CBV c = c0.GetBVConst(); bool bad = false; @@ -2330,7 +2248,7 @@ if (!CONSTANTBV::BitVector_bit_test(c, i)) if (start != -1 && end == -1) -@@ -1189,7 +1190,7 @@ SimplifyingNodeFactory::CreateTerm(Kind +@@ -1193,7 +1194,7 @@ SimplifyingNodeFactory::CreateTerm(Kind ASTNode z = bm.CreateZeroConst(start); result = NodeFactory::CreateTerm(BVCONCAT, end + 1, result, z); } @@ -2339,7 +2257,7 @@ { ASTNode z = bm.CreateZeroConst(width - end - 1); result = NodeFactory::CreateTerm(BVCONCAT, width, z, result); -@@ -1252,7 +1253,6 @@ SimplifyingNodeFactory::CreateTerm(Kind +@@ -1256,7 +1257,6 @@ SimplifyingNodeFactory::CreateTerm(Kind const unsigned outerHigh = children[1].GetUnsignedConst(); const unsigned innerLow = children[0][2].GetUnsignedConst(); @@ -2347,54 +2265,24 @@ result = NodeFactory::CreateTerm(BVEXTRACT, width, children[0][0], bm.CreateBVConst(32, outerHigh + innerLow), bm.CreateBVConst(32, outerLow + innerLow)); } ---- ./src/STPManager/STP.cpp.orig 2012-01-09 22:38:16.000000000 -0700 -+++ ./src/STPManager/STP.cpp 2012-01-10 16:05:21.237609723 -0700 -@@ -59,8 +59,8 @@ namespace BEEV { - newS = new MinisatCore(); - else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS) - newS = new MinisatCore_prop(); -- -- -+ else -+ newS = NULL; +--- ./src/AST/ArrayTransformer.cpp.orig 2012-05-11 20:18:08.000000000 -0600 ++++ ./src/AST/ArrayTransformer.cpp 2012-08-07 16:26:11.762851935 -0600 +@@ -60,7 +60,6 @@ namespace BEEV + iset_end = arrayToIndexToRead.end(); + iset != iset_end; iset++) + { +- const ASTNode& ArrName = iset->first; + map& mapper = iset->second; - SATSolver& NewSolver = *newS; + for (map::iterator it =mapper.begin() ; it != mapper.end();it++) +--- ./src/AST/ASTmisc.cpp.orig 2012-04-03 00:43:00.000000000 -0600 ++++ ./src/AST/ASTmisc.cpp 2012-08-07 16:26:11.763851934 -0600 +@@ -150,7 +150,7 @@ namespace BEEV ---- ./src/parser/ParserInterface.h.orig 2011-07-09 00:56:51.000000000 -0600 -+++ ./src/parser/ParserInterface.h 2012-01-10 16:05:21.238609702 -0700 -@@ -214,7 +214,7 @@ public: - assert(symbols.size() == cache.size()); - cache.erase(cache.end()-1); - ASTVec & current = symbols.back(); -- for (int i=0; i < current.size() ;i++) -+ for (size_t i=0; i < current.size() ;i++) - letMgr._parser_symbol_table.erase(current[i]); - symbols.erase(symbols.end()-1); - } -@@ -234,7 +234,7 @@ public: + visited.insert(n.GetNodeNum()); - void printStatus() - { -- for (int i=0; i < cache.size();i++) -+ for (size_t i=0; i < cache.size();i++) - { - cache[i].print(); - } -@@ -271,7 +271,7 @@ public: +- for (int i = 0; i < n.Degree(); i++) ++ for (size_t i = 0; i < n.Degree(); i++) + numberOfReadsLessThan(n[i], visited, soFar,limit); + } - // Loop through the set of assertions converting them to single nodes.. - ASTVec v; -- for (int i = 0; i < assertionsSMT2.size(); i++) -+ for (size_t i = 0; i < assertionsSMT2.size(); i++) - { - if (assertionsSMT2[i].size() == 1) - {} -@@ -310,7 +310,7 @@ public: - // It's satisfiable, so everything beneath it is satisfiable too. - if (last_result ==SOLVER_SATISFIABLE) - { -- for (int i=0; i < cache.size(); i++) -+ for (size_t i=0; i < cache.size(); i++) - { - assert(cache[i].result != SOLVER_UNSATISFIABLE); - cache[i].result = SOLVER_SATISFIABLE; diff --git a/stp.spec b/stp.spec index 79c30e9..913501c 100644 --- a/stp.spec +++ b/stp.spec @@ -1,11 +1,11 @@ # Upstream occasionally releases a subversion snapshot, but no "regular" # releases since the 0.1 release. -%global svnver 1493 -%global svntim 20120109svn +%global svnver 1666 +%global svntim 20120615svn Name: stp Version: 0.1 -Release: 10.%{svntim}%{?dist} +Release: 11.%{svntim}%{?dist} Summary: Constraint solver/decision procedure Group: Applications/Engineering @@ -19,12 +19,12 @@ URL: http://sourceforge.net/projects/stp-fast-prover/ # stp-0.1 # tar cvJf stp-0.1.tar.xz stp-0.1 Source0: stp-%{version}.tar.xz +# This patch is specific to Fedora. Use the existing cryptominisat and boost +# libraries instead of the bundled versions. +Patch0: stp-unbundle.patch # This patch has not yet been sent upstream. Fix a bunch of compiler warnings # that may indicate miscompiled code. -Patch0: stp-warning.patch -# This patch has not yet been sent upstream. Deal with new C++ declaration -# ordering rules in GCC 4.7. -Patch1: stp-gcc47.patch +Patch1: stp-warning.patch BuildRequires: bison BuildRequires: boost-devel @@ -77,20 +77,26 @@ or automated prover). Provides a static library. %patch0 %patch1 -# Make sure nothing uses the shipped boost sources -rm -fr src/boost +# Make sure nothing uses the shipped boost or cryptominisat sources +rm -fr src/boost src/sat/cryptominisat2 # We do not want to know about the order of member initializers -sed -i "s/\(-Wno-deprecated\)/\1 -Wno-reorder/" scripts/Makefile.common +sed -i "s/-Wno-deprecated/& -Wno-reorder/" scripts/Makefile.common # Avoid a BR on subversion, as well as subversion version hell -sed -i "s|\`svnversion \$(TOP)\`|%{svnver}|" src/main/Makefile +sed -i "s|\`svnversion -c \$(TOP)\`|%{svnver}|" src/main/Makefile + +# Fix Makefile bugs +sed -e "s/^\.PHONY:.*/& depend/" -e "s/^depend:.*/& ASTKind.h/" \ + -i src/AST/Makefile +sed -i "s/^\.PHONY:.*/& depend/" src/main/Makefile %build scripts/configure --with-prefix=%{_prefix} # DO NOT use _smp_mflags; build will fail. -make all OPTIMIZE="%{optflags} -DNDEBUG" LIB_DIR=%{_libdir} +make all OPTIMIZE="%{optflags} -DNDEBUG" LIB_DIR=%{_libdir} \ + LDFLAGS="$RPM_LD_FLAGS -lcryptominisat" # Currently the valgrind tests are failing, because valgrind reports the use # of uninitialized variables deep within libdl. All other tests pass, so @@ -116,6 +122,10 @@ make install PREFIX=%{buildroot}%{_prefix} LIB_DIR=%{buildroot}%{_libdir} %{_includedir}/stp/ %changelog +* Tue Aug 7 2012 Jerry James - 0.1-11.20120615svn +- Update to recent subversion snapshot +- Do not build bundled cryptominisat + * Sat Jul 21 2012 Fedora Release Engineering - 0.1-10.20120109svn - Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild