214 lines
6.9 KiB
Diff
214 lines
6.9 KiB
Diff
diff --git a/CMakeLists.txt b/CMakeLists.txt
|
|
index a43eb68..c0db102 100644
|
|
--- a/CMakeLists.txt
|
|
+++ b/CMakeLists.txt
|
|
@@ -109,6 +109,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_GNUCPP11)
|
|
@@ -219,6 +220,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>
|
|
|
|
class RunTimes : boost::noncopyable
|
|
{
|
|
diff --git a/src/libstp/CMakeLists.txt b/src/libstp/CMakeLists.txt
|
|
index 8ad9ccb..045b8ac 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
|
|
@@ -74,7 +73,7 @@ endif()
|
|
# 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 8646824..0d77ff5 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
|
|
{
|
|
+ class CryptoMinisatSolver : public CMSat::Solver
|
|
+ {
|
|
+ public:
|
|
+ uint64_t getConflicts() const { return conflicts; }
|
|
+ uint64_t getDecisions() const { return decisions; }
|
|
+ uint64_t getMaxLiterals() const { return max_literals; }
|
|
+ uint64_t getPropagations() const { return propagations; }
|
|
+ uint64_t getRndDecisions() const { return rnd_decisions; }
|
|
+ uint64_t getStarts() const { return starts; }
|
|
+ uint64_t getTotLiterals() const { return tot_literals; }
|
|
+ };
|
|
|
|
CryptoMinisat::CryptoMinisat()
|
|
{
|
|
- s = new MINISAT::Solver();
|
|
+ s = new CryptoMinisatSolver();
|
|
}
|
|
|
|
CryptoMinisat::~CryptoMinisat()
|
|
@@ -30,9 +41,9 @@ namespace BEEV
|
|
// Cryptominisat uses a slightly different Lit class too.
|
|
|
|
// VERY SLOW>
|
|
- MINISAT::vec<MINISAT::Lit> v;
|
|
+ CMSat::vec<CMSat::Lit> v;
|
|
for (int i =0; i<ps.size();i++)
|
|
- v.push(MINISAT::Lit(var(ps[i]), sign(ps[i])));
|
|
+ v.push(CMSat::Lit(var(ps[i]), sign(ps[i])));
|
|
|
|
return s->addClause(v);
|
|
}
|
|
@@ -63,7 +74,7 @@ namespace BEEV
|
|
|
|
void CryptoMinisat::setVerbosity(int v)
|
|
{
|
|
- s->verbosity = v;
|
|
+ s->conf.verbosity = v;
|
|
}
|
|
|
|
int CryptoMinisat::nVars()
|
|
diff --git a/src/sat/CryptoMinisat.h b/src/sat/CryptoMinisat.h
|
|
index 76e7a47..9ecb5b6 100644
|
|
--- a/src/sat/CryptoMinisat.h
|
|
+++ b/src/sat/CryptoMinisat.h
|
|
@@ -6,16 +6,13 @@
|
|
|
|
#include "SATSolver.h"
|
|
|
|
-namespace MINISAT
|
|
-{
|
|
- class Solver;
|
|
-}
|
|
-
|
|
namespace BEEV
|
|
{
|
|
+ class CryptoMinisatSolver;
|
|
+
|
|
class CryptoMinisat : public SATSolver
|
|
{
|
|
- MINISAT::Solver* s;
|
|
+ CryptoMinisatSolver* s;
|
|
|
|
public:
|
|
CryptoMinisat();
|
|
diff --git a/tests/api/C/CMakeLists.txt b/tests/api/C/CMakeLists.txt
|
|
index dcdcc3d..e0146a8 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
|