Merge pull request #2020 from tautschnig/sat-cleanup

Remove outdated SAT solvers

Author: tautschnig

src/common

@@ -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

src/config.inc

@@ -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
@@ -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
@@ -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"

src/solvers/CMakeLists.txt

@@ -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
@@ -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
 )
@@ -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})

src/solvers/Makefile

@@ -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)
@@ -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)
@@ -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) \
@@ -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 \
@@ -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 \
@@ -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)
@@ -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)
 
 ###############################################################################
 

src/solvers/sat/read_dimacs_cnf.cpp

@@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
 // #define SATCHECK_MINISAT2
 // #define SATCHECK_GLUCOSE
 // #define SATCHECK_BOOLEFORCE
-// #define SATCHECK_PRECOSAT
 // #define SATCHECK_PICOSAT
 // #define SATCHECK_LINGELING
 
@@ -47,10 +46,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #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
@@ -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"