From 5a3a024fae7e721b13c74ebdffc57dc4d6e3dabb Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 19 Mar 2014 17:09:33 -0600 Subject: [PATCH] Update to recent git snapshot, now hosted on github. Build now uses cmake. Tests now need boolector, which has license problems. Disable %%check for now unless we can find something useful to do. --- .gitignore | 2 +- sources | 2 +- stp-unbundle.patch | 463 +++---- stp-undefined.patch | 80 ++ stp-warning.patch | 2850 +++++++++++++------------------------------ stp.spec | 116 +- 6 files changed, 1141 insertions(+), 2372 deletions(-) create mode 100644 stp-undefined.patch diff --git a/.gitignore b/.gitignore index a214bd6..a8345f8 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1 @@ -/stp-0.1.tar.xz +/stp-stp-fe766c9.tar.gz diff --git a/sources b/sources index 35c150c..2182b29 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -4a44259e06e7d18ccc6615ca65dbc426 stp-0.1.tar.xz +3104c3fcb6e89da91f766e9b61dd87d9 stp-stp-fe766c9.tar.gz diff --git a/stp-unbundle.patch b/stp-unbundle.patch index 5c7a525..3e1b906 100644 --- a/stp-unbundle.patch +++ b/stp-unbundle.patch @@ -1,67 +1,138 @@ ---- ./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 @@ +diff --git a/CMakeLists.txt b/CMakeLists.txt +index cc5bb76..169c064 100644 +--- a/CMakeLists.txt ++++ b/CMakeLists.txt +@@ -69,6 +69,7 @@ endmacro() + if(BUILD_SHARED_LIBS) + message(STATUS "Building shared library currently broken due to mix of C++/C code") + add_cxx_flag_if_supported("-fPIC") ++ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fPIC") + endif() - #include "../AST/AST.h" - #include "../STPManager/STPManager.h" --#include "../boost/noncopyable.hpp" -+#include + check_cxx_compiler_flag("-std=gnu++11" HAVE_FLAG_STD_GNUPP11) +@@ -179,6 +180,7 @@ include_directories(${Boost_INCLUDE_DIRS}) - namespace BEEV + find_package(BISON REQUIRED) + find_package(FLEX REQUIRED) ++find_package(Cryptominisat REQUIRED) + + # ----------------------------------------------------------------------------- + # Setup library build path (this is **not** the library install path) +diff --git a/cmake/modules/FindCryptominisat.cmake b/cmake/modules/FindCryptominisat.cmake +new file mode 100644 +index 0000000..e900145 +--- /dev/null ++++ b/cmake/modules/FindCryptominisat.cmake +@@ -0,0 +1,32 @@ ++# - Find cryptominisat ++# Find the cryptominisat library ++# ++# This module defines the following variables: ++# CRYPTOMINISAT_FOUND - True if _INCLUDE_DIR & _LIBRARY are found ++# CRYPTOMINISAT_LIBRARIES - Set when CRYPTOMINISAT_LIBRARY is found ++# CRYPTOMINISAT_INCLUDE_DIRS - Set when CRYPTOMINISAT_INCLUDE_DIR is found ++# ++# CRYPTOMINISAT_INCLUDE_DIR - where to find Solver.h, etc. ++# CRYPTOMINISAT_LIBRARY - the cryptominisat library ++# ++ ++find_path(CRYPTOMINISAT_INCLUDE_DIR NAMES cmsat/Solver.h ++ DOC "The cryptominisat include directory" ++) ++ ++find_library(CRYPTOMINISAT_LIBRARY NAMES cryptominisat ++ DOC "The cryptominisat library" ++) ++ ++# handle the QUIETLY and REQUIRED arguments and set CRYPTOMINISAT_FOUND to ++# TRUE if all listed variables are TRUE ++find_package_handle_standard_args(CRYPTOMINISAT DEFAULT_MSG ++ CRYPTOMINISAT_LIBRARY ++ CRYPTOMINISAT_INCLUDE_DIR) ++ ++if(CRYPTOMINISAT_FOUND) ++ set( CRYPTOMINISAT_LIBRARIES ${CRYPTOMINISAT_LIBRARY} ) ++ set( CRYPTOMINISAT_INCLUDE_DIRS ${CRYPTOMINISAT_INCLUDE_DIR} ) ++endif() ++ ++mark_as_advanced(CRYPTOMINISAT_INCLUDE_DIR CRYPTOMINISAT_LIBRARY) +diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp +index 7912aeb..cf646b4 100644 +--- a/src/AST/RunTimes.cpp ++++ b/src/AST/RunTimes.cpp +@@ -13,7 +13,7 @@ + #include + #include + #include "RunTimes.h" +-#include "../sat/cryptominisat2/time_mem.h" ++#include + + // BE VERY CAREFUL> Update the Category Names to match. + std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Variable Elimination", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Removing Unconstrained", "Pure Literals" , "ITE Contexts", "AIG core simplification", "Interval Propagation", "Always True"}; +@@ -67,7 +67,7 @@ void RunTimes::print() + std::cerr.precision(2); + std::cerr << "Statistics Total: " << ((double)cummulative_ms)/1000 << "s" << std::endl; + std::cerr << "CPU Time Used : " << cpuTime() << "s" << std::endl; +- std::cerr << "Peak Memory Used: " << memUsedPeak()/(1024.0*1024.0) << "MB" << std::endl; ++ std::cerr << "Peak Memory Used: " << memUsed()/(1024.0*1024.0) << "MB" << std::endl; + + clear(); + +diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h +index 191711e..9a44acd 100644 +--- a/src/AST/RunTimes.h ++++ b/src/AST/RunTimes.h +@@ -18,7 +18,7 @@ + #include + #include + #include +-#include "../sat/cryptominisat2/time_mem.h" ++#include + + class RunTimes : boost::noncopyable { ---- ./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 +diff --git a/src/libstp/CMakeLists.txt b/src/libstp/CMakeLists.txt +index eabc0d6..8cc3bc7 100644 +--- a/src/libstp/CMakeLists.txt ++++ b/src/libstp/CMakeLists.txt +@@ -13,7 +13,6 @@ set(stp_lib_targets + tosat + sat + minisat2 +- cryptominisat2 + simplifier + constantbv + abc +@@ -58,7 +57,7 @@ set_target_properties(libstp PROPERTIES + # Clients of libstp that don't use CMake will have to link the Boost libraries + # in manually. + # ----------------------------------------------------------------------------- +-target_link_libraries(libstp ${Boost_LIBRARIES}) ++target_link_libraries(libstp ${Boost_LIBRARIES} cryptominisat) - 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 + # ----------------------------------------------------------------------------- +diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt +index 4749a77..ffb169e 100644 +--- a/src/sat/CMakeLists.txt ++++ b/src/sat/CMakeLists.txt +@@ -1,4 +1,3 @@ +-add_subdirectory(cryptominisat2) + add_subdirectory(minisat) - 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 @@ + add_library(sat OBJECT +diff --git a/src/sat/CryptoMinisat.cpp b/src/sat/CryptoMinisat.cpp +index 27f372d..93e9b85 100644 +--- a/src/sat/CryptoMinisat.cpp ++++ b/src/sat/CryptoMinisat.cpp +@@ -7,15 +7,26 @@ #undef l_Undef -#include "cryptominisat2/Solver.h" -#include "cryptominisat2/SolverTypes.h" +#include ++#include namespace BEEV { @@ -84,7 +155,7 @@ } CryptoMinisat::~CryptoMinisat() -@@ -30,9 +40,9 @@ namespace BEEV +@@ -30,9 +41,9 @@ namespace BEEV // Cryptominisat uses a slightly different Lit class too. // VERY SLOW> @@ -94,64 +165,21 @@ - v.push(MINISAT::Lit(var(ps[i]), sign(ps[i]))); + v.push(CMSat::Lit(var(ps[i]), sign(ps[i]))); - s->addClause(v); + return s->addClause(v); } -@@ -63,7 +73,7 @@ namespace BEEV +@@ -63,7 +74,7 @@ namespace BEEV - int CryptoMinisat::setVerbosity(int v) + void 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 +diff --git a/src/sat/CryptoMinisat.h b/src/sat/CryptoMinisat.h +index 9c11c1d..50d55fc 100644 +--- a/src/sat/CryptoMinisat.h ++++ b/src/sat/CryptoMinisat.h @@ -6,16 +6,13 @@ #include "SATSolver.h" @@ -172,223 +200,14 @@ 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 +diff --git a/tests/api/C/CMakeLists.txt b/tests/api/C/CMakeLists.txt +index 99c1478..2a490ff 100644 +--- a/tests/api/C/CMakeLists.txt ++++ b/tests/api/C/CMakeLists.txt +@@ -1,4 +1,6 @@ + AddGTestSuite(C-api-tests) ++find_library(cryptominisat) ++find_library(m) - 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 - { + # ----------------------------------------------------------------------------- + # Find the public headers associated with libstp diff --git a/stp-undefined.patch b/stp-undefined.patch new file mode 100644 index 0000000..a5f305e --- /dev/null +++ b/stp-undefined.patch @@ -0,0 +1,80 @@ +diff --git a/src/extlib-abc/aig/aig/aigPart.c b/src/extlib-abc/aig/aig/aigPart.c +index a4cc116..c486a11 100644 +--- a/src/extlib-abc/aig/aig/aigPart.c ++++ b/src/extlib-abc/aig/aig/aigPart.c +@@ -871,10 +871,6 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi + ***********************************************************************/ + Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) + { +- extern int Cmd_CommandExecute( void * pAbc, char * sCommand ); +- extern void * Abc_FrameGetGlobalFrame(); +- extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax ); +- + Vec_Ptr_t * vOutsTotal, * vOuts; + Aig_Man_t * pAigTotal, * pAigPart, * pAig; + Vec_Int_t * vPart, * vPartSupp; +@@ -898,8 +894,6 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) + Aig_ManForEachPi( pAig, pObj, k ) + pObj->pNext = (Aig_Obj_t *)(long)k; + +- Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" ); +- + // create the total fraiged AIG + vPartSupp = Vec_IntAlloc( 100 ); // maps part PI num into total PI num + Vec_PtrForEachEntry( vParts, vPart, i ) +@@ -936,7 +930,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) + i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), + Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) ); + // compute equivalence classes (to be stored in pNew->pReprs) +- pAig = Fra_FraigChoice( pAigPart, 1000 ); ++ pAig = NULL; + Aig_ManStop( pAig ); + // reset the pData pointers + Aig_ManForEachObj( pAigPart, pObj, k ) +@@ -951,8 +945,6 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) + Vec_VecFree( (Vec_Vec_t *)vParts ); + Vec_IntFree( vPartSupp ); + +- Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" ); +- + // clear the PI numbers + Vec_PtrForEachEntry( vAigs, pAig, i ) + Aig_ManForEachPi( pAig, pObj, k ) +diff --git a/src/extlib-abc/aig/aig/aigShow.c b/src/extlib-abc/aig/aig/aigShow.c +index a88f493..34b26ef 100644 +--- a/src/extlib-abc/aig/aig/aigShow.c ++++ b/src/extlib-abc/aig/aig/aigShow.c +@@ -328,7 +328,6 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * + ***********************************************************************/ + void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) + { +- extern void Abc_ShowFile( char * FileNameDot ); + static int Counter = 0; + char FileNameDot[200]; + FILE * pFile; +@@ -344,8 +343,6 @@ void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) + fclose( pFile ); + // generate the file + Aig_WriteDotAig( pMan, FileNameDot, fHaig, vBold ); +- // visualize the file +- Abc_ShowFile( FileNameDot ); + } + + +diff --git a/src/extlib-abc/aig/kit/kitGraph.c b/src/extlib-abc/aig/kit/kitGraph.c +index 1ae5891..f6ea2ca 100644 +--- a/src/extlib-abc/aig/kit/kitGraph.c ++++ b/src/extlib-abc/aig/kit/kitGraph.c +@@ -20,6 +20,12 @@ + + #include "kit.h" + ++Kit_Graph_t *Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, ++ Vec_Int_t * vMemory ) ++{ ++ return NULL; ++} ++ + //////////////////////////////////////////////////////////////////////// + /// DECLARATIONS /// + //////////////////////////////////////////////////////////////////////// diff --git a/stp-warning.patch b/stp-warning.patch index 69d27f5..a7bfb95 100644 --- a/stp-warning.patch +++ b/stp-warning.patch @@ -1,805 +1,82 @@ ---- ./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) { +diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp +index 0e028c4..7cfa7a7 100644 +--- a/src/AST/ASTmisc.cpp ++++ b/src/AST/ASTmisc.cpp +@@ -154,7 +154,7 @@ namespace BEEV - Expr vc_getCounterExample(VC vc, Expr e) { - nodestar a = (nodestar)e; -- bmstar b = (bmstar)(((stpstar)vc)->bm); - ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); + visited.insert(n.GetNodeNum()); - 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++) + numberOfReadsLessThan(n[i], visited, soFar,limit); + } - 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); +diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +index 9c18b69..4fc3320 100644 +--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp ++++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +@@ -389,7 +389,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) + const ASTNode& in2 = swap ? children[0] : children[1]; + const Kind k1 = in1.GetKind(); + const Kind k2 = in2.GetKind(); +- const int width = in1.GetValueWidth(); ++ const unsigned int width = in1.GetValueWidth(); - bool t = false; -@@ -590,7 +588,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(); -@@ -982,7 +979,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: "\ -@@ -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) { - } - - 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/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 - { - 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; - } -@@ -79,7 +79,7 @@ namespace BEEV - if (n0.size() != n1.size()) - return false; - -- 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 - - 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); - -@@ -787,14 +787,14 @@ namespace BEEV + if (in1 == in2) + //terms are syntactically the same +@@ -526,7 +526,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) + bool foundZero = false, foundOne = false; + const unsigned original_width = in2[0].GetValueWidth(); + const unsigned new_width = in2.GetValueWidth(); +- for (int i = original_width - 1; i < new_width; i++) ++ for (unsigned int i = original_width - 1; i < new_width; i++) + if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(), i)) + foundOne = true; + else +@@ -1176,10 +1176,12 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec & + for (size_t i = 0; i < width; 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)); + if (CONSTANTBV::BitVector_bit_test(c, i)) +- if (start == -1) +- start = i; // first one bit. +- else if (end != -1) +- bad = true; ++ { ++ if (start == -1) ++ start = i; // first one bit. ++ else if (end != -1) ++ bad = true; ++ } -- 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); + if (!CONSTANTBV::BitVector_bit_test(c, i)) + if (start != -1 && end == -1) +@@ -1200,7 +1202,7 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec & + ASTNode z = bm.CreateZeroConst(start); + result = NodeFactory::CreateTerm(BVCONCAT, end + 1, result, z); } -+ } - } - } - } -@@ -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 = 0; i < bitWidth; i++) -+ for (unsigned int i = 0; i < bitWidth; i++) - { - // Copy all the laters into products - while(later[i].size() > 0) -@@ -2302,7 +2303,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); -@@ -2312,7 +2313,7 @@ namespace BEEV - products[i].pop_back(); - } - -- assert(results.size() == ((unsigned)bitWidth)); -+ assert(results.size() == bitWidth); - return results; - } - -@@ -2321,7 +2322,7 @@ namespace BEEV - BBNodeVec - BitBlaster::v8(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; -@@ -2334,14 +2335,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; -@@ -2351,7 +2352,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; -@@ -2362,7 +2363,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) -@@ -2373,14 +2374,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; - } - -@@ -2392,7 +2393,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]; -@@ -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 (end < width - 1) ++ if (end < (int) width - 1) { - 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); + ASTNode z = bm.CreateZeroConst(width - end - 1); + result = NodeFactory::CreateTerm(BVCONCAT, width, z, result); +diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp +index 395e737..ff5cc3d 100644 +--- a/src/STPManager/STP.cpp ++++ b/src/STPManager/STP.cpp +@@ -576,7 +576,7 @@ namespace BEEV { -- 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 + ToSATAIG toSATAIG(bm, cb, arrayTransformer); - // 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 -@@ -149,7 +149,7 @@ public: - Aig_Obj_t * pNode; - assert (children.size() != 0); +- ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ; ++ ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : &toSATAIG; -- 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 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); - // It was ommitted from the initial problem, so assign it freshly. -- for (int i = 0; i < a.GetValueWidth(); i++) -+ for (unsigned int i = 0; i < a.GetValueWidth(); i++) - { - SATSolver::Var v = SatSolver.newVar(); - // We probably don't want the variable eliminated. -@@ -55,7 +55,7 @@ namespace BEEV - getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, ToSATBase::ASTNodeToSATVar& satVar, - Polarity polary = BOTH) - { -- const int width = a.GetValueWidth(); -+ const unsigned int width = a.GetValueWidth(); - assert(width == b.GetValueWidth()); - assert(!a.isConstant() || !b.isConstant()); - -@@ -72,7 +72,7 @@ namespace BEEV - SATSolver::vec_literals all; - const int result = SatSolver.newVar(); - -- for (int i = 0; i < width; i++) -+ for (unsigned int i = 0; i < width; i++) - { - SATSolver::vec_literals s; - -@@ -116,7 +116,7 @@ namespace BEEV + if (bm->soft_timeout_expired) + return SOLVER_TIMEOUT; +diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp +index 4ce3767..b5c061f 100644 +--- a/src/absrefine_counterexample/AbstractionRefinement.cpp ++++ b/src/absrefine_counterexample/AbstractionRefinement.cpp +@@ -119,7 +119,7 @@ namespace BEEV } return result; } @@ -808,16 +85,7 @@ { ASTNode constant = a.isConstant() ? a : b; vector vec = v_a.size() == 0 ? v_b : v_a; -@@ -128,7 +128,7 @@ namespace BEEV - all.push(SATSolver::mkLit(result, false)); - - CBV v = constant.GetBVConst(); -- for (int i = 0; i < width; i++) -+ for (unsigned int i = 0; i < width; i++) - { - if (polary != RIGHT_ONLY) - { -@@ -214,7 +214,7 @@ namespace BEEV +@@ -217,7 +217,7 @@ namespace BEEV void applyAxiomsToSolver(ToSATBase::ASTNodeToSATVar & satVar, vector & toBe, SATSolver & SatSolver) { @@ -826,49 +94,11 @@ { applyAxiomToSAT(SatSolver, toBe[i], satVar); } -@@ -269,7 +269,6 @@ namespace BEEV - for (vector >::const_iterator iset = arrayToIndex.begin(), - iset_end = arrayToIndex.end(); iset != iset_end; iset++) - { -- const ASTNode& ArrName = iset->first; - const map& mapper = iset->second; - - vector listOfIndices; -@@ -318,13 +317,13 @@ namespace BEEV - - //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& index_j = listOfIndices[j]; - -@@ -556,13 +555,13 @@ namespace BEEV - - //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& index_j = listOfIndices[j]; - ---- ./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 +diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp +index 0f52bce..4029a53 100644 +--- a/src/absrefine_counterexample/CounterExample.cpp ++++ b/src/absrefine_counterexample/CounterExample.cpp +@@ -48,7 +48,7 @@ namespace BEEV assert(symbol.GetKind() == SYMBOL); vector bitVector_array(symbolWidth,false); @@ -877,7 +107,7 @@ { const unsigned sat_variable_index = v[index]; -@@ -863,7 +863,7 @@ namespace BEEV +@@ -871,7 +871,7 @@ namespace BEEV ASTNode symbol = it->first; vector v = it->second; @@ -886,321 +116,37 @@ { 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; ibm); -- s->addClause(v); -+ return s->addClause(v); - } - - bool -@@ -71,7 +71,7 @@ namespace BEEV - return s->newVar(); - } - -- 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(); - -- int setVerbosity(int v); -+ void setVerbosity(int v); - - int nVars(); - ---- ./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. - { -- s->addClause(ps); -+ return s->addClause(ps); - } - - bool + 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: "\ +diff --git a/src/cpp_interface/cpp_interface.cpp b/src/cpp_interface/cpp_interface.cpp +index 4da3685..3ce0c3e 100644 +--- a/src/cpp_interface/cpp_interface.cpp ++++ b/src/cpp_interface/cpp_interface.cpp @@ -47,7 +47,7 @@ namespace BEEV - return Minisat::toInt(s->modelValue(x)); - } - -- int SimplifyingMinisat::setVerbosity(int v) -+ void SimplifyingMinisat::setVerbosity(int v) - { - s->verbosity = v; - } ---- ./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/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 - MinisatCore::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver. - { -- s->addClause(ps); -+ return s->addClause(ps); - } - - template -@@ -58,7 +58,7 @@ namespace BEEV - } - - template -- int MinisatCore::setVerbosity(int v) -+ void MinisatCore::setVerbosity(int v) - { - s->verbosity = v; - } -@@ -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; - -- if (i.size() > INDEX_BIT_WIDTH || ki.size() > INDEX_BIT_WIDTH) -+ if (i.size() > (int)INDEX_BIT_WIDTH || ki.size() > (int)INDEX_BIT_WIDTH) - { - printf("The array propagators unfortunately don't do arbitrary precision integers yet. " - "With the INDICES_128BITS compile time flag STP does 128-bits on 64-bit machines compiled with GCC. " -- "Currently STP is compiled to use %d bit indices. " -+ "Currently STP is compiled to use %zu bit indices. " - "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())); -@@ -1136,7 +1136,6 @@ void Solver_prop::analyze(CRef confl, ve - - if (debug_print) - printf("%d %d\n", toInt(p), toInt(var(p))); -- Minisat::Clause cl= ca[confl]; - - assert(ca[confl][0] ==p); - assert(value(p) != l_Undef); ---- ./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; } - typedef uint128_t index_type; -+# define PRIuIT PRIu128 - #else - typedef uint64_t index_type; -+# define PRIuIT PRIu64 - #endif - - #define INDEX_BIT_WIDTH (sizeof(index_type) *8) -@@ -227,7 +229,7 @@ private: - printf("Value Size: %d\n", value.size()); - printClause2(value); - -- printf("Known Index: %ld ", isIndexConstant() ? index_constant : -1); -+ printf("Known Index: %" PRIuIT " ", isIndexConstant() ? index_constant : (index_type)-1); - printf("Known Value: %c\n", isValueConstant() ? 't' : 'f'); - printf("Array ID:%d\n", array_id); - printf("------------\n"); ---- ./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); - -- proof = (FILE*)fclose(proof); -- assert(proof == NULL); -+ int err = fclose(proof); -+ assert(err == 0); -+ proof = NULL; - } - - 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. - { -- s->addClause(ps); -+ return s->addClause(ps); - } - - template -@@ -66,7 +66,7 @@ namespace BEEV - } - - template -- int MinisatCore_prop::setVerbosity(int v) -+ void MinisatCore_prop::setVerbosity(int v) - { - s->verbosity = v; - } ---- ./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(); - -- int setVerbosity(int v); -+ void setVerbosity(int v); - - int nVars(); - ---- ./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); - - 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 = ""; - -- 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 = ""; - -- 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; - -- 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, + // 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/src/extlib-abc/aig/aig/aigShow.c b/src/extlib-abc/aig/aig/aigShow.c +index ae8fa8b..a88f493 100644 +--- a/src/extlib-abc/aig/aig/aigShow.c ++++ b/src/extlib-abc/aig/aig/aigShow.c +@@ -329,7 +329,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) { extern void Abc_ShowFile( char * FileNameDot ); @@ -1209,205 +155,11 @@ 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; -+ - // 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; - - // 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-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 ) - { -- unsigned uCube, uDiv, uCube2, uDiv2, uQuo; -+ unsigned uCube, uDiv, uCube2 = 0, uDiv2, uQuo; - int i, i2, k, k2, nCubesRem; - 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-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 ) - { -- pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); -- pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); -+ pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc, pNode->eEdge0.edgeBits.fCompl ); -+ pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc, pNode->eEdge1.edgeBits.fCompl ); - pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 ); - } - // 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-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) ); - pGraph->fConst = 1; -- pGraph->eRoot.fCompl = 1; -+ pGraph->eRoot.edgeBits.fCompl = 1; - return pGraph; - } - -@@ -109,8 +109,8 @@ Kit_Graph_t * Kit_GraphCreateLeaf( int i - Kit_Graph_t * pGraph; - assert( 0 <= iLeaf && iLeaf < nLeaves ); - pGraph = Kit_GraphCreate( nLeaves ); -- pGraph->eRoot.Node = iLeaf; -- pGraph->eRoot.fCompl = fCompl; -+ pGraph->eRoot.edgeBits.Node = iLeaf; -+ pGraph->eRoot.edgeBits.fCompl = fCompl; - return pGraph; - } - -@@ -174,8 +174,8 @@ Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Grap - // set the inputs and other info - pNode->eEdge0 = eEdge0; - pNode->eEdge1 = eEdge1; -- pNode->fCompl0 = eEdge0.fCompl; -- pNode->fCompl1 = eEdge1.fCompl; -+ pNode->fCompl0 = eEdge0.edgeBits.fCompl; -+ pNode->fCompl1 = eEdge1.edgeBits.fCompl; - return Kit_EdgeCreate( pGraph->nSize - 1, 0 ); - } - -@@ -198,12 +198,12 @@ Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph - // set the inputs and other info - pNode->eEdge0 = eEdge0; - pNode->eEdge1 = eEdge1; -- pNode->fCompl0 = eEdge0.fCompl; -- pNode->fCompl1 = eEdge1.fCompl; -+ pNode->fCompl0 = eEdge0.edgeBits.fCompl; -+ pNode->fCompl1 = eEdge1.edgeBits.fCompl; - // make adjustments for the OR gate - pNode->fNodeOr = 1; -- pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl; -- pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl; -+ pNode->eEdge0.edgeBits.fCompl = !pNode->eEdge0.edgeBits.fCompl; -+ pNode->eEdge1.edgeBits.fCompl = !pNode->eEdge1.edgeBits.fCompl; - return Kit_EdgeCreate( pGraph->nSize - 1, 1 ); - } - -@@ -224,11 +224,11 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Grap - if ( Type == 0 ) - { - // derive the first AND -- eEdge0.fCompl ^= 1; -+ eEdge0.edgeBits.fCompl ^= 1; - eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); -- eEdge0.fCompl ^= 1; -+ eEdge0.edgeBits.fCompl ^= 1; - // derive the second AND -- eEdge1.fCompl ^= 1; -+ eEdge1.edgeBits.fCompl ^= 1; - eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); - // derive the final OR - eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); -@@ -238,12 +238,12 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Grap - // derive the first AND - eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); - // derive the second AND -- eEdge0.fCompl ^= 1; -- eEdge1.fCompl ^= 1; -+ eEdge0.edgeBits.fCompl ^= 1; -+ eEdge1.edgeBits.fCompl ^= 1; - eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); - // derive the final OR - eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); -- eNode.fCompl ^= 1; -+ eNode.edgeBits.fCompl ^= 1; - } - return eNode; - } -@@ -267,7 +267,7 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Grap - // derive the first AND - eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT ); - // derive the second AND -- eEdgeC.fCompl ^= 1; -+ eEdgeC.edgeBits.fCompl ^= 1; - eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE ); - // derive the final OR - eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); -@@ -275,16 +275,16 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Grap - else - { - // complement the arguments -- eEdgeT.fCompl ^= 1; -- eEdgeE.fCompl ^= 1; -+ eEdgeT.edgeBits.fCompl ^= 1; -+ eEdgeE.edgeBits.fCompl ^= 1; - // derive the first AND - eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT ); - // derive the second AND -- eEdgeC.fCompl ^= 1; -+ eEdgeC.edgeBits.fCompl ^= 1; - eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE ); - // derive the final OR - eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); -- eNode.fCompl ^= 1; -+ eNode.edgeBits.fCompl ^= 1; - } - return eNode; - } -@@ -326,10 +326,10 @@ unsigned Kit_GraphToTruth( Kit_Graph_t * - // compute the function for each internal node - Kit_GraphForEachNode( pGraph, pNode, i ) - { -- uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; -- uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; -- uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0; -- uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1; -+ uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc; -+ uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc; -+ uTruth0 = pNode->eEdge0.edgeBits.fCompl? ~uTruth0 : uTruth0; -+ uTruth1 = pNode->eEdge1.edgeBits.fCompl? ~uTruth1 : uTruth1; - uTruth = uTruth0 & uTruth1; - pNode->pFunc = (void *)(long)uTruth; - } ---- ./src/extlib-abc/aig/dar/darRefact.c.orig 2010-03-06 06:48:41.000000000 -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; - Aig_Obj_t * pAnd, * pAnd0, * pAnd1; -- int i, Counter, LevelNew, LevelOld; -+ int i, Counter, LevelNew; - // check for constant function or a literal - if ( Kit_GraphIsConst(pGraph) || Kit_GraphIsVar(pGraph) ) - return 0; -@@ -230,16 +230,16 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig +diff --git a/src/extlib-abc/aig/dar/darRefact.c b/src/extlib-abc/aig/dar/darRefact.c +index d744b4f..83fb3b0 100644 +--- a/src/extlib-abc/aig/dar/darRefact.c ++++ b/src/extlib-abc/aig/dar/darRefact.c +@@ -230,16 +230,16 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, K Kit_GraphForEachNode( pGraph, pNode, i ) { // get the children of this node @@ -1428,16 +180,7 @@ pAnd = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 ); // return -1 if the node is the same as the original root if ( Aig_Regular(pAnd) == pRoot ) -@@ -263,7 +263,7 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig - LevelNew = (int)Aig_Regular(pAnd0)->Level; - else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd1) ) - LevelNew = (int)Aig_Regular(pAnd1)->Level; -- LevelOld = (int)Aig_Regular(pAnd)->Level; -+// LevelOld = (int)Aig_Regular(pAnd)->Level; - // assert( LevelNew == LevelOld ); - } - if ( LevelNew > LevelMax ) -@@ -312,8 +312,8 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Ma +@@ -312,8 +312,8 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_ //printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) ); Kit_GraphForEachNode( pGraph, pNode, i ) { @@ -1448,35 +191,165 @@ pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 ); /* printf( "Checking " ); ---- ./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 +diff --git a/src/extlib-abc/aig/kit/kitAig.c b/src/extlib-abc/aig/kit/kitAig.c +index de301f2..15d39d6 100644 +--- a/src/extlib-abc/aig/kit/kitAig.c ++++ b/src/extlib-abc/aig/kit/kitAig.c +@@ -54,8 +54,8 @@ Aig_Obj_t * Kit_GraphToAigInternal( Aig_Man_t * pMan, Kit_Graph_t * pGraph ) + // build the AIG nodes corresponding to the AND gates of the graph + Kit_GraphForEachNode( pGraph, pNode, i ) + { +- pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); +- pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); ++ pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc, pNode->eEdge0.edgeBits.fCompl ); ++ pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc, pNode->eEdge1.edgeBits.fCompl ); + pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 ); + } + // complement the result if necessary +diff --git a/src/extlib-abc/aig/kit/kitGraph.c b/src/extlib-abc/aig/kit/kitGraph.c +index 39ef587..1ae5891 100644 +--- a/src/extlib-abc/aig/kit/kitGraph.c ++++ b/src/extlib-abc/aig/kit/kitGraph.c +@@ -69,7 +69,7 @@ Kit_Graph_t * Kit_GraphCreateConst0() + pGraph = ALLOC( Kit_Graph_t, 1 ); + memset( pGraph, 0, sizeof(Kit_Graph_t) ); + pGraph->fConst = 1; +- pGraph->eRoot.fCompl = 1; ++ pGraph->eRoot.edgeBits.fCompl = 1; + return pGraph; + } + +@@ -109,8 +109,8 @@ Kit_Graph_t * Kit_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl ) + Kit_Graph_t * pGraph; + assert( 0 <= iLeaf && iLeaf < nLeaves ); + pGraph = Kit_GraphCreate( nLeaves ); +- pGraph->eRoot.Node = iLeaf; +- pGraph->eRoot.fCompl = fCompl; ++ pGraph->eRoot.edgeBits.Node = iLeaf; ++ pGraph->eRoot.edgeBits.fCompl = fCompl; + return pGraph; + } + +@@ -174,8 +174,8 @@ Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edg + // set the inputs and other info + pNode->eEdge0 = eEdge0; + pNode->eEdge1 = eEdge1; +- pNode->fCompl0 = eEdge0.fCompl; +- pNode->fCompl1 = eEdge1.fCompl; ++ pNode->fCompl0 = eEdge0.edgeBits.fCompl; ++ pNode->fCompl1 = eEdge1.edgeBits.fCompl; + return Kit_EdgeCreate( pGraph->nSize - 1, 0 ); + } + +@@ -198,12 +198,12 @@ Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge + // set the inputs and other info + pNode->eEdge0 = eEdge0; + pNode->eEdge1 = eEdge1; +- pNode->fCompl0 = eEdge0.fCompl; +- pNode->fCompl1 = eEdge1.fCompl; ++ pNode->fCompl0 = eEdge0.edgeBits.fCompl; ++ pNode->fCompl1 = eEdge1.edgeBits.fCompl; + // make adjustments for the OR gate + pNode->fNodeOr = 1; +- pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl; +- pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl; ++ pNode->eEdge0.edgeBits.fCompl = !pNode->eEdge0.edgeBits.fCompl; ++ pNode->eEdge1.edgeBits.fCompl = !pNode->eEdge1.edgeBits.fCompl; + return Kit_EdgeCreate( pGraph->nSize - 1, 1 ); + } + +@@ -224,11 +224,11 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edg + if ( Type == 0 ) + { + // derive the first AND +- eEdge0.fCompl ^= 1; ++ eEdge0.edgeBits.fCompl ^= 1; + eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); +- eEdge0.fCompl ^= 1; ++ eEdge0.edgeBits.fCompl ^= 1; + // derive the second AND +- eEdge1.fCompl ^= 1; ++ eEdge1.edgeBits.fCompl ^= 1; + eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); + // derive the final OR + eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); +@@ -238,12 +238,12 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edg + // derive the first AND + eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); + // derive the second AND +- eEdge0.fCompl ^= 1; +- eEdge1.fCompl ^= 1; ++ eEdge0.edgeBits.fCompl ^= 1; ++ eEdge1.edgeBits.fCompl ^= 1; + eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); + // derive the final OR + eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); +- eNode.fCompl ^= 1; ++ eNode.edgeBits.fCompl ^= 1; + } + return eNode; + } +@@ -267,7 +267,7 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edg + // derive the first AND + eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT ); + // derive the second AND +- eEdgeC.fCompl ^= 1; ++ eEdgeC.edgeBits.fCompl ^= 1; + eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE ); + // derive the final OR + eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); +@@ -275,16 +275,16 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edg + else + { + // complement the arguments +- eEdgeT.fCompl ^= 1; +- eEdgeE.fCompl ^= 1; ++ eEdgeT.edgeBits.fCompl ^= 1; ++ eEdgeE.edgeBits.fCompl ^= 1; + // derive the first AND + eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT ); + // derive the second AND +- eEdgeC.fCompl ^= 1; ++ eEdgeC.edgeBits.fCompl ^= 1; + eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE ); + // derive the final OR + eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); +- eNode.fCompl ^= 1; ++ eNode.edgeBits.fCompl ^= 1; + } + return eNode; + } +@@ -326,10 +326,10 @@ unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph ) + // compute the function for each internal node + Kit_GraphForEachNode( pGraph, pNode, i ) + { +- uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; +- uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; +- uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0; +- uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1; ++ uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc; ++ uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc; ++ uTruth0 = pNode->eEdge0.edgeBits.fCompl? ~uTruth0 : uTruth0; ++ uTruth1 = pNode->eEdge1.edgeBits.fCompl? ~uTruth1 : uTruth1; + uTruth = uTruth0 & uTruth1; + pNode->pFunc = (void *)(long)uTruth; + } +diff --git a/src/extlib-abc/kit.h b/src/extlib-abc/kit.h +index af3a1a8..963a977 100644 +--- a/src/extlib-abc/kit.h ++++ b/src/extlib-abc/kit.h @@ -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 ++typedef union Kit_Edge_t_ Kit_Edge_t; ++union Kit_Edge_t_ ++{ + struct { + unsigned fCompl : 1; // the complemented bit + unsigned Node : 30; // the decomposition node pointed by the edge @@ -1485,7 +358,7 @@ }; typedef struct Kit_Node_t_ Kit_Node_t; -@@ -203,18 +206,18 @@ static inline void Kit_SopShrink +@@ -203,18 +206,18 @@ static inline void Kit_SopShrink( Kit_Sop_t * cSop, int nCubesNew ) 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; } @@ -1513,7 +386,7 @@ 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 +@@ -222,14 +225,12 @@ static inline Kit_Node_t * Kit_GraphNode( Kit_Graph_t * pGraph, int i ) 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; } @@ -1532,7 +405,7 @@ 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 +@@ -486,6 +487,18 @@ static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar ) /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -1551,130 +424,426 @@ #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; - - 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 +diff --git a/src/parser/smt2.y b/src/parser/smt2.y +index c48ddaf..f756d66 100644 +--- a/src/parser/smt2.y ++++ b/src/parser/smt2.y +@@ -239,7 +239,7 @@ cmdi: + {} + | LPAREN_TOK PUSH_TOK NUMERAL_TOK RPAREN_TOK { - 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); +- for (int i=0; i < $3;i++) ++ for (unsigned int i=0; i < $3;i++) + { + parserInterface->push(); + } +@@ -247,7 +247,7 @@ cmdi: } + | LPAREN_TOK POP_TOK NUMERAL_TOK RPAREN_TOK + { +- for (int i=0; i < $3;i++) ++ for (unsigned int i=0; i < $3;i++) + parserInterface->pop(); + parserInterface->success(); + } +@@ -307,7 +307,7 @@ STRING_TOK LPAREN_TOK function_params RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVE + BEEV::parserInterface->storeFunction(*$1, *$3, *$11); ---- ./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]); - } + // Next time the variable is used, we want it to be fresh. +- for (int i = 0; i < $3->size(); i++) ++ for (size_t i = 0; i < $3->size(); i++) + BEEV::parserInterface->removeSymbol((*$3)[i]); + + delete $1; +@@ -321,7 +321,7 @@ STRING_TOK LPAREN_TOK function_params RPAREN_TOK BOOL_TOK an_formula + BEEV::parserInterface->storeFunction(*$1, *$3, *$6); -@@ -465,7 +465,7 @@ namespace simplifier + // Next time the variable is used, we want it to be fresh. +- for (int i = 0; i < $3->size(); i++) ++ for (size_t i = 0; i < $3->size(); i++) + BEEV::parserInterface->removeSymbol((*$3)[i]); - assert(FixedBits::equals(newBits, current)); + delete $1; +diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp +index 7129f50..21a5855 100644 +--- a/src/printer/SMTLIB1Printer.cpp ++++ b/src/printer/SMTLIB1Printer.cpp +@@ -215,7 +215,7 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os) + { + string close = ""; -- 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) +- for (int i =0; i < c.size()-1; i++) ++ for (size_t i =0; i < c.size()-1; i++) + { + os << "(" << functionToSMTLIBName(kind,true); + os << " "; +diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp +index 5ee4e98..d446897 100644 +--- a/src/printer/SMTLIB2Printer.cpp ++++ b/src/printer/SMTLIB2Printer.cpp +@@ -213,7 +213,7 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) + { + 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 << " "; +diff --git a/src/simplifier/AlwaysTrue.h b/src/simplifier/AlwaysTrue.h +index e74df19..eaf0c9d 100644 +--- a/src/simplifier/AlwaysTrue.h ++++ b/src/simplifier/AlwaysTrue.h +@@ -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)); + } +diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h +index 7c762b1..34c92c1 100644 +--- a/src/simplifier/EstablishIntervals.h ++++ b/src/simplifier/EstablishIntervals.h +@@ -120,7 +120,7 @@ namespace BEEV + ASTVec new_children; + new_children.reserve(result.GetChildren().size()); + +- 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)); + + if (new_children == result.GetChildren()) +@@ -499,7 +499,7 @@ namespace BEEV + result = freshUnsignedInterval(n.GetValueWidth()); + + // 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); +@@ -512,7 +512,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) +@@ -520,13 +520,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); +@@ -601,7 +601,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++) { ---- ./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; + if (children[i] == NULL) + { +@@ -617,7 +617,7 @@ namespace BEEV + if (CONSTANTBV::Set_Max(max) >= 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; +@@ -690,7 +690,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) + { +@@ -719,7 +719,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); +@@ -736,7 +736,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); +@@ -757,7 +757,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; +@@ -766,7 +766,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(); + } + } +@@ -799,10 +799,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(); +diff --git a/src/simplifier/FindPureLiterals.h b/src/simplifier/FindPureLiterals.h +index 4b03916..4ff05bc 100644 +--- a/src/simplifier/FindPureLiterals.h ++++ b/src/simplifier/FindPureLiterals.h +@@ -111,7 +111,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; + +@@ -122,7 +122,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; } -+ return false; - } +diff --git a/src/simplifier/MutableASTNode.h b/src/simplifier/MutableASTNode.h +index 3e9a8e2..4d37b8e 100644 +--- a/src/simplifier/MutableASTNode.h ++++ b/src/simplifier/MutableASTNode.h +@@ -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)); ---- ./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); + MutableASTNode * mut = createNode(n); -- int substitutionsLastApplied; -+ size_t substitutionsLastApplied; - public: +- for (int i = 0; i < n.Degree(); i++) ++ for (size_t i = 0; i < n.Degree(); i++) + tempChildren[i]->parents.insert(mut); - 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 - } + mut->children.insert(mut->children.end(),tempChildren.begin(),tempChildren.end()); +@@ -86,7 +86,7 @@ private: + assert(found); + } - 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 < 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; -- 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()); + 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)); - //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; + // 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); ---- ./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 + propagateUpDirty(); +@@ -249,7 +249,7 @@ private: + + ASTNode& node = all[i]->n; + bool found[node.GetValueWidth()]; +- for (int j=0; j CreateTerm(BVNEG, width, rhs)); + + if (lhs.GetKind() == BVXOR || lhs.GetKind() == BVPLUS) +- for (int i = 0; i < lhs.Degree(); i++) ++ for (size_t i = 0; i < lhs.Degree(); i++) + { + ASTVec others; +- for (int j = 0; j < lhs.Degree(); j++) ++ for (size_t j = 0; j < lhs.Degree(); j++) + if (j != i) + others.push_back(lhs[j]); + +diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp +index ca5dd81..0fa3803 100644 +--- a/src/simplifier/RemoveUnconstrained.cpp ++++ b/src/simplifier/RemoveUnconstrained.cpp +@@ -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(); +@@ -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)); + +diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp +index 5a2abd5..d7a2a61 100644 +--- a/src/simplifier/SubstitutionMap.cpp ++++ b/src/simplifier/SubstitutionMap.cpp +@@ -216,7 +216,7 @@ namespace BEEV + 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. +diff --git a/src/simplifier/UseITEContext.h b/src/simplifier/UseITEContext.h +index 5d95d39..45f8d2f 100644 +--- a/src/simplifier/UseITEContext.h ++++ b/src/simplifier/UseITEContext.h @@ -28,7 +28,7 @@ namespace BEEV if (n.GetKind() == NOT && n[0].GetKind() == OR) { @@ -1693,28 +862,142 @@ 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; +diff --git a/src/simplifier/VariablesInExpression.cpp b/src/simplifier/VariablesInExpression.cpp +index 0bdc37f..656a5a7 100644 +--- a/src/simplifier/VariablesInExpression.cpp ++++ b/src/simplifier/VariablesInExpression.cpp +@@ -42,7 +42,7 @@ Symbols* VariablesInExpression::getSymbol(const ASTNode& n) { + } -@@ -121,7 +121,7 @@ public: + 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::SetofVarsSeenInTerm(Symbols* symbol, bool& d + vector av; + VarSeenInTerm(symbol,visited,*symbols,av); - 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; +- 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::VarSeenInTerm(const ASTNode& var, + 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; + +diff --git a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp +index 7958269..1dded88 100644 +--- a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp ++++ b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp +@@ -129,6 +129,7 @@ fast_exit(FixedBits& c0, FixedBits& c1) + } + return false; } ---- ./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 ++ return true; + } + + +diff --git a/src/simplifier/constantBitP/ConstantBitP_Division.cpp b/src/simplifier/constantBitP/ConstantBitP_Division.cpp +index dea6eb1..4d8f64c 100644 +--- a/src/simplifier/constantBitP/ConstantBitP_Division.cpp ++++ b/src/simplifier/constantBitP/ConstantBitP_Division.cpp +@@ -157,14 +157,14 @@ Result bvUnsignedQuotientAndRemainder(vector& children, + 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); + } + +diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp +index d4f5319..8ac4a37 100644 +--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp ++++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp +@@ -433,7 +433,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]); + } + +@@ -469,7 +469,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])) +diff --git a/src/simplifier/constantBitP/FixedBits.cpp b/src/simplifier/constantBitP/FixedBits.cpp +index 273175a..1fe1686 100644 +--- a/src/simplifier/constantBitP/FixedBits.cpp ++++ b/src/simplifier/constantBitP/FixedBits.cpp +@@ -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) + { +diff --git a/src/simplifier/constantBitP/MersenneTwister.h b/src/simplifier/constantBitP/MersenneTwister.h +index bd63d31..238fa3f 100644 +--- a/src/simplifier/constantBitP/MersenneTwister.h ++++ b/src/simplifier/constantBitP/MersenneTwister.h +@@ -231,7 +231,7 @@ inline void MTRand::seed( uint32 *const bigSeed, const uint32 seedLength ) + initialize(19650218UL); + int i = 1; + uint32 j = 0; +- int k = ( N > seedLength ? N : seedLength ); ++ int k = ( N > seedLength ? (int) N : seedLength ); + for( ; k; --k ) + { + state[i] = +diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp +index 46ac6e8..24cdbf6 100644 +--- a/src/simplifier/consteval.cpp ++++ b/src/simplifier/consteval.cpp +@@ -37,13 +37,13 @@ namespace BEEV + CBV tmp0 = NULL; + CBV tmp1 = NULL; + +- unsigned int number_of_children = input_children.size(); ++ size_t number_of_children = input_children.size(); + assert(number_of_children >=1); + assert(k != BVCONST); + + ASTVec children; + children.reserve(number_of_children); +- for (int i =0; i < number_of_children; i++) ++ for (size_t i =0; i < number_of_children; i++) + { + if (input_children[i].isConstant()) + children.push_back(input_children[i]); +diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp +index b309a8a..76cfb04 100644 +--- a/src/simplifier/simplifier.cpp ++++ b/src/simplifier/simplifier.cpp @@ -248,7 +248,7 @@ namespace BEEV assert(false); } @@ -1781,15 +1064,7 @@ 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 +@@ -2658,7 +2659,7 @@ namespace BEEV assert(BVTypeCheck(output)); // If the leading bits are zero. Replace it by a concat with zero. @@ -1798,7 +1073,7 @@ 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 +@@ -2680,13 +2681,13 @@ namespace BEEV } if (output.GetKind() == BVAND) { @@ -1815,7 +1090,7 @@ for (j = 0; j < n.GetValueWidth(); j++) if (CONSTANTBV::BitVector_bit_test(n.GetBVConst(), j)) break; -@@ -2692,7 +2692,7 @@ namespace BEEV +@@ -2703,7 +2704,7 @@ namespace BEEV //cerr << "old" << output; ASTNode zeroes = _bm->CreateZeroConst(trailingZeroes); ASTVec newChildren; @@ -1824,455 +1099,86 @@ 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 +diff --git a/src/to-sat/ASTNode/ToSAT.cpp b/src/to-sat/ASTNode/ToSAT.cpp +index 9fa5ebc..72d41b5 100644 +--- a/src/to-sat/ASTNode/ToSAT.cpp ++++ b/src/to-sat/ASTNode/ToSAT.cpp +@@ -53,7 +53,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; + // 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() == BOOLEXTRACT && n[0].GetKind() == SYMBOL || (n.GetKind() == SYMBOL && !isTseitinVariable(n))) ++ if ((n.GetKind() == BOOLEXTRACT && n[0].GetKind() == SYMBOL) || (n.GetKind() == SYMBOL && !isTseitinVariable(n))) + { + const ASTNode& symbol = n.GetKind() == BOOLEXTRACT ? n[0] : n; + const unsigned index = n.GetKind() == BOOLEXTRACT ? n[1].GetUnsignedConst() : 0; +@@ -313,7 +313,7 @@ namespace BEEV + ClauseBuckets::iterator itend = cb->end(); -@@ -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 + ClauseList *cl = (*it).second; + sat = toSATandSolve(SatSolver,*cl, count==cb->size(),cm); +diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp +index 401119c..d72ffa6 100644 +--- a/src/to-sat/BitBlaster.cpp ++++ b/src/to-sat/BitBlaster.cpp +@@ -1678,13 +1678,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; ++ } } - 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) + return NULL; +@@ -1831,22 +1831,24 @@ namespace BEEV + for (int i = 0; i < b->getWidth(); i++) { -@@ -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 (b->isFixed(i)) +- if (b->getValue(i)) +- { +- assert(v[i]== BBTrue); +- } +- else +- { +- if (v[i] != BBFalse) ++ { ++ if (b->getValue(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)); +- cerr << *b; +- cerr << i << endl; +- cerr << n; +- cerr << (v[i] == BBTrue) << endl; ++ assert(v[i]== BBTrue); + } ++ else ++ { ++ if (v[i] != BBFalse) ++ { ++ cerr << *b; ++ cerr << i << endl; ++ cerr << n; ++ cerr << (v[i] == BBTrue) << endl; ++ } -@@ -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(); -- const int width = in1.GetValueWidth(); -+ const unsigned int width = in1.GetValueWidth(); - - if (in1 == in2) - //terms are syntactically the same -@@ -462,8 +462,8 @@ SimplifyingNodeFactory::CreateSimpleEQ(c - { - int match1 = -1, match2 = -1; - -- for (int i = 0; i < c1.size(); i++) -- for (int j = 0; j < c2.size(); j++) -+ for (int i = 0; (size_t)i < c1.size(); i++) -+ for (int j = 0; (size_t)j < c2.size(); j++) - { - if (c1[i] == c2[j]) - { -@@ -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(); -- for (int i = original_width - 1; i < new_width; i++) -+ for (unsigned int i = original_width - 1; i < new_width; i++) - if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(), i)) - foundOne = true; - else -@@ -1107,7 +1107,7 @@ SimplifyingNodeFactory::CreateTerm(Kind - bool oneFound = false; - bool zeroFound = false; - -- for (int i = 0; i < children.size(); i++) -+ for (size_t i = 0; i < children.size(); i++) - { - if (children[i].GetKind() == BEEV::BVCONST) - { -@@ -1126,7 +1126,7 @@ SimplifyingNodeFactory::CreateTerm(Kind - else if (oneFound) - { - ASTVec new_children; -- for (int i = 0; i < children.size(); i++) -+ for (size_t i = 0; i < children.size(); i++) - { - if (children[i].GetKind() != BEEV::BVCONST || !CONSTANTBV::BitVector_is_full(children[i].GetBVConst())) - new_children.push_back(children[i]); -@@ -1166,13 +1166,14 @@ SimplifyingNodeFactory::CreateTerm(Kind - int end = -1; - BEEV::CBV c = c0.GetBVConst(); - bool bad = false; -- for (int i = 0; i < width; i++) -+ for (unsigned int i = 0; i < width; i++) - { -- if (CONSTANTBV::BitVector_bit_test(c, i)) -+ if (CONSTANTBV::BitVector_bit_test(c, i)) { - if (start == -1) - start = i; // first one bit. - else if (end != -1) - bad = true; +- assert(v[i]== BBFalse); +- } ++ assert(v[i]== BBFalse); ++ } + } - - if (!CONSTANTBV::BitVector_bit_test(c, i)) - if (start != -1 && end == -1) -@@ -1193,7 +1194,7 @@ SimplifyingNodeFactory::CreateTerm(Kind - ASTNode z = bm.CreateZeroConst(start); - result = NodeFactory::CreateTerm(BVCONCAT, end + 1, result, z); - } -- if (end < width - 1) -+ if (end < (int)width - 1) - { - ASTNode z = bm.CreateZeroConst(width - end - 1); - result = NodeFactory::CreateTerm(BVCONCAT, width, z, result); -@@ -1256,7 +1257,6 @@ SimplifyingNodeFactory::CreateTerm(Kind - const unsigned outerHigh = children[1].GetUnsignedConst(); - - const unsigned innerLow = children[0][2].GetUnsignedConst(); -- const unsigned innerHigh = children[0][1].GetUnsignedConst(); - result = NodeFactory::CreateTerm(BVEXTRACT, width, children[0][0], bm.CreateBVConst(32, outerHigh + innerLow), - bm.CreateBVConst(32, outerLow + innerLow)); - } ---- ./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; - - 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 - - visited.insert(n.GetNodeNum()); - -- for (int i = 0; i < n.Degree(); i++) -+ for (size_t i = 0; i < n.Degree(); i++) - numberOfReadsLessThan(n[i], visited, soFar,limit); - } - + } + } + } diff --git a/stp.spec b/stp.spec index b5bb2f3..904b4f0 100644 --- a/stp.spec +++ b/stp.spec @@ -1,38 +1,34 @@ # Upstream occasionally releases a subversion snapshot, but no "regular" # releases since the 0.1 release. -%global svnver 1673 -%global svntim 20130223svn +%global gitdate 20140319 +%global gittag fe766c9add6f80453ec14f4a3b4d5cf3a0385551 +%global shorttag %(echo %{gittag} | cut -b -7) +%global user stp Name: stp Version: 0.1 -Release: 18.%{svntim}%{?dist} +Release: 19.%{gitdate}git.%{shorttag}%{?dist} Summary: Constraint solver/decision procedure Group: Applications/Engineering License: MIT -URL: http://sourceforge.net/projects/stp-fast-prover/ -# The source for this package was pulled from upstream's subversion repository. -# Use the following commands to generate the tarball: -# -# svn export -r %%{svnver} \ -# https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp \ -# 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 +URL: http://stp.github.io/stp/ +Source0: https://github.com/%{user}/%{name}/tarball/%{gittag}/%{user}-%{name}-%{shorttag}.tar.gz +# This patch is specific to Fedora. Use the existing cryptominisat library +# instead of the bundled version. +Patch0: %{name}-unbundle.patch # This patch has not yet been sent upstream. Fix a bunch of compiler warnings # that may indicate miscompiled code. -Patch1: stp-warning.patch +Patch1: %{name}-warning.patch +# This patch has not yet been sent upstream. Eliminate undefined symbols. +Patch2: %{name}-undefined.patch BuildRequires: bison BuildRequires: boost-devel +BuildRequires: cmake BuildRequires: cryptominisat-devel BuildRequires: flex -BuildRequires: time -BuildRequires: valgrind -BuildRequires: zlib-devel +BuildRequires: python2 %description STP (Simple Theorem Prover) is a constraint solver (also referred to as @@ -56,85 +52,53 @@ Additional information can be found at: Summary: Development files for STP constraint solver/decision procedure Group: Applications/Engineering Requires: %{name}%{?_isa} = %{version}-%{release} -Provides: %{name}-static = %{version}-%{release} -# This "devel" package provides a static (not dynamic) library because: -# 1. This is the normal usage mode when linking this as a library; -# it's what upstream and existing programs that use this program expect. -# 2. This speeds execution. In this library, speed matters. -# There's a speed penalty for .so files, and this program is much -# like a chess program - it's essentially an inner loop that searches -# a massive space of possibilities. -# A dynamic .so version could be create using: -# gcc -shared -Wl,-soname,libstp.so.1 -o libstp.so.1.0.1 libstp.a -# but this would require -fpic to compile (slowing the results). -# See my document: -# http://www.dwheeler.com/program-library/Program-Library-HOWTO/ + %description devel Development files for the STP (Simple Theorem Prover), a constraint solver (also referred to as a decision procedure or automated prover). Provides a static library. %prep -%setup -q -%patch0 -%patch1 +%setup -q -n %{user}-%{name}-%{shorttag} +%patch0 -p1 +%patch1 -p1 +%patch2 -p1 -# Make sure nothing uses the shipped boost or cryptominisat sources -rm -fr src/boost src/sat/cryptominisat2 +# Make sure nothing uses the shipped cryptominisat sources +rm -fr src/sat/cryptominisat2 # We do not want to know about the order of member initializers -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 -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 - -# Fix underlinked tests -sed -i 's/^LIBS=.*/& -lcryptominisat -lm/' tests/c-api-tests/Makefile +sed -i "s/-Wno-deprecated/& -Wno-reorder/" CMakeLists.txt %build -scripts/configure --with-prefix=%{_prefix} - -# DO NOT use _smp_mflags; build will fail. -make all OPTIMIZE="%{optflags} -DNDEBUG" LIB_DIR=%{_libdir} \ - LDFLAGS="$RPM_LD_FLAGS -lcryptominisat" +%cmake %install -mkdir -p %{buildroot}%{_bindir} -mkdir -p %{buildroot}%{_includedir}/stp -mkdir -p %{buildroot}%{_libdir} +make install DESTDIR=%{buildroot} -# This "make install" doesn't support DESTDIR=%%{buildroot}. -# We'll rig PREFIX/LIB_DIR, since that happens to work for this makefile. -make install PREFIX=%{buildroot}%{_prefix} LIB_DIR=%{buildroot}%{_libdir} - -%check -# Most of the tests are broken. Run the ones that aren't. -export PATH=$PATH:%{buildroot}%{_bindir} -make check -%ifarch %{ix86} x86_64 -# On non-x86 architectures, the memory leak tests tend to fail, because -# valgrind finds problems in glibc itself. Also, the non-valgrind tests -# tend to fail because they time out. Until valgrind works and I can figure -# out how to adapt the timeout estimates for such architectures, skip these -# tests. -make regressstp -make regresscapi -%endif +# Fix up the libdir install on 64-bit targets +if [ %{__isa_bits} = "64" ]; then + mkdir %{buildroot}%{_libdir} + mv %{buildroot}%{_prefix}/lib/cmake %{buildroot}%{_libdir} + mv %{buildroot}%{_prefix}/lib/libstp.so %{buildroot}%{_libdir} +fi %files %{_bindir}/* -%doc AUTHORS README LICENSE LICENSE_COMPONENTS papers +%{_libdir}/libstp.so +%doc AUTHORS README.markdown LICENSE LICENSE_COMPONENTS papers %files devel -%{_libdir}/libstp*.a %{_includedir}/stp/ +%{_libdir}/cmake/STP/ %changelog +* Wed Mar 19 2014 Jerry James - 0.1-19.20140319git.6110a49 +- Update to recent git snapshot, now hosted on github +- Build now uses cmake +- Tests now need boolector, which has license problems. Disable %%check for + now unless we can find something useful to do. + * Wed Oct 9 2013 Jerry James - 0.1-18.20130223svn - Really rebuild for cryptominisat 2.9.8