Remove support for Limmat as a SAT solver

It wasn't available via configuration options anymore anyway and Limmat's victory at the SAT competition dates back to 2002.
smowton · Apr 8, 2018 · a0fd3f7 · a0fd3f7
1 parent 28cca9c
commit a0fd3f7
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 182 deletions.
diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
@@ -44,9 +44,6 @@ set(booleforce_source
 set(minibdd_source
     ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD/example.cpp
 )
-set(limmat_source
-    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_limmat.cpp
-)
 
 file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
@@ -62,7 +59,6 @@ list(REMOVE_ITEM sources
     ${lingeling_source}
     ${booleforce_source}
     ${minibdd_source}
-    ${limmat_source}
 )
 
 add_library(solvers ${sources})

diff --git a/src/solvers/Makefile b/src/solvers/Makefile
@@ -77,13 +77,6 @@ ifneq ($(LINGELING),)
   CP_CXXFLAGS += -DHAVE_LINGELING
 endif
 
-ifneq ($(LIMMAT),)
-  LIMMAT_SRC=sat/satcheck_limmat.cpp
-  LIMMAT_INCLUDE=-I $(LIMMAT)
-  LIMMAT_LIB=$(LIMMAT)/liblimmat$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_LIMMAT
-endif
-
 SRC = $(BOOLEFORCE_SRC) \
       $(CHAFF_SRC) \
       $(CUDD_SRC) \
@@ -96,7 +89,6 @@ SRC = $(BOOLEFORCE_SRC) \
       $(PRECOSAT_SRC) \
       $(SMVSAT_SRC) \
       $(SQUOLEM2_SRC) \
-      $(LIMMAT_SRC) \
       cvc/cvc_conv.cpp \
       cvc/cvc_dec.cpp \
       flattening/arrays.cpp \

diff --git a/src/solvers/sat/satcheck_limmat.cpp b/src/solvers/sat/satcheck_limmat.cpp
diff --git a/src/solvers/sat/satcheck_limmat.h b/src/solvers/sat/satcheck_limmat.h