Skip to content

Commit a0fd3f7

Browse files
committed
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.
1 parent 28cca9c commit a0fd3f7

File tree

4 files changed

+0
-182
lines changed

4 files changed

+0
-182
lines changed

src/solvers/CMakeLists.txt

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -44,9 +44,6 @@ set(booleforce_source
4444
set(minibdd_source
4545
${CMAKE_CURRENT_SOURCE_DIR}/miniBDD/example.cpp
4646
)
47-
set(limmat_source
48-
${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_limmat.cpp
49-
)
5047

5148
file(GLOB_RECURSE sources "*.cpp" "*.h")
5249
list(REMOVE_ITEM sources
@@ -62,7 +59,6 @@ list(REMOVE_ITEM sources
6259
${lingeling_source}
6360
${booleforce_source}
6461
${minibdd_source}
65-
${limmat_source}
6662
)
6763

6864
add_library(solvers ${sources})

src/solvers/Makefile

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -77,13 +77,6 @@ ifneq ($(LINGELING),)
7777
CP_CXXFLAGS += -DHAVE_LINGELING
7878
endif
7979

80-
ifneq ($(LIMMAT),)
81-
LIMMAT_SRC=sat/satcheck_limmat.cpp
82-
LIMMAT_INCLUDE=-I $(LIMMAT)
83-
LIMMAT_LIB=$(LIMMAT)/liblimmat$(LIBEXT)
84-
CP_CXXFLAGS += -DHAVE_LIMMAT
85-
endif
86-
8780
SRC = $(BOOLEFORCE_SRC) \
8881
$(CHAFF_SRC) \
8982
$(CUDD_SRC) \
@@ -96,7 +89,6 @@ SRC = $(BOOLEFORCE_SRC) \
9689
$(PRECOSAT_SRC) \
9790
$(SMVSAT_SRC) \
9891
$(SQUOLEM2_SRC) \
99-
$(LIMMAT_SRC) \
10092
cvc/cvc_conv.cpp \
10193
cvc/cvc_dec.cpp \
10294
flattening/arrays.cpp \

src/solvers/sat/satcheck_limmat.cpp

Lines changed: 0 additions & 137 deletions
This file was deleted.

src/solvers/sat/satcheck_limmat.h

Lines changed: 0 additions & 33 deletions
This file was deleted.

0 commit comments

Comments
 (0)