Set up glucose externalproject

Author: reuk

.travis.yml

@@ -163,7 +163,7 @@ jobs:
           packages:
             - g++-5
       install:
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_FLAGS_RELEASE=-O3' '-DCMAKE_CXX_FLAGS=-Wall -Wpedantic -Werror' '-DCMAKE_CXX_COMPILER=g++-5'
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_FLAGS_RELEASE=-O3' '-DCMAKE_CXX_FLAGS=-Wall -Wpedantic -Werror' '-DCMAKE_CXX_COMPILER=g++-5' '-Dsat_impl=glucose'
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE)
 

CMakeLists.txt

@@ -17,6 +17,10 @@ add_subdirectory(src)
 
 set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
 
+set(sat_impl "minisat2" CACHE STRING
+    "This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
+)
+
 if(${enable_cbmc_tests})
     enable_testing()
 endif()

scripts/glucose_CMakeLists.txt

@@ -0,0 +1,30 @@
+cmake_minimum_required(VERSION 3.2)
+
+# CBMC only uses part of glucose.
+# This CMakeLists is designed to build just the parts that are needed.
+
+set(CMAKE_OSX_DEPLOYMENT_TARGET "10.9")
+set(CMAKE_OSX_ARCHITECTURES "i386;x86_64")
+set(CMAKE_BUILD_TYPE RelWithDebInfo)
+
+add_library(glucose-condensed
+    simp/SimpSolver.cc
+    core/Solver.cc
+)
+
+target_include_directories(glucose-condensed
+    PUBLIC
+    $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
+    $<INSTALL_INTERFACE:include>
+)
+
+install(TARGETS glucose-condensed EXPORT glucose-condensed-targets
+    LIBRARY DESTINATION lib
+    ARCHIVE DESTINATION lib
+    RUNTIME DESTINATION bin
+    INCLUDES DESTINATION include
+)
+
+install(DIRECTORY . DESTINATION include FILES_MATCHING PATTERN "*.h")
+
+install(EXPORT glucose-condensed-targets DESTINATION lib/cmake/glucose-condensed)

src/CMakeLists.txt

@@ -89,18 +89,20 @@ set(extern_location ${CMAKE_CURRENT_BINARY_DIR}/extern)
 set(extern_include_directory ${extern_location}/include)
 file(MAKE_DIRECTORY ${extern_include_directory})
 
+################################################################################
+
 set(minisat_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}minisat2-condensed${CMAKE_STATIC_LIBRARY_SUFFIX})
 
-#   minisat download
-#   This downloads minisat2, then patches it.
-#   Then, it injects a minimal CMakeLists.txt so that we can build just the bits
-#   we actually want, without having to update the provided makefile.
+#   minisat download: This downloads minisat2, then patches it.  Then, it
+#   injects a minimal CMakeLists.txt so that we can build just the bits we
+#   actually want, without having to update the provided makefile.
+
 ExternalProject_Add(minisat2-extern
     PREFIX ${extern_location}
     URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
     PATCH_COMMAND patch -p1 -i ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
           COMMAND cmake -E copy ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt
-          CMAKE_ARGS -DCBMC_INCLUDE_DIR:path=${CMAKE_CURRENT_SOURCE_DIR} -DCMAKE_INSTALL_PREFIX:PATH=<INSTALL_DIR>
+          CMAKE_ARGS -DCMAKE_INSTALL_PREFIX:PATH=<INSTALL_DIR> -DCBMC_INCLUDE_DIR:path=${CMAKE_CURRENT_SOURCE_DIR}
     BUILD_BYPRODUCTS ${minisat_lib}
 )
 
@@ -111,6 +113,32 @@ set_target_properties(minisat2-condensed PROPERTIES
 )
 add_dependencies(minisat2-condensed minisat2-extern)
 
+################################################################################
+
+set(glucose_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}glucose-condensed${CMAKE_STATIC_LIBRARY_SUFFIX})
+
+#   glucose download: This downloads glucose, then patches it.  Then, it
+#   injects a minimal CMakeLists.txt so that we can build just the bits we
+#   actually want, without having to update the provided makefile.
+
+ExternalProject_Add(glucose-extern
+    PREFIX ${extern_location}
+    URL http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz
+    PATCH_COMMAND patch -p1 -i ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/glucose-syrup-patch
+          COMMAND cmake -E copy ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt
+          CMAKE_ARGS -DCMAKE_INSTALL_PREFIX:PATH=<INSTALL_DIR>
+    BUILD_BYPRODUCTS ${glucose_lib}
+)
+
+add_library(glucose-condensed STATIC IMPORTED)
+set_target_properties(glucose-condensed PROPERTIES
+    IMPORTED_LOCATION ${glucose_lib}
+    INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}"
+)
+add_dependencies(glucose-condensed glucose-extern)
+
+################################################################################
+
 #   Override add_executable to automatically sign the target on OSX.
 function(add_executable name)
     _add_executable(${name} ${ARGN})

src/solvers/CMakeLists.txt

@@ -1,5 +1,3 @@
-#   TODO Specify which solver to use (minisat2 etc.)
-
 #   We may use one of several different solver libraries.
 #   The following files wrap the chosen solver library.
 #   We remove them all from the solver-library sources list, and then add the
@@ -73,11 +71,16 @@ list(REMOVE_ITEM sources
 
 add_library(solvers ${sources} ${headers})
 
-if(TARGET minisat2-extern)
+if("${sat_impl}" STREQUAL "minisat2" AND TARGET minisat2-extern)
     target_sources(solvers PRIVATE ${minisat2_source})
     add_dependencies(solvers minisat2-extern)
-    target_compile_definitions(solvers PUBLIC HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS)
+    target_compile_definitions(solvers PUBLIC SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS)
     target_link_libraries(solvers minisat2-condensed)
+elseif("${sat_impl}" STREQUAL "glucose" AND TARGET glucose-extern)
+    target_sources(solvers PRIVATE ${glucose_source})
+    add_dependencies(solvers glucose-extern)
+    target_compile_definitions(solvers PUBLIC SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS)
+    target_link_libraries(solvers glucose-condensed)
 endif()
 
 target_link_libraries(solvers util)

src/solvers/sat/satcheck.h

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 // #define SATCHECK_ZCHAFF
 // #define SATCHECK_MINISAT1
-#define SATCHECK_MINISAT2
+// #define SATCHECK_MINISAT2
 // #define SATCHECK_GLUCOSE
 // #define SATCHECK_BOOLEFORCE
 // #define SATCHECK_PRECOSAT

src/solvers/sat/satcheck_glucose.cpp

@@ -114,7 +114,7 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
 template<typename T>
 propt::resultt satcheck_glucose_baset<T>::prop_solve()
 {
-  assert(status!=ERROR);
+  assert(status!=statust::ERROR);
 
   // We start counting at 1, thus there is one variable fewer.
   {
@@ -153,9 +153,8 @@ propt::resultt satcheck_glucose_baset<T>::prop_solve()
       {
         messaget::status() <<
           "SAT checker: instance is SATISFIABLE" << eom;
-        assert(!solver->model.empty());
-        status=SAT;
-        return P_SATISFIABLE;
+        status=statust::SAT;
+        return resultt::P_SATISFIABLE;
       }
       else
       {
@@ -165,8 +164,8 @@ propt::resultt satcheck_glucose_baset<T>::prop_solve()
     }
   }
 
-  status=UNSAT;
-  return P_UNSATISFIABLE;
+  status=statust::UNSAT;
+  return resultt::P_UNSATISFIABLE;
 }
 
 template<typename T>