[stp] Update to recent git snapshot, now hosted on github. Build now uses cmake. Tests now need boolector,
Jerry James
jjames at fedoraproject.org
Wed Mar 19 23:09:51 UTC 2014
commit 5a3a024fae7e721b13c74ebdffc57dc4d6e3dabb
Author: Jerry James <jamesjer at betterlinux.com>
Date: Wed Mar 19 17:09:33 2014 -0600
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 | 473 +++-------
stp-undefined.patch | 80 ++
stp-warning.patch | 2668 +++++++++++++++------------------------------------
stp.spec | 118 +--
6 files changed, 1056 insertions(+), 2287 deletions(-)
---
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 @@
-
- #include "../AST/AST.h"
- #include "../STPManager/STPManager.h"
--#include "../boost/noncopyable.hpp"
-+#include <boost/noncopyable.hpp>
-
- namespace BEEV
- {
---- ./src/to-sat/AIG/ToCNFAIG.h.orig 2012-01-23 15:51:23.000000000 -0700
-+++ ./src/to-sat/AIG/ToCNFAIG.h 2012-08-07 16:22:05.823811600 -0600
-@@ -6,7 +6,7 @@
- #include "../../extlib-abc/dar.h"
- #include "../ToSATBase.h"
- #include "BBNodeManagerAIG.h"
--#include "../../boost/noncopyable.hpp"
-+#include <boost/noncopyable.hpp>
-
- 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 <boost/noncopyable.hpp>
-
- 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 <cassert>
- #include <map>
- #include "../STPManager/STPManager.h"
--#include "../boost/noncopyable.hpp"
-+#include <boost/noncopyable.hpp>
- #include <list>
- #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 <boost/noncopyable.hpp>
+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()
+
+ check_cxx_compiler_flag("-std=gnu++11" HAVE_FLAG_STD_GNUPP11)
+@@ -179,6 +180,7 @@ include_directories(${Boost_INCLUDE_DIRS})
+
+ 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 <iostream>
+ #include <utility>
+ #include "RunTimes.h"
+-#include "../sat/cryptominisat2/time_mem.h"
++#include <cmsat/time_mem.h>
+
+ // 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 <boost/utility.hpp>
+ #include <iostream>
+ #include <sstream>
+-#include "../sat/cryptominisat2/time_mem.h"
++#include <cmsat/time_mem.h>
- namespace BEEV
+ class RunTimes : boost::noncopyable
{
---- ./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 @@
+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)
+
+
+ # -----------------------------------------------------------------------------
+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)
+
+ 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 <cmsat/Solver.h>
++#include <cmsat/SolverTypes.h>
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 <boost/noncopyable.hpp>
-
- 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 <stack>
--#include "../boost/noncopyable.hpp"
-+#include <boost/noncopyable.hpp>
-
- 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 <assert.h>
- #include <iostream>
- #include <set>
--#include "../boost/noncopyable.hpp"
-+#include <boost/noncopyable.hpp>
-
- 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 <boost/noncopyable.hpp>
-
- 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 <list>
- #include "../STPManager/NodeIterator.h"
--#include "../boost/noncopyable.hpp"
-+#include <boost/noncopyable.hpp>
-
- // 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 <boost/noncopyable.hpp>
-
- 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 <boost/noncopyable.hpp>
-
- 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 <boost/noncopyable.hpp>
-
- 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 <boost/noncopyable.hpp>
-
- 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 <boost/noncopyable.hpp>
-
- 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 <boost/noncopyable.hpp>
-
- // 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 <boost/noncopyable.hpp>
-
- 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 <boost/noncopyable.hpp>
-
-
- 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 <boost/noncopyable.hpp>
-
- 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 <boost/noncopyable.hpp>
-
- 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 <boost/noncopyable.hpp>
-
- //This finds conjuncts which are one of: (= SYMBOL BVCONST), (= BVCONST (READ SYMBOL BVCONST)),
- // (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL)
---- ./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 <boost/noncopyable.hpp>
-
- 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 <vector>
- #include "../ASTKind.h"
--#include "../../boost/noncopyable.hpp"
-+#include <boost/noncopyable.hpp>
-
- 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 <boost/noncopyable.hpp>
-
- 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 <string>
- #include "../sat/utils/System.h"
- #include <iomanip>
--#include "../boost/noncopyable.hpp"
-+#include <boost/noncopyable.hpp>
-
- class RunTimes : boost::noncopyable
- {
+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)
+
+ # -----------------------------------------------------------------------------
+ # 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);
-
- bool t = false;
-@@ -570,7 +569,6 @@ Expr vc_getCounterExample(VC vc, Expr e)
-
- void vc_getCounterExampleArray(VC vc, Expr e, Expr **indices, Expr **values, int *size) {
- nodestar a = (nodestar)e;
-- bmstar b = (bmstar)(((stpstar)vc)->bm);
- ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);
-
- bool t = false;
-@@ -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<BEEV::ASTNode *>::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<BBNode>& 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<BBNode, BBNodeManagerT>::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
- {
- // Add all the children up using an addition network.
- vector<BBNodeVec> results;
-- for (int i = 0; i < term.Degree(); i++)
-+ for (size_t i = 0; i < term.Degree(); i++)
- results.push_back(BBTerm(term[i], support));
-
-- const int bitWidth = term[0].GetValueWidth();
-+ const unsigned int bitWidth = term[0].GetValueWidth();
- std::vector<list<BBNode> > 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<BBNode, BBNodeManagerT>::buildAdditionNetworkResult(vector<list<BBNode> >& products, set<BBNode>& 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<BBNode, BBNodeManagerT>::multWithBounds(const ASTNode&n, vector<list<BBNode> >& 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<BBNode> 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<BBNode, BBNodeManagerT>::mult_normal(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support,
- const ASTNode&n)
- {
-- const int bitWidth = n.GetValueWidth();
-+ const unsigned int bitWidth = n.GetValueWidth();
-
- // If we have details of the partial products which can be true,
- int highestZero = -1;
-@@ -1698,7 +1698,7 @@ namespace BEEV
-
- BBNodeVec prod = BBNodeVec(BBAndBit(y, *x.begin())); // start prod with first partial product.
-
-- for (int i = 1; i < bitWidth; i++) // start loop at next bit.
-+ for (unsigned int i = 1; i < bitWidth; i++) // start loop at next bit.
- {
- const BBNode& xit = x[i];
-
-@@ -1715,7 +1715,7 @@ namespace BEEV
- BBNodeVec pprod = BBAndBit(ycopy, xit);
-
- // Iterate through from the current location upwards, setting anything to zero that can be..
-- if (ms != NULL && highestZero >= i)
-+ if (ms != NULL && highestZero >= (int)i)
- {
- for (int column = i; column <= highestZero; column++)
- {
-@@ -1740,7 +1740,7 @@ namespace BEEV
- {
-
- // Add the carry from the prior column. i.e. each second sorted formula.
-- for (int k = 1; k < priorSorted.size(); k += 2)
-+ for (size_t k = 1; k < priorSorted.size(); k += 2)
- {
- current.push_back(priorSorted[k]);
- }
-@@ -1820,7 +1820,7 @@ namespace BEEV
- FixedBits* b = cb->fixedMap->map->find(n)->second;
- for (int i = 0; i < b->getWidth(); i++)
- {
-- if (b->isFixed(i))
-+ if (b->isFixed(i)) {
- if (b->getValue(i))
- {
- assert(v[i]== BBTrue);
-@@ -1837,6 +1837,7 @@ namespace BEEV
-
- assert(v[i]== BBFalse);
- }
-+ }
- }
- }
- }
-@@ -1850,7 +1851,7 @@ namespace BEEV
- BitBlaster<BBNode, BBNodeManagerT>::setColumnsToZero(vector<list<BBNode> >& products, set<BBNode>& 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<BBNode> 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 <BBNode> 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<BBNode> 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<BBNode, BBNodeManagerT>::v6(vector<list<BBNode> >& products, set<BBNode>& support, const ASTNode&n)
- {
-- const int bitWidth = n.GetValueWidth();
-+ const unsigned int bitWidth = n.GetValueWidth();
-
- vector<BBNode> prior;
-
-- for (int i = 0; i < bitWidth; i++)
-+ for (unsigned int i = 0; i < bitWidth; i++)
- {
- vector<BBNode> output;
- sortingNetworkAdd(support, products[i], output ,prior);
-@@ -2101,7 +2102,7 @@ namespace BEEV
- BBNodeVec
- BitBlaster<BBNode, BBNodeManagerT>::v13(vector<list<BBNode> >& products, set<BBNode>& 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<BBNode, BBNodeManagerT>::v9(vector<list<BBNode> >& products, set<BBNode>& 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<BBNode> sorted; // The current column (sorted) gets put into here.
- vector<BBNode> 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<BBNode, BBNodeManagerT>::v7(vector<list<BBNode> >& products, set<BBNode>& 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<list<BBNode> > later(bitWidth+1);
- std::vector<list<BBNode> > 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();
- }
+ visited.insert(n.GetNodeNum());
-- assert(results.size() == ((unsigned)bitWidth));
-+ assert(results.size() == bitWidth);
- return results;
+- for (int i = 0; i < n.Degree(); i++)
++ for (size_t i = 0; i < n.Degree(); i++)
+ numberOfReadsLessThan(n[i], visited, soFar,limit);
}
-@@ -2321,7 +2322,7 @@ namespace BEEV
- BBNodeVec
- BitBlaster<BBNode, BBNodeManagerT>::v8(vector<list<BBNode> >& products, set<BBNode>& 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<list<BBNode> > later(bitWidth+1); // +1 then ignore the topmost.
- std::vector<list<BBNode> > next(bitWidth+1);
+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();
-- for (int i = 0; i < bitWidth; i++)
-+ for (unsigned int i = 0; i < bitWidth; i++)
+ 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++)
{
- // 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<BBNode> result(in);
+ 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;
++ }
-- 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 <BBNode> evenL;
- vector <BBNode> 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 <BBNode> evenR; // Take the even of each.
- vector <BBNode> oddR; // Take the odd of each
-- for (int i =0; i < in2.size();i++)
-+ for (size_t i =0; i < in2.size();i++)
- {
- if (i%2 ==0)
- evenR.push_back(in2[i]);
-@@ -2450,7 +2451,7 @@ namespace BEEV
- vector <BBNode> even = evenL.size()< evenR.size() ? mergeSorted(evenR,evenL) : mergeSorted(evenL,evenR);
- vector <BBNode> odd = oddL.size() < oddR.size() ? mergeSorted(oddR,oddL) : mergeSorted(oddL,oddR);
-
-- for (int i =0; i < std::max(even.size(),odd.size());i++)
-+ for (size_t i =0; i < std::max(even.size(),odd.size());i++)
+ if (!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);
+ }
+- if (end < width - 1)
++ if (end < (int) width - 1)
{
- if (even.size() > i)
- result.push_back(even[i]);
-@@ -2495,7 +2496,7 @@ namespace BEEV
-
- // check if y is already zero.
- bool isZero = true;
-- for (int i = 0; i < rwidth; i++)
-+ for (unsigned int i = 0; i < rwidth; i++)
- if (y[i] != nf->getFalse())
- {
- isZero = false;
---- ./src/to-sat/AIG/BBNodeManagerAIG.h.orig 2012-01-29 20:28:39.000000000 -0700
-+++ ./src/to-sat/AIG/BBNodeManagerAIG.h 2012-08-07 16:26:11.736851970 -0600
-@@ -149,7 +149,7 @@ public:
- Aig_Obj_t * pNode;
- assert (children.size() != 0);
-
-- for (int i =0; i < children.size();i++)
-+ for (size_t i =0; i < children.size();i++)
- assert(!children[i].IsNull());
-
- switch (kind)
---- ./src/to-sat/AIG/ToSATAIG.cpp.orig 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<unsigned>& 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<unsigned>& 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<unsigned> 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<unsigned>& 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 ASTNode*>::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());
+ 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 {
-@@ -72,7 +72,7 @@ namespace BEEV
- SATSolver::vec_literals all;
- const int result = SatSolver.newVar();
+ ToSATAIG toSATAIG(bm, cb, arrayTransformer);
-- for (int i = 0; i < width; i++)
-+ for (unsigned int i = 0; i < width; i++)
- {
- SATSolver::vec_literals s;
+- ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ;
++ ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : &toSATAIG;
-@@ -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<unsigned> 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<AxiomToBe> & toBe, SATSolver & SatSolver)
{
@@ -826,49 +94,11 @@
{
applyAxiomToSAT(SatSolver, toBe[i], satVar);
}
-@@ -269,7 +269,6 @@ namespace BEEV
- for (vector<pair<ASTNode, ArrayTransformer::arrTypeMap> >::const_iterator iset = arrayToIndex.begin(),
- iset_end = arrayToIndex.end(); iset != iset_end; iset++)
- {
-- const ASTNode& ArrName = iset->first;
- const map<ASTNode, ArrayTransformer::ArrayRead>& mapper = iset->second;
-
- vector<ASTNode> 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<bool> 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<unsigned> 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; i<ps.size();i++)
- v.push(CMSat::Lit(var(ps[i]), sign(ps[i])));
-
-- 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
-@@ -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<T>::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver.
- {
-- s->addClause(ps);
-+ return s->addClause(ps);
- }
-
- template <class T>
-@@ -58,7 +58,7 @@ namespace BEEV
- }
-
- template <class T>
-- int MinisatCore<T>::setVerbosity(int v)
-+ void MinisatCore<T>::setVerbosity(int v)
- {
- s->verbosity = v;
- }
-@@ -97,7 +97,7 @@ namespace BEEV
- template <class T>
- bool MinisatCore<T>::simplify()
- {
-- s->simplify();
-+ return s->simplify();
- }
-
+diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
+index dd761d3..2876211 100644
+--- a/src/c_interface/c_interface.cpp
++++ b/src/c_interface/c_interface.cpp
+@@ -989,7 +989,7 @@ Expr vc_bvConstExprFromInt(VC vc,
+ bmstar b = (bmstar)(((stpstar)vc)->bm);
---- ./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
+ 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
-
- 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<T>::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver.
- {
-- s->addClause(ps);
-+ return s->addClause(ps);
- }
-
- template <class T>
-@@ -66,7 +66,7 @@ namespace BEEV
- }
-
- template <class T>
-- int MinisatCore_prop<T>::setVerbosity(int v)
-+ void MinisatCore_prop<T>::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,57 +155,47 @@
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_
+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
+- pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node );
+- pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node );
++ pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.edgeBits.Node );
++ pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.edgeBits.Node );
+ // get the AIG nodes corresponding to the children
+ pAnd0 = pNode0->pFunc;
+ pAnd1 = pNode1->pFunc;
+ if ( pAnd0 && pAnd1 )
+ {
+ // if they are both present, find the resulting node
+- pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.fCompl );
+- pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.fCompl );
++ pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.edgeBits.fCompl );
++ pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.edgeBits.fCompl );
+ pAnd = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 );
+ // return -1 if the node is the same as the original root
+ if ( Aig_Regular(pAnd) == pRoot )
+@@ -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 )
+ {
+- 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( pAig, pAnd0, pAnd1 );
+ /*
+ printf( "Checking " );
+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 )
{
@@ -1270,8 +206,10 @@
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
+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) );
@@ -1281,7 +219,7 @@
return pGraph;
}
-@@ -109,8 +109,8 @@ Kit_Graph_t * Kit_GraphCreateLeaf( int i
+@@ -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 );
@@ -1292,7 +230,7 @@
return pGraph;
}
-@@ -174,8 +174,8 @@ Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Grap
+@@ -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;
@@ -1303,7 +241,7 @@
return Kit_EdgeCreate( pGraph->nSize - 1, 0 );
}
-@@ -198,12 +198,12 @@ Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph
+@@ -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;
@@ -1320,7 +258,7 @@
return Kit_EdgeCreate( pGraph->nSize - 1, 1 );
}
-@@ -224,11 +224,11 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Grap
+@@ -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
@@ -1335,7 +273,7 @@
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
+@@ -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
@@ -1351,7 +289,7 @@
}
return eNode;
}
-@@ -267,7 +267,7 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Grap
+@@ -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
@@ -1360,7 +298,7 @@
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
+@@ -275,16 +275,16 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edg
else
{
// complement the arguments
@@ -1381,7 +319,7 @@
}
return eNode;
}
-@@ -326,10 +326,10 @@ unsigned Kit_GraphToTruth( Kit_Graph_t *
+@@ -326,10 +326,10 @@ unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph )
// compute the function for each internal node
Kit_GraphForEachNode( pGraph, pNode, i )
{
@@ -1396,87 +334,22 @@
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
- Kit_GraphForEachNode( pGraph, pNode, i )
- {
- // get the children of this node
-- pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node );
-- pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node );
-+ pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.edgeBits.Node );
-+ pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.edgeBits.Node );
- // get the AIG nodes corresponding to the children
- pAnd0 = pNode0->pFunc;
- pAnd1 = pNode1->pFunc;
- if ( pAnd0 && pAnd1 )
- {
- // if they are both present, find the resulting node
-- pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.fCompl );
-- pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.fCompl );
-+ pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.edgeBits.fCompl );
-+ pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.edgeBits.fCompl );
- 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
- //printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) );
- 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( 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/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,151 +424,213 @@
#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<Minisat::Solver>(bm->soft_timeout_expired);
- else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS)
- newS = new MinisatCore_prop<Minisat::Solver_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);
+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
+ {
+- for (int i=0; i < $3;i++)
++ for (unsigned int i=0; i < $3;i++)
+ {
+ parserInterface->push();
+ }
+@@ -247,7 +247,7 @@ cmdi:
}
- else
+ | LPAREN_TOK POP_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->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);
+
+ // 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);
+
+ // 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;
+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 = "";
---- ./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]);
- }
+- 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 = "";
-@@ -465,7 +465,7 @@ namespace simplifier
+- 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;
- assert(FixedBits::equals(newBits, current));
+- 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 < n.Degree(); i++)
-+ for (size_t i = 0; i < n.Degree(); i++)
- {
- if (!FixedBits::equals(*getUpdatedFixedBits(n[i]),
- childrenFixedBits[i]))
---- ./src/simplifier/constantBitP/FixedBits.cpp.orig 2012-02-17 06:48:39.000000000 -0700
-+++ ./src/simplifier/constantBitP/FixedBits.cpp 2012-08-07 16:34:38.053114918 -0600
-@@ -382,7 +382,7 @@ namespace simplifier
- void
- FixedBits::fromUnsigned(unsigned val)
- {
-- for (unsigned i = 0; i < width; i++)
-+ for (unsigned i = 0; i < (unsigned) width; i++)
- {
- if (i < (unsigned) width && i < sizeof(unsigned) * 8)
- {
---- ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp.orig 2012-04-22 05:52:33.000000000 -0600
-+++ ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp 2012-08-07 16:37:05.172884335 -0600
-@@ -128,6 +128,7 @@ fast_exit(FixedBits& c0, FixedBits& c1)
- }
- return false;
- }
-+ return false;
- }
+- 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());
---- ./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);
+ // 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);
+ }
-- int substitutionsLastApplied;
-+ size_t substitutionsLastApplied;
- public:
+- 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..
- 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
- }
+ 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);
+ }
- vector<Symbols*> 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<Symbols*> av;
- VarSeenInTerm(symbol,visited,*symbols,av);
+- 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);
-- 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());
+ bool bad= false;
+- for (int i =0; i < children.size(); i++)
++ for (size_t i =0; i < children.size(); i++)
+ {
+ if (children[i] == NULL)
+ {
+@@ -617,7 +617,7 @@ namespace BEEV
+ if (CONSTANTBV::Set_Max(max) >= width)
+ bad = true;
- //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;
+- 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
---- ./src/simplifier/UseITEContext.h.orig 2012-08-07 16:26:07.500857699 -0600
-+++ ./src/simplifier/UseITEContext.h 2012-08-07 16:26:11.756851943 -0600
-@@ -28,7 +28,7 @@ namespace BEEV
- if (n.GetKind() == NOT && n[0].GetKind() == OR)
- {
- ASTVec flat = FlattenKind(OR, n[0].GetChildren());
-- for (int i = 0; i < flat.size(); i++)
-+ for (size_t i = 0; i < flat.size(); i++)
- context.insert(nf->CreateNode(NOT, flat[i]));
- }
- else if (n.GetKind() == AND)
-@@ -86,7 +86,7 @@ namespace BEEV
- }
- else
- {
-- for (int i = 0; i < n.GetChildren().size(); i++)
-+ for (size_t i = 0; i < n.GetChildren().size(); i++)
- new_children.push_back(visit(n[i], visited, visited_empty, context));
- }
+ 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]);
---- ./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:
+ 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:
@@ -1704,7 +639,7 @@
build(n[i],polarity);
break;
-@@ -121,7 +121,7 @@ public:
+@@ -122,7 +122,7 @@ public:
default:
polarity = bothPolarity; // both
@@ -1713,139 +648,124 @@
build(n[i],polarity);
break;
}
---- ./src/simplifier/simplifier.cpp.orig 2012-04-29 04:49:41.000000000 -0600
-+++ ./src/simplifier/simplifier.cpp 2012-08-07 16:26:11.757851942 -0600
-@@ -248,7 +248,7 @@ namespace BEEV
- assert(false);
- }
-
-- for (int i = 0; i < n.Degree(); i++)
-+ for (size_t i = 0; i < n.Degree(); i++)
- {
- checkIfInSimplifyMap(n[i], visited);
- }
-@@ -523,6 +523,7 @@ namespace BEEV
- return getConstantBit(n[0], i);
-
- assert(false);
-+ return -1;
- }
+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<MutableASTNode *> tempChildren;
+ tempChildren.reserve(n.Degree());
- ASTNode
-@@ -1302,7 +1303,7 @@ namespace BEEV
- else
- {
- ASTVec newC;
-- for (int i = 0; i < a.GetChildren().size(); i++)
-+ for (size_t i = 0; i < a.GetChildren().size(); i++)
- {
- newC.push_back(SimplifyFormula(a[i], false, VarConstMap));
- }
-@@ -1664,9 +1665,9 @@ namespace BEEV
- assert(BVMULT == k || SBVDIV == k || BVPLUS ==k);
- const int inputValueWidth = output.GetValueWidth();
+- for (int i = 0; i < n.Degree(); i++)
++ for (size_t i = 0; i < n.Degree(); i++)
+ tempChildren.push_back(build(n[i], visited));
-- int lengthA = output.GetChildren()[0][0].GetValueWidth();
-- int lengthB = output.GetChildren()[1][0].GetValueWidth();
-- int maxLength;
-+ unsigned int lengthA = output.GetChildren()[0][0].GetValueWidth();
-+ unsigned int lengthB = output.GetChildren()[1][0].GetValueWidth();
-+ unsigned int maxLength;
- if (BVMULT == output.GetKind())
- maxLength = lengthA + lengthB;
- else if (BVPLUS == output.GetKind() || SBVDIV == output.GetKind())
-@@ -1694,7 +1695,7 @@ namespace BEEV
- {
- const ASTNode a = children[0];
- const ASTNode b = children[1];
-- const int width = children[0].GetValueWidth();
-+ const unsigned int width = children[0].GetValueWidth();
- ASTNode output;
+ MutableASTNode * mut = createNode(n);
- assert(b.isConstant());
-@@ -1725,7 +1726,7 @@ namespace BEEV
- {
- const ASTNode a = children[0];
- const ASTNode b = children[1];
-- const int width = children[0].GetValueWidth();
-+ const unsigned int width = children[0].GetValueWidth();
- ASTNode output;
+- for (int i = 0; i < n.Degree(); i++)
++ for (size_t i = 0; i < n.Degree(); i++)
+ tempChildren[i]->parents.insert(mut);
- assert(b.isConstant());
-@@ -1906,7 +1907,7 @@ namespace BEEV
- //I haven't measured if this is worth the expense.
- {
- bool notSimplified = false;
-- for (int i = 0; i < inputterm.Degree(); i++)
-+ for (size_t i = 0; i < inputterm.Degree(); i++)
- if (inputterm[i].GetType() != ARRAY_TYPE)
- if (!hasBeenSimplified(inputterm[i]))
- {
-@@ -2247,7 +2248,6 @@ namespace BEEV
- case BVEXTRACT:
- {
- const unsigned innerLow = a0[2].GetUnsignedConst();
-- const unsigned innerHigh = a0[1].GetUnsignedConst();
+ mut->children.insert(mut->children.end(),tempChildren.begin(),tempChildren.end());
+@@ -86,7 +86,7 @@ private:
+ assert(found);
+ }
- output = nf->CreateTerm(BVEXTRACT, inputValueWidth, a0[0], _bm->CreateBVConst(32, i_val + innerLow),
- _bm->CreateBVConst(32, j_val + innerLow));
-@@ -2647,7 +2647,7 @@ namespace BEEV
- assert(BVTypeCheck(output));
+- 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;
- // If the leading bits are zero. Replace it by a concat with zero.
-- int i;
-+ unsigned int i;
- if (output.GetKind() == BVAND && output.Degree() == 2 && ((i = numberOfLeadingZeroes(output[0])) > 0))
- {
- // i contains the number of leading zeroes.
-@@ -2669,13 +2669,13 @@ namespace BEEV
- }
- if (output.GetKind() == BVAND)
- {
-- int trailingZeroes = 0;
-- for (int i = 0; i < output.Degree(); i++)
-+ unsigned int trailingZeroes = 0;
-+ for (size_t i = 0; i < output.Degree(); i++)
- {
- const ASTNode& n = output[i];
- if (n.GetKind() != BVCONST)
- continue;
-- int j;
-+ unsigned int j;
- for (j = 0; j < n.GetValueWidth(); j++)
- if (CONSTANTBV::BitVector_bit_test(n.GetBVConst(), j))
- break;
-@@ -2692,7 +2692,7 @@ namespace BEEV
- //cerr << "old" << output;
- ASTNode zeroes = _bm->CreateZeroConst(trailingZeroes);
- ASTVec newChildren;
-- for (int i = 0; i < output.Degree(); i++)
-+ for (size_t i = 0; i < output.Degree(); i++)
- newChildren.push_back(
- nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - trailingZeroes, output[i],
- _bm->CreateBVConst(32, output.GetValueWidth() - 1),
---- ./src/simplifier/RemoveUnconstrained.cpp.orig 2012-03-19 21:59:03.000000000 -0600
-+++ ./src/simplifier/RemoveUnconstrained.cpp 2012-08-07 16:28:13.624742813 -0600
-@@ -55,7 +55,7 @@ namespace BEEV
+ 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));
- bool allChildrenAreUnconstrained(vector <MutableASTNode*> children)
- {
-- for (int i =0; i < children.size(); i++)
-+ for (size_t i =0; i < children.size(); i++)
- if (!children[i]->isUnconstrained())
- return false;
+ // 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);
-@@ -100,7 +100,7 @@ namespace BEEV
- // Going to be rebuilt later anyway, so discard.
- vector<MutableASTNode*> variables;
+ propagateUpDirty();
+@@ -249,7 +249,7 @@ private:
-- for (int i =0; i <extracts.size(); i++)
-+ for (size_t i =0; i <extracts.size(); i++)
- {
- ASTNode& var = extracts[i]->n;
- assert(var.GetKind() == SYMBOL);
-@@ -151,7 +151,7 @@ namespace BEEV
- }
+ ASTNode& node = all[i]->n;
+ bool found[node.GetValueWidth()];
+- for (int j=0; j <node.GetValueWidth();j++)
++ for (unsigned int j=0; j <node.GetValueWidth();j++)
+ found[j] = false;
+
+ ParentsType::const_iterator it;
+@@ -330,7 +330,7 @@ private:
+ static void
+ cleanup()
+ {
+- for (int i = 0; i < all.size(); i++)
++ for (size_t i = 0; i < all.size(); i++)
+ delete all[i];
+ all.clear();
+ }
+diff --git a/src/simplifier/PropagateEqualities.cpp b/src/simplifier/PropagateEqualities.cpp
+index 09534ee..5facb98 100644
+--- a/src/simplifier/PropagateEqualities.cpp
++++ b/src/simplifier/PropagateEqualities.cpp
+@@ -31,10 +31,10 @@ namespace BEEV
+
+ bool result = false;
+ if (k == XOR)
+- 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]);
+
+@@ -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 (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 <MutableASTNode*> 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<MutableASTNode*> variables;
+
+- for (int i =0; i <extracts.size(); i++)
++ for (size_t i =0; i <extracts.size(); i++)
+ {
+ ASTNode& var = extracts[i]->n;
+ assert(var.GetKind() == SYMBOL);
+@@ -151,7 +151,7 @@ namespace BEEV
+ }
ASTNode concat = concatVec[0];
- for (int i=1; i < concatVec.size();i++)
@@ -1871,15 +791,6 @@
children.push_back(mutable_children[j]->n);
const size_t numberOfChildren = children.size();
-@@ -217,7 +217,7 @@ namespace BEEV
- unsigned indexWidth = muteNode.getParent().n.GetIndexWidth();
-
- ASTNode other;
-- MutableASTNode* muteOther;
-+ MutableASTNode* muteOther = NULL;
-
- if(numberOfChildren == 2)
- {
@@ -242,7 +242,7 @@ namespace BEEV
{
int found = 0;
@@ -1916,363 +827,358 @@
if (children[i] != var)
other.push_back(mutable_children[i]->toASTNode(nf));
-@@ -639,7 +639,6 @@ namespace BEEV
- {
- ASTNode v =replaceParentWithFresh(muteParent, variable_array);
-
-- const unsigned resultWidth = width;
- const unsigned operandWidth = var.GetValueWidth();
- assert(children[0] == var); // It can't be anywhere else.
-
---- ./src/simplifier/AlwaysTrue.h.orig 2012-08-07 16:26:07.501857698 -0600
-+++ ./src/simplifier/AlwaysTrue.h 2012-08-07 16:26:11.759851939 -0600
-@@ -85,7 +85,7 @@ public:
- else
- new_state = state;
+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);
-- for (int i=0; i < n.Degree(); i++)
-+ for (size_t i=0; i < n.Degree(); i++)
+ sort(av.begin(), av.end());
+- for (int i = 0; i < av.size(); i++)
++ for (size_t i = 0; i < av.size(); 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++)
+ 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)
{
- 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 flat = FlattenKind(OR, n[0].GetChildren());
+- for (int i = 0; i < flat.size(); i++)
++ for (size_t i = 0; i < flat.size(); i++)
+ context.insert(nf->CreateNode(NOT, flat[i]));
+ }
+ else if (n.GetKind() == AND)
+@@ -86,7 +86,7 @@ namespace BEEV
+ }
+ else
{
- 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
+- for (int i = 0; i < n.GetChildren().size(); i++)
++ for (size_t i = 0; i < n.GetChildren().size(); i++)
+ new_children.push_back(visit(n[i], visited, visited_empty, context));
+ }
- 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<MutableASTNode *> tempChildren;
- tempChildren.reserve(n.Degree());
+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) {
+ }
-- for (int i = 0; i < n.Degree(); i++)
-+ for (size_t i = 0; i < n.Degree(); i++)
- tempChildren.push_back(build(n[i], visited));
+ vector<Symbols*> 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<Symbols*> av;
+ VarSeenInTerm(symbol,visited,*symbols,av);
- MutableASTNode * mut = createNode(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::VarSeenInTerm(const ASTNode& var,
+ sort(av.begin(), av.end());
-- for (int i = 0; i < n.Degree(); i++)
-+ for (size_t i = 0; i < n.Degree(); i++)
- tempChildren[i]->parents.insert(mut);
+ //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;
- mut->children.insert(mut->children.end(),tempChildren.begin(),tempChildren.end());
-@@ -86,7 +86,7 @@ private:
- assert(found);
+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;
+ }
++ return true;
+ }
-- 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);
+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<FixedBits*>& children,
+ if (whatIs == QUOTIENT_IS_OUTPUT) {
+ setUnsignedMinMax(output, minQuotient, maxQuotient);
- propagateUpDirty();
-@@ -249,7 +249,7 @@ private:
+- 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);
- ASTNode& node = all[i]->n;
- bool found[node.GetValueWidth()];
-- for (int j=0; j <node.GetValueWidth();j++)
-+ for (unsigned int j=0; j <node.GetValueWidth();j++)
- found[j] = false;
+- for (int i =0; i < width;i++)
++ for (unsigned int i =0; i < width;i++)
+ CONSTANTBV::BitVector_Bit_On(maxQuotient,i);
+ }
- ParentsType::const_iterator it;
-@@ -330,7 +330,7 @@ private:
- static void
- cleanup()
+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 < all.size(); i++)
-+ for (size_t i = 0; i < all.size(); i++)
- delete all[i];
- all.clear();
+- for (int i = 0; i < n.Degree(); i++)
++ for (size_t i = 0; i < n.Degree(); i++)
+ workList->push(n[i]);
}
---- ./src/simplifier/SubstitutionMap.cpp.orig 2012-03-19 21:59:03.000000000 -0600
-+++ ./src/simplifier/SubstitutionMap.cpp 2012-08-07 16:26:11.760851937 -0600
-@@ -212,7 +212,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.
---- ./src/simplifier/EstablishIntervals.h.orig 2012-08-07 16:26:07.504857695 -0600
-+++ ./src/simplifier/EstablishIntervals.h 2012-08-07 16:26:11.761851936 -0600
-@@ -118,7 +118,7 @@ namespace BEEV
- ASTVec new_children;
- new_children.reserve(result.GetChildren().size());
+@@ -469,7 +469,7 @@ namespace simplifier
-- 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())
-@@ -497,7 +497,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);
-@@ -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);
+ assert(FixedBits::equals(newBits, current));
- bool bad= false;
-- for (int i =0; i < children.size(); i++)
-+ for (size_t i =0; i < children.size(); i++)
+- 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)
{
- 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;
+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);
-- 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
+ 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);
+ }
- 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();
- }
+- for (int i = 0; i < n.Degree(); i++)
++ for (size_t i = 0; i < n.Degree(); i++)
+ {
+ checkIfInSimplifyMap(n[i], visited);
}
-@@ -797,10 +797,10 @@ namespace BEEV
+@@ -523,6 +523,7 @@ namespace BEEV
+ return getConstantBit(n[0], i);
- ~EstablishIntervals()
- {
-- for (int i =0; i < toDeleteLater.size();i++)
-+ for (size_t i =0; i < toDeleteLater.size();i++)
- delete toDeleteLater[i];
+ assert(false);
++ return -1;
+ }
-- for (int i =0; i < likeAutoPtr.size();i++)
-+ for (size_t i =0; i < likeAutoPtr.size();i++)
- CONSTANTBV::BitVector_Destroy(likeAutoPtr[i]);
+ ASTNode
+@@ -1302,7 +1303,7 @@ namespace BEEV
+ else
+ {
+ ASTVec newC;
+- for (int i = 0; i < a.GetChildren().size(); i++)
++ for (size_t i = 0; i < a.GetChildren().size(); i++)
+ {
+ newC.push_back(SimplifyFormula(a[i], false, VarConstMap));
+ }
+@@ -1664,9 +1665,9 @@ namespace BEEV
+ assert(BVMULT == k || SBVDIV == k || BVPLUS ==k);
+ const int inputValueWidth = output.GetValueWidth();
- 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();
+- int lengthA = output.GetChildren()[0][0].GetValueWidth();
+- int lengthB = output.GetChildren()[1][0].GetValueWidth();
+- int maxLength;
++ unsigned int lengthA = output.GetChildren()[0][0].GetValueWidth();
++ unsigned int lengthB = output.GetChildren()[1][0].GetValueWidth();
++ unsigned int maxLength;
+ if (BVMULT == output.GetKind())
+ maxLength = lengthA + lengthB;
+ else if (BVPLUS == output.GetKind() || SBVDIV == output.GetKind())
+@@ -1694,7 +1695,7 @@ namespace BEEV
+ {
+ const ASTNode a = children[0];
+ const ASTNode b = children[1];
+- const int width = children[0].GetValueWidth();
++ const unsigned int width = children[0].GetValueWidth();
+ ASTNode output;
- if (in1 == in2)
- //terms are syntactically the same
-@@ -462,8 +462,8 @@ SimplifyingNodeFactory::CreateSimpleEQ(c
- {
- int match1 = -1, match2 = -1;
+ assert(b.isConstant());
+@@ -1725,7 +1726,7 @@ namespace BEEV
+ {
+ const ASTNode a = children[0];
+ const ASTNode b = children[1];
+- const int width = children[0].GetValueWidth();
++ const unsigned int width = children[0].GetValueWidth();
+ ASTNode output;
-- 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++)
+ assert(b.isConstant());
+@@ -1906,7 +1907,7 @@ namespace BEEV
+ //I haven't measured if this is worth the expense.
+ {
+ bool notSimplified = false;
+- for (int i = 0; i < inputterm.Degree(); i++)
++ for (size_t i = 0; i < inputterm.Degree(); i++)
+ if (inputterm[i].GetType() != ARRAY_TYPE)
+ if (!hasBeenSimplified(inputterm[i]))
{
- 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;
+@@ -2658,7 +2659,7 @@ namespace BEEV
+ assert(BVTypeCheck(output));
-- 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 the leading bits are zero. Replace it by a concat with zero.
+- int i;
++ unsigned int i;
+ if (output.GetKind() == BVAND && output.Degree() == 2 && ((i = numberOfLeadingZeroes(output[0])) > 0))
+ {
+ // i contains the number of leading zeroes.
+@@ -2680,13 +2681,13 @@ namespace BEEV
+ }
+ if (output.GetKind() == BVAND)
{
-- 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;
-+ }
-
- 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)
+- int trailingZeroes = 0;
+- for (int i = 0; i < output.Degree(); i++)
++ unsigned int trailingZeroes = 0;
++ for (size_t i = 0; i < output.Degree(); i++)
{
- 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 ASTNode& n = output[i];
+ if (n.GetKind() != BVCONST)
+ continue;
+- int j;
++ unsigned int j;
+ for (j = 0; j < n.GetValueWidth(); j++)
+ if (CONSTANTBV::BitVector_bit_test(n.GetBVConst(), j))
+ break;
+@@ -2703,7 +2704,7 @@ namespace BEEV
+ //cerr << "old" << output;
+ ASTNode zeroes = _bm->CreateZeroConst(trailingZeroes);
+ ASTVec newChildren;
+- for (int i = 0; i < output.Degree(); i++)
++ for (size_t i = 0; i < output.Degree(); i++)
+ newChildren.push_back(
+ nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - trailingZeroes, output[i],
+ _bm->CreateBVConst(32, output.GetValueWidth() - 1),
+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
- 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<ASTNode, ArrayTransformer::ArrayRead>& mapper = iset->second;
-
- for (map<ASTNode, ArrayTransformer::ArrayRead>::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
+ // 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();
- visited.insert(n.GetNodeNum());
+ 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);
+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.Degree(); i++)
-+ for (size_t i = 0; i < n.Degree(); i++)
- numberOfReadsLessThan(n[i], visited, soFar,limit);
- }
+- 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;
+@@ -1831,22 +1831,24 @@ namespace BEEV
+ for (int i = 0; i < b->getWidth(); i++)
+ {
+ if (b->isFixed(i))
+- if (b->getValue(i))
+- {
+- assert(v[i]== BBTrue);
+- }
+- else
+- {
+- if (v[i] != BBFalse)
++ {
++ if (b->getValue(i))
+ {
+- 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;
++ }
+
+- assert(v[i]== BBFalse);
+- }
++ assert(v[i]== BBFalse);
++ }
++ }
+ }
+ }
+ }
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}
-
-# 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
+make install DESTDIR=%{buildroot}
+
+# 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 <loganjerry at gmail.com> - 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 <loganjerry at gmail.com> - 0.1-18.20130223svn
- Really rebuild for cryptominisat 2.9.8
More information about the scm-commits
mailing list