Skip to content

Remove outdated SAT solvers #2020

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Apr 8, 2018
Merged

Remove outdated SAT solvers #2020

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
28cca9c
Remove unused DIMACS parser
tautschnig Apr 8, 2018
a0fd3f7
Remove support for Limmat as a SAT solver
tautschnig Apr 8, 2018
2aa81eb
Remove support for SMVSAT
tautschnig Apr 8, 2018
70741ff
Remove support for Precosat
tautschnig Apr 8, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 1 addition & 5 deletions src/common
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -159,18 +159,14 @@ else
endif

# select default solver to be minisat2 if no other is specified
ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT),)
ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT),)
MINISAT2 = ../../minisat-2.2.1
endif

ifneq ($(IPASIR),)
CP_CXXFLAGS += -DHAVE_IPASIR
endif

ifneq ($(PRECOSAT),)
CP_CXXFLAGS += -DHAVE_PRECOSAT
endif

ifneq ($(PICOSAT),)
CP_CXXFLAGS += -DHAVE_PICOSAT
endif
Expand Down
10 changes: 0 additions & 10 deletions src/config.inc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ endif
#LIB_GLPK = -lglpk

# SAT-solvers we have
#PRECOSAT = ../../precosat-576-7e5e66f-120112
#PICOSAT = ../../picosat-959
#LINGELING = ../../lingeling-587f-4882048-110513
#CHAFF = ../../zChaff
Expand All @@ -25,16 +24,11 @@ endif
#MINISAT2 = ../../minisat-2.2.1
#IPASIR = ../../ipasir
#GLUCOSE = ../../glucose-syrup
#SMVSAT =

# Extra library for SAT solver. This should link to the archive file to be used
# when linking against an IPASIR solver.
LIBSOLVER =

ifneq ($(PRECOSAT),)
CP_CXXFLAGS += -DSATCHECK_PRECOSAT
endif

ifneq ($(PICOSAT),)
CP_CXXFLAGS += -DSATCHECK_PICOSAT
endif
Expand Down Expand Up @@ -63,10 +57,6 @@ ifneq ($(GLUCOSE),)
CP_CXXFLAGS += -DSATCHECK_GLUCOSE
endif

ifneq ($(SMVSAT),)
CP_CXXFLAGS += -DSATCHECK_SMVSAT
endif

# Signing identity for MacOS Gatekeeper

OSX_IDENTITY="Developer ID Application: Daniel Kroening"
12 changes: 0 additions & 12 deletions src/solvers/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,6 @@ set(minisat2_source
set(glucose_source
${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_glucose.cpp
)
set(smvsat_source
${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_smvsat.cpp
)
set(squolem2_source
${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_squolem.cpp
${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_squolem_core.cpp
Expand All @@ -29,9 +26,6 @@ set(cudd_source
${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_bdd_core.cpp
${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_skizzo_core.cpp
)
set(precosat_source
${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_precosat.cpp
)
set(picosat_source
${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_picosat.cpp
)
Expand All @@ -44,25 +38,19 @@ 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
${chaff_source}
${minisat_source}
${minisat2_source}
${glucose_source}
${smvsat_source}
${squolem2_source}
${cudd_source}
${precosat_source}
${picosat_source}
${lingeling_source}
${booleforce_source}
${minibdd_source}
${limmat_source}
)

add_library(solvers ${sources})
Expand Down
32 changes: 4 additions & 28 deletions src/solvers/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,12 +36,6 @@ ifneq ($(GLUCOSE),)
CP_CXXFLAGS += -DHAVE_GLUCOSE -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
endif

ifneq ($(SMVSAT),)
SMVSAT_SRC=sat/satcheck_smvsat.cpp
SMVSAT_INCLUDE=-I $(SMVSAT)/include
SMVSAT_LIB=$(SMVSAT)/lib/libsmvsat$(LIBEXT)
endif

ifneq ($(SQUOLEM2),)
SQUOLEM2_SRC=qbf/qbf_squolem.cpp qbf/qbf_squolem_core.cpp
SQUOLEM2_INCLUDE=-I $(SQUOLEM2)
Expand All @@ -56,13 +50,6 @@ ifneq ($(CUDD),)
-L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
endif

ifneq ($(PRECOSAT),)
PRECOSAT_SRC=sat/satcheck_precosat.cpp
PRECOSAT_INCLUDE=-I $(PRECOSAT)
PRECOSAT_LIB=$(PRECOSAT)/precosat$(OBJEXT)
CP_CXXFLAGS += -DHAVE_PRECOSAT
endif

ifneq ($(PICOSAT),)
PICOSAT_SRC=sat/satcheck_picosat.cpp
PICOSAT_INCLUDE=-I $(PICOSAT)
Expand All @@ -77,13 +64,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) \
Expand All @@ -93,10 +73,7 @@ SRC = $(BOOLEFORCE_SRC) \
$(IPASIR_SRC) \
$(MINISAT_SRC) \
$(PICOSAT_SRC) \
$(PRECOSAT_SRC) \
$(SMVSAT_SRC) \
$(SQUOLEM2_SRC) \
$(LIMMAT_SRC) \
cvc/cvc_conv.cpp \
cvc/cvc_dec.cpp \
flattening/arrays.cpp \
Expand Down Expand Up @@ -199,7 +176,6 @@ SRC = $(BOOLEFORCE_SRC) \
sat/cnf_clause_list.cpp \
sat/dimacs_cnf.cpp \
sat/pbs_dimacs_cnf.cpp \
sat/read_dimacs_cnf.cpp \
sat/resolution_proof.cpp \
sat/satcheck.cpp \
smt1/smt1_conv.cpp \
Expand All @@ -214,8 +190,8 @@ SRC = $(BOOLEFORCE_SRC) \
INCLUDES += -I .. \
$(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
$(IPASIR_INCLUDE) \
$(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
$(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
$(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)

CLEANFILES = solvers$(LIBEXT) \
smt2_solver$(EXEEXT) smt2/smt2_solver$(OBJEXT) smt2/smt2_solver$(DEPEXT)
Expand All @@ -231,8 +207,8 @@ endif
endif

SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
$(MINISAT2_LIB) $(SMVSAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
$(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
$(MINISAT2_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
$(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)

###############################################################################

Expand Down
105 changes: 0 additions & 105 deletions src/solvers/sat/read_dimacs_cnf.cpp
View file
Open in desktop

This file was deleted.

19 changes: 0 additions & 19 deletions src/solvers/sat/read_dimacs_cnf.h
View file
Open in desktop

This file was deleted.

12 changes: 0 additions & 12 deletions src/solvers/sat/satcheck.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@ Author: Daniel Kroening, [email protected]
// #define SATCHECK_MINISAT2
// #define SATCHECK_GLUCOSE
// #define SATCHECK_BOOLEFORCE
// #define SATCHECK_PRECOSAT
// #define SATCHECK_PICOSAT
// #define SATCHECK_LINGELING

Expand Down Expand Up @@ -47,10 +46,6 @@ Author: Daniel Kroening, [email protected]
#define SATCHECK_BOOLEFORCE
#endif

#if defined(HAVE_PRECOSAT) && !defined(SATCHECK_PRECOSAT)
#define SATCHECK_PRECOSAT
#endif

#if defined(HAVE_PICOSAT) && !defined(SATCHECK_PICOSAT)
#define SATCHECK_PICOSAT
#endif
Expand Down Expand Up @@ -94,13 +89,6 @@ typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert;
typedef satcheck_ipasirt satcheckt;
typedef satcheck_ipasirt satcheck_no_simplifiert;

#elif defined SATCHECK_PRECOSAT

#include "satcheck_precosat.h"

typedef satcheck_precosatt satcheckt;
typedef satcheck_precosatt satcheck_no_simplifiert;

#elif defined SATCHECK_PICOSAT

#include "satcheck_picosat.h"
Expand Down
Loading